{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:12Z","timestamp":1784837772354,"version":"3.55.0"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816872","type":"print"},{"value":"9783030816889","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We revisit the symbolic verification of Markov chains with respect to finite horizon reachability properties. The prevalent approach iteratively computes step-bounded state reachability probabilities. By contrast, recent advances in probabilistic inference suggest symbolically representing all horizon-length paths through the Markov chain. We ask whether this perspective advances the state-of-the-art in probabilistic model checking. First, we formally describe both approaches in order to highlight their key differences. Then, using these insights we develop<jats:sc>Rubicon<\/jats:sc>, a tool that transpiles<jats:sc>Prism<\/jats:sc>models to the probabilistic inference tool . Finally, we demonstrate better scalability compared to probabilistic model checkers on selected benchmarks. All together, our results suggest that probabilistic inference is a valuable addition to the probabilistic model checking portfolio, with<jats:sc>Rubicon<\/jats:sc>as a first step towards integrating both perspectives.<\/jats:p>","DOI":"10.1007\/978-3-030-81688-9_27","type":"book-chapter","created":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:20:47Z","timestamp":1626452447000},"page":"577-601","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Model Checking Finite-Horizon Markov Chains with Probabilistic Inference"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8190-5412","authenticated-orcid":false,"given":"Steven","family":"Holtzen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1248-0000","authenticated-orcid":false,"given":"Marcell","family":"Vazquez-Chanlatte","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2031-1514","authenticated-orcid":false,"given":"Todd","family":"Millstein","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6190-8707","authenticated-orcid":false,"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3434-2503","authenticated-orcid":false,"given":"Guy","family":"Van den Broeck","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Aflaki, S., Volk, M., Bonakdarpour, B., Katoen, J.P., Storjohann, A.: Automated fine tuning of probabilistic self-stabilizing algorithms. In: SRDS, pp. 94\u2013103. IEEE (2017)","DOI":"10.1109\/SRDS.2017.22"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Alfaro","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 395\u2013410. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46419-0_27"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-78800-3_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"ME Andr\u00e9s","year":"2008","unstructured":"Andr\u00e9s, M.E., van Rossum, P.: Conditional probabilities over probabilistic and nondeterministic systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 157\u2013172. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_12"},{"key":"27_CR4","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1007\/978-3-319-10575-8_28","volume-title":"Handbook of Model Checking","author":"C Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"key":"27_CR5","doi-asserted-by":"publisher","first-page":"104504","DOI":"10.1016\/j.ic.2019.104504","volume":"272","author":"C Baier","year":"2020","unstructured":"Baier, C., Hensel, C., Hutschenreiter, L., Junges, S., Katoen, J.P., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. Inf. Comput. 272, 104504 (2020)","journal-title":"Inf. Comput."},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-63166-6_14","volume-title":"Computer Aided Verification","author":"C Baier","year":"1997","unstructured":"Baier, C., Hermanns, H.: Weak bisimulation for fully probabilistic processes. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 119\u2013130. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_14"},{"key":"27_CR7","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-642-54862-8_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Baier","year":"2014","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., M\u00e4rcker, S.: Computing conditional probabilities in Markovian models efficiently. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 515\u2013530. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_43"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Baluta, T., Shen, S., Shinde, S., Meel, K.S., Saxena, P.: Quantitative verification of neural networks and its security applications. In: CCS, pp. 1249\u20131264. ACM (2019)","DOI":"10.1145\/3319535.3354245"},{"key":"27_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-319-89884-1_7","volume-title":"Programming Languages and Systems","author":"K Batz","year":"2018","unstructured":"Batz, K., Kaminski, B.L., Katoen, J.-P., Matheja, C.: How long, O Bayesian network, will I sample thee? - a program analysis perspective on expected sampling times. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 186\u2013213. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_7"},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., et al.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Budde, C.E., et al.: On correctness, precision, and performance in quantitative verification: QComp 2020 competition report. In: ISOLA. LNCS. Springer, Heidelberg (2020)","DOI":"10.1007\/978-3-030-83723-5_15"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Carpenter, B., et al.: Stan: a probabilistic programming language. J. Stat. Soft. VV(Ii) (2016)","DOI":"10.18637\/jss.v076.i01"},{"key":"27_CR14","unstructured":"Chakraborty, S., Fried, D., Meel, K.S., Vardi, M.Y.: From weighted to unweighted model counting. In: IJCAI, pp. 689\u2013695. AAAI Press (2015)"},{"key":"27_CR15","unstructured":"Chavira, M., Darwiche, A.: Compiling Bayesian networks using variable elimination. In: IJCAI, pp. 2443\u20132449 (2007)"},{"issue":"6\u20137","key":"27_CR16","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1016\/j.artint.2007.11.002","volume":"172","author":"M Chavira","year":"2008","unstructured":"Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artif. Intell. 172(6\u20137), 772\u2013799 (2008)","journal-title":"Artif. Intell."},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M.Z., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: TASE, pp. 85\u201392. IEEE (2013)","DOI":"10.1109\/TASE.2013.20"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Claret, G., Rajamani, S.K., Nori, A.V., Gordon, A.D., Borgstr\u00f6m, J.: Bayesian inference using data flow analysis. In: FSE, pp. 92\u2013102 (2013)","DOI":"10.1145\/2491411.2491423"},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Scenario-based verification of uncertain MDPs. In: TACAS. LNCS, vol. 12078, pp. 287\u2013305. Springer, Heidelberg (2020)","DOI":"10.1007\/978-3-030-45190-5_16"},{"key":"27_CR20","unstructured":"Darwiche, A.: SDD: a new canonical representation of propositional knowledge bases. In: IJCAI, pp. 819\u2013826 (2011)"},{"key":"27_CR21","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. JAIR 17, 229\u2013264 (2002)","journal-title":"JAIR"},{"key":"27_CR22","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. 3407, pp. 280\u2013294. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_21"},{"key":"27_CR23","unstructured":"De Raedt, L., Kimmig, A., Toivonen, H.: ProbLog: a probabilistic prolog and its application in link discovery. In: IJCAI, vol. 7, pp. 2462\u20132467 (2007)"},{"key":"27_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., et al.: PROPhESY: a PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_13"},{"key":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1007\/978-3-319-46520-3_28","volume-title":"Automated Technology for Verification and Analysis","author":"D Deininger","year":"2016","unstructured":"Deininger, D., Dimitrova, R., Majumdar, R.: Symbolic model checking for factored probabilistic models. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 444\u2013460. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_28"},{"issue":"2","key":"27_CR26","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/s10009-017-0468-z","volume":"20","author":"T van Dijk","year":"2018","unstructured":"van Dijk, T., van de Pol, J.: Multi-core symbolic bisimulation minimisation. STTT 20(2), 157\u2013177 (2018)","journal-title":"STTT"},{"issue":"3","key":"27_CR27","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1017\/S1471068414000076","volume":"15","author":"D Fierens","year":"2015","unstructured":"Fierens, D., et al.: Inference and learning in probabilistic logic programs using weighted Boolean formulas. Theory Pract. Log. Prog. 15(3), 358\u2013401 (2015)","journal-title":"Theory Pract. Log. Prog."},{"key":"27_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-540-78929-1_13","volume-title":"Hybrid Systems: Computation and Control","author":"M Fr\u00e4nzle","year":"2008","unstructured":"Fr\u00e4nzle, M., Hermanns, H., Teige, T.: Stochastic satisfiability modulo theory: a novel technique for the analysis of probabilistic hybrid systems. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 172\u2013186. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78929-1_13"},{"key":"27_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-41528-4_4","volume-title":"Computer Aided Verification","author":"T Gehr","year":"2016","unstructured":"Gehr, T., Misailovic, S., Vechev, M.: PSI: exact symbolic inference for probabilistic programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 62\u201383. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_4"},{"key":"27_CR30","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: FOSE, pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"27_CR31","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.peva.2013.11.004","volume":"73","author":"F Gretz","year":"2014","unstructured":"Gretz, F., Katoen, J.P., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110\u2013132 (2014)","journal-title":"Perform. Eval."},{"key":"27_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-12002-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PASS: abstraction refinement for infinite probabilistic models. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 353\u2013357. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_30"},{"issue":"1","key":"27_CR33","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13(1), 3\u201319 (2011)","journal-title":"STTT"},{"key":"27_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51"},{"key":"27_CR35","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: TACAS. LNCS, vol. 11427, pp. 344\u2013350. Springer, Heidelberg (2019)","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"27_CR36","doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker storm. STTT (2021, to appear)","DOI":"10.1007\/s10009-021-00633-z"},{"issue":"2","key":"27_CR37","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T Herman","year":"1990","unstructured":"Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63\u201367 (1990)","journal-title":"Inf. Process. Lett."},{"key":"27_CR38","doi-asserted-by":"crossref","unstructured":"Holtzen, S., Junges, S., Vazquez-Chanlatte, M., Millstein, T., Seshia, S.A., Van den Broeck, G.: Model checking finite-horizon Markov chains with probabilistic inference. CoRR abs\/2105.12326 (2021)","DOI":"10.1007\/978-3-030-81688-9_27"},{"key":"27_CR39","doi-asserted-by":"crossref","unstructured":"Holtzen, S., Van den Broeck, G., Millstein, T.: Scaling exact inference for discrete probabilistic programs. PACMPL OOPSLA, November 2020","DOI":"10.1145\/3428208"},{"key":"27_CR40","unstructured":"Jansen, D.N., Groote, J.F., Timmers, F., Yang, P.: A near-linear-time algorithm for weak bisimilarity on Markov chains. In: CONCUR. LIPIcs, vol. 171, pp. 8:1\u20138:20. Schloss Dagstuhl - LZI (2020)"},{"key":"27_CR41","unstructured":"Junges, S., et al.: Finite-state controllers of POMDPs using parameter synthesis. In: UAI, pp. 519\u2013529. AUAI Press (2018)"},{"key":"27_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-23506-6_4","volume-title":"Correct System Design","author":"J-P Katoen","year":"2015","unstructured":"Katoen, J.-P., Gretz, F., Jansen, N., Kaminski, B.L., Olmedo, F.: Understanding probabilistic programs. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 15\u201332. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23506-6_4"},{"key":"27_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-71209-1_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J-P Katoen","year":"2007","unstructured":"Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87\u2013101. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_9"},{"issue":"3","key":"27_CR44","first-page":"246","volume":"36","author":"M Kattenbelt","year":"2010","unstructured":"Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. FMSD 36(3), 246\u2013280 (2010)","journal-title":"FMSD"},{"key":"27_CR45","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1613\/jair.1.11595","volume":"68","author":"M Klauck","year":"2020","unstructured":"Klauck, M., Steinmetz, M., Hoffmann, J., Hermanns, H.: Bridging the gap between probabilistic model checking and probabilistic planning: survey, compilations, and empirical comparison. JAIR 68, 247\u2013310 (2020)","journal-title":"JAIR"},{"issue":"2","key":"27_CR46","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10009-017-0456-3","volume":"20","author":"J Klein","year":"2018","unstructured":"Klein, J., et al.: Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic b\u00fcchi automata. STTT 20(2), 179\u2013194 (2018)","journal-title":"STTT"},{"key":"27_CR47","volume-title":"Probabilistic Graphical Models: Principles and Techniques","author":"D Koller","year":"2009","unstructured":"Koller, D., Friedman, N.: Probabilistic Graphical Models: Principles and Techniques. MIT Press, Cambridge (2009)"},{"issue":"3","key":"27_CR48","first-page":"328","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. JCSS 22(3), 328\u2013350 (1981)","journal-title":"JCSS"},{"key":"27_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 52\u201366. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_5"},{"key":"27_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/11817963_23","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 234\u2013248. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_23"},{"key":"27_CR51","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. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"27_CR52","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: QEST, pp. 203\u2013204. IEEE (2012)","DOI":"10.1109\/QEST.2012.14"},{"issue":"4\u20136","key":"27_CR53","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/s00165-012-0227-6","volume":"24","author":"MZ Kwiatkowska","year":"2012","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic verification of Herman\u2019s self-stabilisation algorithm. Formal Aspects Comput. 24(4\u20136), 661\u2013670 (2012)","journal-title":"Formal Aspects Comput."},{"key":"27_CR54","doi-asserted-by":"crossref","unstructured":"Pearl, J.: Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference. Morgan Kaufmann (1988)","DOI":"10.1016\/B978-0-08-051489-5.50008-4"},{"key":"27_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-319-10696-0_30","volume-title":"Quantitative Evaluation of Systems","author":"MN Rabe","year":"2014","unstructured":"Rabe, M.N., Wintersteiger, C.M., Kugler, H., Yordanov, B., Hamadi, Y.: Symbolic approximation of the bounded reachability probability in large Markov chains. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 388\u2013403. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10696-0_30"},{"key":"27_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-030-59854-9_9","volume-title":"Quantitative Evaluation of Systems","author":"B Salmani","year":"2020","unstructured":"Salmani, B., Katoen, J.-P.: Bayesian inference by symbolic model checking. In: Gribaudo, M., Jansen, D.N., Remke, A. (eds.) QEST 2020. LNCS, vol. 12289, pp. 115\u2013133. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59854-9_9"},{"key":"27_CR57","unstructured":"Sang, T., Beame, P., Kautz, H.A.: Performing Bayesian inference by weighted model counting. In: AAAI, vol. 5, pp. 475\u2013481 (2005)"},{"key":"27_CR58","doi-asserted-by":"crossref","unstructured":"Smolka, S., et al.: Scalable verification of probabilistic networks. In: PLDI, pp. 190\u2013203. ACM (2019)","DOI":"10.1145\/3314221.3314639"},{"key":"27_CR59","unstructured":"van de Meent, J.W., Paige, B., Yang, H., Wood, F.: An Introduction to Probabilistic Programming. arXiv:1809.10756 (2018)"},{"key":"27_CR60","unstructured":"Vazquez-Chanlatte, M., Rabe, M.N., Seshia, S.A.: A model counter\u2019s guide to probabilistic systems. CoRR abs\/1903.09354 (2019)"},{"key":"27_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-030-53291-8_15","volume-title":"Computer Aided Verification","author":"M Vazquez-Chanlatte","year":"2020","unstructured":"Vazquez-Chanlatte, M., Seshia, S.A.: Maximum causal entropy specification inference from demonstrations. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 255\u2013278. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_15"},{"key":"27_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-540-93900-9_29","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Wimmer","year":"2008","unstructured":"Wimmer, R., Braitling, B., Becker, B.: Counterexample generation for discrete-time Markov chains using bounded model checking. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 366\u2013380. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-93900-9_29"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81688-9_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,4]],"date-time":"2023-01-04T17:48:01Z","timestamp":1672854481000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81688-9_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816872","9783030816889"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81688-9_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}