{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:10:09Z","timestamp":1784837409015,"version":"3.55.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319106953","type":"print"},{"value":"9783319106960","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10696-0_31","type":"book-chapter","created":{"date-parts":[[2014,8,27]],"date-time":"2014-08-27T14:33:45Z","timestamp":1409150025000},"page":"404-420","source":"Crossref","is-referenced-by-count":45,"title":["Accelerating Parametric Probabilistic Verification"],"prefix":"10.1007","author":[{"given":"Nils","family":"Jansen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Corzilius","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthias","family":"Volk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ralf","family":"Wimmer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-642-41202-8_20","volume-title":"Formal Methods and Software Engineering","author":"G. Su","year":"2013","unstructured":"Su, G., Rosenblum, D.S.: Asymptotic bounds for quantitative verification of perturbed probabilistic systems. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol.\u00a08144, pp. 297\u2013312. Springer, Heidelberg (2013)"},{"key":"31_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C. Daws","year":"2005","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol.\u00a03407, pp. 280\u2013294. Springer, Heidelberg (2005)"},{"issue":"1","key":"31_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"E.M. Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Software Tools for Technology Transfer\u00a013(1), 3\u201319 (2010)","journal-title":"Software Tools for Technology Transfer"},{"key":"31_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-540-78499-9_20","volume-title":"Foundations of Software Science and Computational Structures","author":"H. Gruber","year":"2008","unstructured":"Gruber, H., Johannsen, J.: Optimal lower bounds on regular expression size using communication complexity. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 273\u2013286. Springer, Heidelberg (2008)"},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-20398-5_12","volume-title":"NASA Formal Methods","author":"E.M. Hahn","year":"2011","unstructured":"Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric Markov decision processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 146\u2013161. Springer, Heidelberg (2011)"},{"key":"31_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"Computer Aided Verification","author":"E.M. Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: A model checker for parametric Markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 660\u2013664. Springer, Heidelberg (2010)"},{"key":"31_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Han, T., Katoen, J.P., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: Proc. of RTSS, pp. 173\u2013182. IEEE CS (2008)","DOI":"10.1109\/RTSS.2008.19"},{"key":"31_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-39799-8_35","volume-title":"Computer Aided Verification","author":"A. Puggelli","year":"2013","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 527\u2013542. Springer, Heidelberg (2013)"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-36742-7_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Benedikt","year":"2013","unstructured":"Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval Markov chains. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 32\u201346. Springer, Heidelberg (2013)"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Jansen, N., Corzilius, F., Volk, M., Wimmer, R., \u00c1brah\u00e1m, E., Katoen, J.P., Becker, B.: Accelerating parametric probabilistic verification. CoRR abs\/1312.3979 (2013)","DOI":"10.1007\/978-3-319-10696-0_31"},{"key":"31_CR12","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)"},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m, E., Jansen, N., Wimmer, R., Katoen, J.P., Becker, B.: DTMC model checking by SCC reduction. In: Proc. of QEST, pp. 37\u201346. IEEE CS (2010)","DOI":"10.1109\/QEST.2010.13"},{"issue":"2","key":"31_CR14","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM Journal on Computing\u00a01(2), 146\u2013160 (1972)","journal-title":"SIAM Journal on Computing"},{"key":"31_CR15","unstructured":"Quarteroni, A., Sacco, R., Saleri, F.: Numerical Mathematics. Springer (2000)"},{"key":"31_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D. Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 339\u2013354. Springer, Heidelberg (2012)"},{"issue":"1","key":"31_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/jsco.2001.0494","volume":"33","author":"C. Bauer","year":"2002","unstructured":"Bauer, C., Frink, A., Kreckel, R.: Introduction to the GiNaC framework for symbolic computation within the C++ programming language. J. Symb. Comput.\u00a033(1), 1\u201312 (2002)","journal-title":"J. Symb. Comput."},{"key":"31_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-58085-9_75","volume-title":"Types for Proofs and Programs","author":"L. Helmink","year":"1994","unstructured":"Helmink, L., Sellink, M., Vaandrager, F.: Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806, pp. 127\u2013165. Springer, Heidelberg (1994)"},{"issue":"1","key":"31_CR19","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"M.K. Reiter","year":"1998","unstructured":"Reiter, M.K., Rubin, A.D.: Crowds: Anonymity for web transactions. ACM Trans. on Information and System Security\u00a01(1), 66\u201392 (1998)","journal-title":"ACM Trans. on Information and System Security"},{"key":"31_CR20","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1109\/TNANO.2002.807393","volume":"1","author":"J. Han","year":"2002","unstructured":"Han, J., Jonker, P.: A system architecture solution for unreliable nanoelectronic devices. IEEE Transactions on Nanotechnology\u00a01, 201\u2013208 (2002)","journal-title":"IEEE Transactions on Nanotechnology"},{"issue":"3-4","key":"31_CR21","doi-asserted-by":"crossref","first-page":"209","DOI":"10.3233\/SAT190012","volume":"1","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling, and Computation\u00a01(3-4), 209\u2013236 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling, and Computation"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10696-0_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,23]],"date-time":"2020-08-23T19:39:36Z","timestamp":1598211576000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10696-0_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319106953","9783319106960"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10696-0_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}