{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:13:06Z","timestamp":1784837586243,"version":"3.55.0"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2020,7,29]],"date-time":"2020-07-29T00:00:00Z","timestamp":1595980800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,7,29]],"date-time":"2020-07-29T00:00:00Z","timestamp":1595980800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["NSF CCF-1900924"],"award-info":[{"award-number":["NSF CCF-1900924"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["NSF CNS-1553548"],"award-info":[{"award-number":["NSF CNS-1553548"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["NSF CNS-1314485"],"award-info":[{"award-number":["NSF CNS-1314485"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["NSF CCF-1319754"],"award-info":[{"award-number":["NSF CCF-1319754"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["NSF CCF-1564296"],"award-info":[{"award-number":["NSF CCF-1564296"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","award":["PhD Fellowship"],"award-info":[{"award-number":["PhD Fellowship"]}],"id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1901069"],"award-info":[{"award-number":["CCF-1901069"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1901069"],"award-info":[{"award-number":["CCF-1901069"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1007\/s10703-020-00348-y","type":"journal-article","created":{"date-parts":[[2020,7,29]],"date-time":"2020-07-29T16:03:58Z","timestamp":1596038638000},"page":"90-126","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Exact quantitative probabilistic model checking through rational search"],"prefix":"10.1007","volume":"56","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew S.","family":"Bauer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rohit","family":"Chadha","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"A. Prasad","family":"Sistla","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,7,29]]},"reference":[{"key":"348_CR1","unstructured":"(2017) Ensuring the reliability of your model checker: interval iteration for Markov decision processes. https:\/\/wwwtcs.inf.tu-dresden.de\/ALGI\/PUB\/CAV17\/"},{"key":"348_CR2","unstructured":"(2017) PRISM benchmark suite,http:\/\/www.prismmodelchecker.org\/benchmarks\/. Accessed 5 May 2020"},{"key":"348_CR3","unstructured":"(2017) PRISM case studies, http:\/\/www.prismmodelchecker.org\/casestudies\/. Accessed 5 May 2020"},{"key":"348_CR4","unstructured":"(2019) Apfloat. http:\/\/www.apfloat.org\/"},{"key":"348_CR5","unstructured":"(2019) CUDD. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/html\/"},{"key":"348_CR6","unstructured":"(2019) GNU multiple precision arithmetic library. https:\/\/gmplib.org\/"},{"key":"348_CR7","unstructured":"(2019) JScience. http:\/\/jscience.org\/"},{"key":"348_CR8","unstructured":"(2019) RationalSearch. https:\/\/publish.illinois.edu\/rationalmodelchecker\/"},{"key":"348_CR9","unstructured":"de Alfaro L (1997) Formal verification of probabilistic systems. Ph.D. thesis, Stanford University"},{"key":"348_CR10","volume-title":"Principles of model checking (representation and mind series)","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP (2008) Principles of model checking (representation and mind series). The MIT Press, Cambridge"},{"key":"348_CR11","doi-asserted-by":"crossref","unstructured":"Baier C, Klein J, Leuschner L, Parker D, Wunderlich S (2017) Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: Computer aided verification","DOI":"10.1007\/978-3-319-63387-9_8"},{"issue":"1","key":"348_CR12","doi-asserted-by":"publisher","first-page":"133","DOI":"10.4064\/fm-3-1-133-181","volume":"3","author":"S Banach","year":"1922","unstructured":"Banach S (1922) Sur les op\u00e9rations dans les ensembles abstraits et leur application aux \u00e9quations int\u00e9grales. Fundamenta Mathematicae 3(1):133\u2013181","journal-title":"Fundamenta Mathematicae"},{"key":"348_CR13","doi-asserted-by":"publisher","unstructured":"Bauer MS, Mathur U, Chadha R, Sistla AP, Viswanathan M (2017) Exact quantitative probabilistic model checking through rational search. In: Proceedings of the 17th conference on formal methods in computer-aided design, FMCAD Inc, Austin, TX, FMCAD \u201917, pp 92\u201399. https:\/\/doi.org\/10.23919\/FMCAD.2017.8102246. http:\/\/dl.acm.org\/citation.cfm?id=3168451.3168475","DOI":"10.23919\/FMCAD.2017.8102246"},{"key":"348_CR14","doi-asserted-by":"publisher","first-page":"813","DOI":"10.1109\/43.766730","volume":"13","author":"L Benini","year":"1999","unstructured":"Benini L, Bogliolo A, Paleologo GA, De Micheli G (1999) Policy optimization for dynamic power management. IEEE Trans Comput-Aided Des Integr Circuits Syst 13:813\u2013833","journal-title":"IEEE Trans Comput-Aided Des Integr Circuits Syst"},{"key":"348_CR15","doi-asserted-by":"publisher","first-page":"2447","DOI":"10.1109\/TCSI.2007.907863","volume":"54","author":"D Bhaduri","year":"2007","unstructured":"Bhaduri D, Shukla SK, Graham PS, Gokhale MB (2007) Reliability analysis of large circuits using scalable techniques and tools. IEEE Trans Circuits Syst I: Regul Pap 54:2447\u20132460","journal-title":"IEEE Trans Circuits Syst I: Regul Pap"},{"key":"348_CR16","doi-asserted-by":"crossref","unstructured":"Bianco A, de\u00a0Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: 15th Conference foundations of software technology and theoretical computer science, lecture notes in computer science. Springer, Berlin, vol 1026, pp 499\u2013513","DOI":"10.1007\/3-540-60692-0_70"},{"key":"348_CR17","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil T, Chatterjee K, Chmel\u00edk M, Forejt V, K\u0159et\u00ednsk\u00fd J, Kwiatkowska M, Parker D, Ujma M (2014) Verification of markov decision processes using learning algorithms. In: Automated technology for verification and analysis. Springer, Cham, pp 98\u2013114","DOI":"10.1007\/978-3-319-11936-6_8"},{"issue":"8","key":"348_CR18","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"100","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for boolean function manipulation. EEE Trans Comput 100(8):677\u2013691","journal-title":"EEE Trans Comput"},{"key":"348_CR19","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-69850-0_7","volume-title":"Value iteration","author":"K Chatterjee","year":"2008","unstructured":"Chatterjee K, Henzinger TA (2008) Value iteration. Springer, Berlin, pp 107\u2013138. https:\/\/doi.org\/10.1007\/978-3-540-69850-0_7"},{"issue":"1","key":"348_CR20","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BF00206326","volume":"1","author":"D Chaum","year":"1988","unstructured":"Chaum D (1988) The dining cryptographers problem: Unconditional sender and recipient untraceability. J Cryptol 1(1):65\u201375","journal-title":"J Cryptol"},{"key":"348_CR21","doi-asserted-by":"crossref","unstructured":"Daws C (2004) Symbolic and parametric model checking of discrete-time Markov chains. In: International Colloquium on theoretical aspects of computing. Springer, Berlin, pp 280\u2013294","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"348_CR22","doi-asserted-by":"crossref","unstructured":"Dehnert C, Junges S, Katoen JP, Volk M (2017) A storm is coming: A modern probabilistic model checker. In: 29th international conference computer aided verification CAV 2017","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"348_CR23","doi-asserted-by":"crossref","unstructured":"Dehnert C, Junges S, Jansen N, Corzilius F, Volk M, Bruintjes H, Katoen JP, Abraham E (2015) Prophesy: a probabilistic parameter synthesis tool. In: International conference on computer aided verification, CAV","DOI":"10.1007\/978-3-319-21690-4_13"},{"key":"348_CR24","doi-asserted-by":"crossref","unstructured":"van Dijk T, van\u00a0de Pol J (2015) Sylvan: Multi-core decision diagrams. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 677\u2013691","DOI":"10.1007\/978-3-662-46681-0_60"},{"key":"348_CR25","doi-asserted-by":"crossref","unstructured":"Dijkstra EW (1982) Self-stabilization in spite of distributed control. In: Selected writings on computing: a personal perspective. Springer, Berlin","DOI":"10.1007\/978-1-4612-5695-3"},{"issue":"6","key":"348_CR26","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1007\/s10009-006-0014-x","volume":"8","author":"M Duflot","year":"2006","unstructured":"Duflot M, Kwiatkowska M, Norman G, Parker D (2006) A formal analysis of bluetooth device discovery. Int J Softw Tools Technol Transf (STTT) 8(6):621\u2013632","journal-title":"Int J Softw Tools Technol Transf (STTT)"},{"key":"348_CR27","doi-asserted-by":"crossref","unstructured":"Forejt V, Kwiatkowska M, Norman G, Parker D (2011a) Automated verification techniques for probabilistic systems. In: International school on formal methods for the design of computer, communication and software systems. Springer, Berlin, pp 53\u2013113","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"348_CR28","doi-asserted-by":"crossref","unstructured":"Forejt V, Kwiatkowska MZ, Norman G, Parker D (2011b) Automated verification techniques for probabilistic systems. In: Formal methods for eternal networked software systems\u201411th international school on formal methods for the design of computer, communication and software systems, SFM, pp 53\u2013113","DOI":"10.1007\/978-3-642-21455-4_3"},{"issue":"2\u20133","key":"348_CR29","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M Fujita","year":"1997","unstructured":"Fujita M, McGeer PC, Yang JY (1997) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Formal Methods Syst Des 10(2\u20133):149\u2013169","journal-title":"Formal Methods Syst Des"},{"key":"348_CR30","doi-asserted-by":"crossref","unstructured":"Giro S (2012) Efficient computation of exact solutions for quantitative model checking. In: Proceedings of 10th workshop on quantitative aspects of programming languages (QAPL\u201912)","DOI":"10.4204\/EPTCS.85.2"},{"key":"348_CR31","doi-asserted-by":"crossref","unstructured":"Haddad S, Monmege B (2014) Reachability in MDPS: refining convergence of value iteration. In: International workshop on reachability problems. Springer, Berlin, pp 125\u2013137","DOI":"10.1007\/978-3-319-11439-2_10"},{"key":"348_CR32","doi-asserted-by":"crossref","unstructured":"Hahn EM, Hermanns H, Wachter B, Zhang L (2010) PARAM: a model checker for parametric Markov models. In: International conference on computer aided verification (CAV\u201910)","DOI":"10.1007\/978-3-642-14295-6_56"},{"key":"348_CR33","doi-asserted-by":"crossref","unstructured":"Hahn EM, Han T, Zhang L (2011a) Synthesis for PCTL in parametric Markov decision processes. In: NASA formal methods symposium. Springer, Berlin, pp 146\u2013161","DOI":"10.1007\/978-3-642-20398-5_12"},{"issue":"1","key":"348_CR34","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn EM, Hermanns H, Zhang L (2011b) Probabilistic reachability for parametric Markov models. Int J Softw Tools Technol Transf 13(1):3\u201319","journal-title":"Int J Softw Tools Technol Transf"},{"key":"348_CR35","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1016\/j.microrel.2010.07.154","volume":"51","author":"J Han","year":"2011","unstructured":"Han J, Chen H, Boykin E, Fortes J (2011) Reliability evaluation of logic circuits using probabilistic gate models. Microelectron Reliab 51:468\u2013476","journal-title":"Microelectron Reliab"},{"key":"348_CR36","unstructured":"Hoey J, St-Aubin R, Hu A, Boutilier C (1999) Spudd: Stochastic planning using decision diagrams. In: Proceedings of the fifteenth conference on uncertainty in artificial intelligence"},{"key":"348_CR37","volume-title":"Introduction to automata theory, languages, and computation","author":"JE Hopcroft","year":"2008","unstructured":"Hopcroft JE (2008) Introduction to automata theory, languages, and computation. Pearson Education India, Delhi"},{"key":"348_CR38","unstructured":"Jeannet B, D\u2019Argenio P, Larsen K (2002) Rapture: a tool for verifying Markov decision processes. In: Proceeding of tools day, affiliated to 13th international conference concurrency theory (CONCUR\u201902)"},{"key":"348_CR39","doi-asserted-by":"crossref","unstructured":"Katoen JP, Khattri M, Zapreevt I (2005) A Markov reward model checker. In: Second international conference on the quantitative evaluation of systems (QEST\u201905), IEEE","DOI":"10.1109\/QEST.2005.2"},{"issue":"1","key":"348_CR40","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/S0020-0190(02)00455-6","volume":"86","author":"S Kwek","year":"2003","unstructured":"Kwek S, Mehlhorn K (2003) Optimal search for rationals. Inf Process Lett 86(1):23\u201326","journal-title":"Inf Process Lett"},{"key":"348_CR41","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Sproston J (2002) Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Proceedings of 2nd joint international workshop on process algebra and probabilistic methods, performance modeling and verification (PAPM\/PROBMIV\u201902)","DOI":"10.1007\/3-540-45605-8_11"},{"issue":"3","key":"348_CR42","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s001650300007","volume":"14","author":"M Kwiatkowska","year":"2003","unstructured":"Kwiatkowska M, Norman G, Sproston J (2003) Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Formal Aspects Comput 14(3):295\u2013318","journal-title":"Formal Aspects Comput"},{"key":"348_CR43","unstructured":"Kwiatkowska M, Norman G, Parker D (2004) Controller dependability analysis by probabilistic model checking. In: 11th IFAC symposium on information control problems in manufacturing (INCOM\u201904)"},{"key":"348_CR44","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: verification of probabilistic real-time systems. In: International conference on computer aided verification. Springer, Berlin, pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"348_CR45","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"KL McMillan","year":"1993","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer Academic Publishers, Norwell"},{"key":"348_CR46","doi-asserted-by":"crossref","unstructured":"Mohyuddin N, Pakbaznia E, Pedram M (2011) Probabilistic error propagation in a logic circuit using the Boolean difference calculus. In: Advanced techniques in logic synthesis, optimizations and applications. Springer, Berlin, pp 359\u2013381","DOI":"10.1007\/978-1-4419-7518-8_19"},{"key":"348_CR47","doi-asserted-by":"publisher","first-page":"1629","DOI":"10.1109\/TCAD.2005.852033","volume":"24","author":"G Norman","year":"2005","unstructured":"Norman G, Parker D, Kwiatkowska M, Shukla S (2005) Evaluating the reliability of NAND multiplexing with PRISM. IEEE Trans Comput-Aided Des Integr Circuits Syst 24:1629\u20131637","journal-title":"IEEE Trans Comput-Aided Des Integr Circuits Syst"},{"key":"348_CR48","unstructured":"Parker D (2002) Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham"},{"key":"348_CR49","doi-asserted-by":"publisher","first-page":"1200","DOI":"10.1109\/43.952737","volume":"20","author":"Q Qiu","year":"2001","unstructured":"Qiu Q, Qu Q, Pedram M (2001) Stochastic modeling of a power-managed system-construction and optimization. IEEE Trans Comput-Aided Des Integr Circuits Syst 20:1200\u20131217","journal-title":"IEEE Trans Comput-Aided Des Integr Circuits Syst"},{"key":"348_CR50","doi-asserted-by":"crossref","unstructured":"Rabin M (1983) Randomized Byzantine generals. In: Proceedings of symposium on foundations of computer science, pp 403\u2013409","DOI":"10.1109\/SFCS.1983.48"},{"key":"348_CR51","volume-title":"CRM monograph series","author":"J Rutten","year":"2004","unstructured":"Rutten J, Kwiatkowska M, Norman G, Parker D (2004a) Mathematical techniques for analyzing concurrent and probabilistic systems. In: Panangaden P, van Breugel F (eds) CRM monograph series, vol 23. American Mathematical Society, Providence"},{"key":"348_CR52","doi-asserted-by":"publisher","DOI":"10.1090\/crmm\/023","volume-title":"Mathematical techniques for analyzing concurrent and probabilistic systems","author":"JJ Rutten","year":"2004","unstructured":"Rutten JJ, Kwiatkowska M, Norman G, Parker D (2004b) Mathematical techniques for analyzing concurrent and probabilistic systems. American Mathematical Society, Providence"},{"key":"348_CR53","unstructured":"St-Aubin R, Hoey J, Boutilier C (2001) APRICODD: approximate policy construction using decision diagrams. In: Advances in neural information processing systems, pp 1089\u20131095"},{"key":"348_CR54","doi-asserted-by":"crossref","unstructured":"Wimmer R, Kortus A, Herbstritt M, Becker B (2008) Probabilistic model checking and reliability of results. In: 11th IEEE workshop on design and diagnostics of electronic circuits and systems, 2008. DDECS, IEEE, pp 1\u20136","DOI":"10.1109\/DDECS.2008.4538787"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00348-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00348-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00348-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,5]],"date-time":"2022-11-05T02:24:10Z","timestamp":1667615050000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00348-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,29]]},"references-count":54,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["348"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00348-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,7,29]]},"assertion":[{"value":"29 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}