{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T10:55:12Z","timestamp":1785322512232,"version":"3.55.0"},"reference-count":125,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,7,6]],"date-time":"2021-07-06T00:00:00Z","timestamp":1625529600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,6]],"date-time":"2021-07-06T00:00:00Z","timestamp":1625529600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100007210","name":"RWTH Aachen University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100007210","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present the probabilistic model checker <jats:sc>Storm<\/jats:sc>. <jats:sc>Storm<\/jats:sc> supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. <jats:sc>Storm<\/jats:sc> has three major distinguishing features. It supports multiple input languages for Markov models, including the <jats:sc>Jani<\/jats:sc> and <jats:sc>Prism<\/jats:sc> modeling languages, dynamic fault trees, generalized stochastic Petri nets, and the probabilistic guarded command language. It has a modular setup in which solvers and symbolic engines can easily be exchanged. Its Python API allows for rapid prototyping by encapsulating <jats:sc>Storm<\/jats:sc>\u2019s fast and scalable algorithms. This paper reports on the main features of <jats:sc>Storm<\/jats:sc> and explains how to effectively use them. A description is provided of the main distinguishing functionalities of <jats:sc>Storm<\/jats:sc>. Finally, an empirical evaluation of different configurations of <jats:sc>Storm<\/jats:sc> on the QComp 2019 benchmark set is presented.\n<\/jats:p>","DOI":"10.1007\/s10009-021-00633-z","type":"journal-article","created":{"date-parts":[[2021,7,6]],"date-time":"2021-07-06T16:04:44Z","timestamp":1625587484000},"page":"589-610","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":205,"title":["The probabilistic model checker Storm"],"prefix":"10.1007","volume":"24","author":[{"given":"Christian","family":"Hensel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tim","family":"Quatmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthias","family":"Volk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,7,6]]},"reference":[{"key":"633_CR1","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J.P., Wimmer, R.: Counterexample generation for discrete-time Markov models: An introductory survey. In: SFM, LNCS, vol. 8483, pp. 65\u2013121. Springer (2014)","DOI":"10.1007\/978-3-319-07317-0_3"},{"issue":"1","key":"633_CR2","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018)","journal-title":"ACM Trans. Model. Comput. Simul."},{"issue":"1","key":"633_CR3","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/2728816.2728827","volume":"2","author":"R Alur","year":"2015","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Theory in practice for system design and verification. SIGLOG News 2(1), 46\u201351 (2015)","journal-title":"SIGLOG News"},{"issue":"3","key":"633_CR4","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10458-009-9103-z","volume":"21","author":"C Amato","year":"2010","unstructured":"Amato, C., Bernstein, D.S., Zilberstein, S.: Optimizing fixed-size stochastic controllers for POMDPs and decentralized POMDPs. Auton. Agent. Multi-Agent Syst. 21(3), 293\u2013320 (2010)","journal-title":"Auton. Agent. Multi-Agent Syst."},{"key":"633_CR5","doi-asserted-by":"crossref","unstructured":"Andova, S., Hermanns, H., Katoen, J.P.: Discrete-time rewards model-checked. In: FORMATS, LNCS, vol. 2791, pp. 88\u2013104. Springer (2003)","DOI":"10.1007\/978-3-540-40903-8_8"},{"key":"633_CR6","doi-asserted-by":"crossref","unstructured":"Ashok, P., Chatterjee, K., Daca, P., Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Value iteration for long-run average reward in Markov decision processes. In: CAV (1), LNCS, vol. 10426, pp. 201\u2013221. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_10"},{"issue":"1","key":"633_CR7","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1016\/0022-247X(65)90154-X","volume":"10","author":"K \u00c5str\u00f6m","year":"1965","unstructured":"\u00c5str\u00f6m, K.: Optimal control of Markov processes with incomplete state information. J. Math. Anal. Appl. 10(1), 174\u2013205 (1965)","journal-title":"J. Math. Anal. Appl."},{"issue":"1","key":"633_CR8","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Model-checking continous-time Markov chains. ACM Trans. Comput. Log. 1(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Log."},{"key":"633_CR9","doi-asserted-by":"crossref","unstructured":"Baier, C., de\u00a0Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"633_CR10","doi-asserted-by":"crossref","unstructured":"Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M.Z., Ryan, M.: Symbolic model checking for probabilistic processes. In: ICALP, LNCS, vol. 1256, pp. 430\u2013440. Springer (1997)","DOI":"10.1007\/3-540-63165-8_199"},{"issue":"6","key":"633_CR11","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"633_CR12","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":"633_CR13","doi-asserted-by":"crossref","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., M\u00e4rcker, S.: Computing conditional probabilities in Markovian models efficiently. In: TACAS, LNCS, vol. 8413, pp. 515\u2013530. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_43"},{"key":"633_CR14","doi-asserted-by":"crossref","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., Wunderlich, S.: Maximizing the conditional expected reward for reaching the goal. In: TACAS (2), LNCS, vol. 10206, pp. 269\u2013285 (2017)","DOI":"10.1007\/978-3-662-54580-5_16"},{"key":"633_CR15","doi-asserted-by":"crossref","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: CAV (1), LNCS, vol. 10426, pp. 160\u2013180. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_8"},{"issue":"7","key":"633_CR16","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with SLAM. Commun. ACM 54(7), 68\u201376 (2011)","journal-title":"Commun. ACM"},{"key":"633_CR17","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: Version 2.5. Tech. rep., Dep. of Computer Science, The University of Iowa (2015). www.smt-lib.org"},{"key":"633_CR18","doi-asserted-by":"crossref","unstructured":"Bauer, M.S., Mathur, U., Chadha, R., Sistla, A.P., Viswanathan, M.: Exact quantitative probabilistic model checking through rational search. In: FMCAD, pp. 92\u201399. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102246"},{"key":"633_CR19","doi-asserted-by":"crossref","unstructured":"Bork, A., Junges, S., Katoen, J., Quatmann, T.: Verification of indefinite-horizon POMDPs. CoRR abs\/2007.00102 (2020)","DOI":"10.1007\/978-3-030-59152-6_16"},{"key":"633_CR20","doi-asserted-by":"crossref","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.: A compositional semantics for dynamic fault trees in terms of interactive Markov chains. In: ATVA, LNCS, vol. 4762, pp. 441\u2013456. Springer (2007)","DOI":"10.1007\/978-3-540-75596-8_31"},{"key":"633_CR21","doi-asserted-by":"crossref","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.: Dynamic fault tree analysis using input\/output interactive Markov chains. In: DSN, pp. 708\u2013717. IEEE Computer Society (2007)","DOI":"10.1109\/DSN.2007.37"},{"issue":"5","key":"633_CR22","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","volume":"54","author":"M Bozzano","year":"2011","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. Comput. J. 54(5), 754\u2013775 (2011)","journal-title":"Comput. J."},{"key":"633_CR23","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kret\u00ednsk\u00fd, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: ATVA, LNCS, vol. 8837, pp. 98\u2013114. Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"633_CR24","unstructured":"Braziunas, D., Boutilier, C.: Stochastic local search for POMDP controllers. In: AAAI, pp. 690\u2013696. The MIT Press (2004)"},{"key":"633_CR25","doi-asserted-by":"crossref","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: TACAS (2), LNCS, vol. 10206, pp. 151\u2013168 (2017)","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"633_CR26","doi-asserted-by":"crossref","unstructured":"Budde, C.E., Hartmanns, A., Klauck, M., Kret\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Turini, A., Zhang, Z.: On correctness, precision, and performance in quantitative verification (QComp 2020 competition report). In: ISoLA, LNCS. Springer (2020). (To Appear)","DOI":"10.1007\/978-3-030-83723-5_15"},{"key":"633_CR27","doi-asserted-by":"crossref","unstructured":"Butkova, Y., Hartmanns, A., Hermanns, H.: A Modest approach to modelling and checking Markov automata. In: QEST, LNCS, vol. 11785, pp. 52\u201369. Springer (2019)","DOI":"10.1007\/978-3-030-30281-8_4"},{"key":"633_CR28","doi-asserted-by":"crossref","unstructured":"Butkova, Y., Wimmer, R., Hermanns, H.: Long-run rewards for Markov automata. In: TACAS (2), LNCS, vol. 10206, pp. 188\u2013203 (2017)","DOI":"10.1007\/978-3-662-54580-5_11"},{"key":"633_CR29","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/11880646_3","volume":"4220","author":"M Calder","year":"2006","unstructured":"Calder, M., Vyshemirsky, V., Gilbert, D.R., Orton, R.J.: Analysis of signalling pathways using continuous time Markov chains. Trans. Comput. Syst. Biol. VI LNCS 4220, 44\u201367 (2006)","journal-title":"Trans. Comput. Syst. Biol. VI LNCS"},{"key":"633_CR30","doi-asserted-by":"crossref","unstructured":"Ceska, M., Hensel, C., Junges, S., Katoen, J.P.: Counterexample-driven synthesis for probabilistic program sketches. In: FM, LNCS, vol. 11800, pp. 101\u2013120. Springer (2019)","DOI":"10.1007\/978-3-030-30942-8_8"},{"issue":"1","key":"633_CR31","doi-asserted-by":"publisher","first-page":"1:1","DOI":"10.1145\/1838552.1838553","volume":"12","author":"R Chadha","year":"2010","unstructured":"Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement framework for Markov decision processes. ACM Trans. Comput. Log. 12(1), 1:1\u20131:49 (2010)","journal-title":"ACM Trans. Comput. Log."},{"key":"633_CR32","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Chmelik, M., Davies, J.: A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. In: AAAI, pp. 3225\u20133232. AAAI Press (2016)","DOI":"10.1609\/aaai.v30i1.10422"},{"key":"633_CR33","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Qualitative analysis of partially-observable Markov decision processes. In: MFCS, LNCS, vol. 6281, pp. 258\u2013269. Springer (2010)","DOI":"10.1007\/978-3-642-15155-2_24"},{"key":"633_CR34","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 SMT solver. In: TACAS, LNCS, vol. 7795, pp. 93\u2013107. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"633_CR35","unstructured":"Condon, A.: On algorithms for simple stochastic games. In: Advances in Computational Complexity Theory. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a013, pp. 51\u201371. DIMACS\/AMS (1990)"},{"key":"633_CR36","doi-asserted-by":"crossref","unstructured":"Corzilius, F., Kremer, G., Junges, S., Schupp, S., \u00c1brah\u00e1m, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: SAT, LNCS, vol. 9340, pp. 360\u2013368. Springer (2015)","DOI":"10.1007\/978-3-319-24318-4_26"},{"key":"633_CR37","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: FOCS, pp. 338\u2013345. IEEE Computer Society (1988)","DOI":"10.1109\/SFCS.1988.21950"},{"key":"633_CR38","doi-asserted-by":"crossref","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: ICTAC, LNCS, vol. 3407, pp. 280\u2013294. Springer (2004)","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"633_CR39","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Jansen, N., Wimmer, R., \u00c1brah\u00e1m, E., Katoen, J.P.: Fast debugging of PRISM models. In: ATVA, LNCS, vol. 8837, pp. 146\u2013162. Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_11"},{"key":"633_CR40","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.P., \u00c1brah\u00e1m, E.: Prophesy: a probabilistic parameter synthesis tool. In: CAV (1), LNCS, vol. 9206, pp. 214\u2013231. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_13"},{"key":"633_CR41","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: CAV (2), LNCS, vol. 10427, pp. 592\u2013600. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"633_CR42","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Katoen, J.P., Parker, D.: SMT-based bisimulation minimisation of Markov models. In: VMCAI, LNCS, vol. 7737, pp. 28\u201347. Springer (2013)","DOI":"10.1007\/978-3-642-35873-9_5"},{"key":"633_CR43","doi-asserted-by":"crossref","unstructured":"Delgrange, F., Katoen, J., Quatmann, T., Randour, M.: Simple strategies in multi-objective MDPs. In: TACAS (1), LNCS, vol. 12078, pp. 346\u2013364. Springer (2020)","DOI":"10.1007\/978-3-030-45190-5_19"},{"key":"633_CR44","unstructured":"de\u00a0Alfaro, L.: How to specify and verify the long-run average behavior of probabilistic systems. In: LICS, pp. 454\u2013465. IEEE Computer Society (1998)"},{"key":"633_CR45","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS, LNCS, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"633_CR46","doi-asserted-by":"publisher","first-page":"2","DOI":"10.2168\/LMCS-11(2:16)2015","volume":"11","author":"K Dr\u00e4ger","year":"2015","unstructured":"Dr\u00e4ger, K., Forejt, V., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. Logical Methods Comput. Sci. 11, 2 (2015)","journal-title":"Logical Methods Comput. Sci."},{"key":"633_CR47","unstructured":"Dugan, J.B., Bavuso, S.J., Boyd, M.: Fault trees and sequence dependencies. In: Proceedings of RAMS, pp. 286\u2013293. IEEE (1990). 10.1109\/ARMS.1990.67971"},{"key":"633_CR48","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Katoen, J.P., Zhang, L.: A semantics for every GSPN. In: Petri Nets, LNCS, vol. 7927, pp. 90\u2013109. Springer (2013)","DOI":"10.1007\/978-3-642-38697-8_6"},{"key":"633_CR49","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342\u2013351. IEEE Computer Society (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"633_CR50","first-page":"4","volume":"4","author":"K Etessami","year":"2008","unstructured":"Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Logical Methods Comput. Sci. 4, 4 (2008)","journal-title":"Logical Methods Comput. Sci."},{"key":"633_CR51","doi-asserted-by":"crossref","unstructured":"Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: TACAS, LNCS, vol. 6605, pp. 112\u2013127. Springer (2011)","DOI":"10.1007\/978-3-642-19835-9_11"},{"key":"633_CR52","doi-asserted-by":"crossref","unstructured":"Forejt, V., Kwiatkowska, M.Z., Parker, D.: Pareto curves for probabilistic model checking. In: ATVA, LNCS, vol. 7561, pp. 317\u2013332. Springer (2012)","DOI":"10.1007\/978-3-642-33386-6_25"},{"key":"633_CR53","unstructured":"Fredlund, L.: The timing and probability workbench: a tool for analysing timed processes. Tech. Rep.\u00a049, Uppsala University (1994)"},{"key":"633_CR54","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.ress.2019.02.005","volume":"186","author":"M Ghadhab","year":"2019","unstructured":"Ghadhab, M., Junges, S., Katoen, J.P., Kuntz, M., Volk, M.: Safety analysis for vehicle guidance systems with dynamic fault trees. Rel. Eng. Syst. Saf. 186, 37\u201350 (2019)","journal-title":"Rel. Eng. Syst. Saf."},{"key":"633_CR55","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":"633_CR56","unstructured":"Guennebaud, G., Jacob, B., et\u00a0al.: Eigen v3. http:\/\/eigen.tuxfamily.org (2010)"},{"key":"633_CR57","unstructured":"Gurobi\u00a0Optimization, L.: Gurobi optimizer reference manual (2019). http:\/\/www.gurobi.com"},{"key":"633_CR58","doi-asserted-by":"crossref","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: RP, LNCS, vol. 8762, pp. 125\u2013137. Springer (2014)","DOI":"10.1007\/978-3-319-11439-2_10"},{"key":"633_CR59","first-page":"85","volume":"9984","author":"EM Hahn","year":"2016","unstructured":"Hahn, E.M., Hartmanns, A.: A comparison of time- and reward-bounded probabilistic model checking techniques. SETTA LNCS 9984, 85\u2013100 (2016)","journal-title":"SETTA LNCS"},{"key":"633_CR60","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Hartmanns, A., Hensel, C., Klauck, M., Klein, J., Kret\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Ruijters, E., Steinmetz, M.: The 2019 comparison of tools for the analysis of quantitative formal models- (QComp 2019 competition report). In: TACAS (3), LNCS, vol. 11429, pp. 69\u201392. Springer (2019)","DOI":"10.1007\/978-3-030-17502-3_5"},{"issue":"1","key":"633_CR61","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":"633_CR62","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: A web-based probabilistic model checker. In: FM, LNCS, vol. 8442, pp. 312\u2013317. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_22"},{"issue":"2","key":"633_CR63","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/TSE.2009.5","volume":"35","author":"T Han","year":"2009","unstructured":"Han, T., Katoen, J.P., Damman, B.: Counterexample generation in probabilistic model checking. IEEE Trans. Softw. Eng. 35(2), 241\u2013257 (2009)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"633_CR64","unstructured":"Hansen, E.A.: Solving POMDPs by searching in policy space. In: UAI, pp. 211\u2013219. Morgan Kaufmann (1998)"},{"key":"633_CR65","unstructured":"Hansson, H., Jonsson, B.: A framework for reasoning about time and reliability. In: RTSS, pp. 102\u2013111. IEEE Computer Society (1989)"},{"issue":"5","key":"633_CR66","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Asp. Comput."},{"key":"633_CR67","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: TACAS, LNCS, vol. 8413, pp. 593\u2013598. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"633_CR68","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Hermanns, H.: Explicit model checking of very large MDP using partitioning and secondary storage. In: ATVA, LNCS, vol. 9364, pp. 131\u2013147. Springer (2015)","DOI":"10.1007\/978-3-319-24953-7_10"},{"key":"633_CR69","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Junges, S., Katoen, J.P., Quatmann, T.: Multi-cost bounded reachability in MDP. In: TACAS (2), LNCS, vol. 10806, pp. 320\u2013339. Springer (2018)","DOI":"10.1007\/978-3-319-89963-3_19"},{"key":"633_CR70","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Junges, S., Katoen, J.P., Quatmann, T.: Multi-cost bounded tradeoff analysis in MDP. JAR (2020)","DOI":"10.1007\/s10817-020-09574-9"},{"key":"633_CR71","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: CAV (2), LNCS, vol. 12225, pp. 488\u2013511. Springer (2020)","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"633_CR72","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: TACAS (1), LNCS, vol. 11427, pp. 344\u2013350. Springer (2019)","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"633_CR73","doi-asserted-by":"crossref","unstructured":"Hartonas-Garmhausen, V., Campos, S.V.A., Clarke, E.M.: ProbVerus: probabilistic symbolic model checking. In: ARTS, LNCS, vol. 1601, pp. 96\u2013110. Springer (1999)","DOI":"10.1007\/3-540-48778-6_6"},{"issue":"2\u20133","key":"633_CR74","first-page":"171","volume":"28","author":"J He","year":"1997","unstructured":"He, J., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Sci. Comput. Program. 28(2\u20133), 171\u2013192 (1997)","journal-title":"Sci. Comput. Program."},{"key":"633_CR75","doi-asserted-by":"crossref","unstructured":"Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: TYPES, LNCS, vol. 806, pp. 127\u2013165. Springer (1993)","DOI":"10.1007\/3-540-58085-9_75"},{"key":"633_CR76","unstructured":"Hensel, C.: The probabilistic model checker Storm: symbolic methods for probabilistic model checking. Ph.D. thesis, RWTH Aachen University, Germany (2018)"},{"key":"633_CR77","doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker storm: evaluation results and replication package (2020). https:\/\/doi.org\/10.5281\/zenodo.3571209","DOI":"10.1007\/s10009-021-00633-z"},{"key":"633_CR78","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Katoen, J.P., Meyer-Kayser, J., Siegle, M.: A Markov chain model checker. In: TACAS, LNCS, vol. 1785, pp. 347\u2013362. Springer (2000)","DOI":"10.1007\/3-540-46419-0_24"},{"issue":"2","key":"633_CR79","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/2560217.2560218","volume":"57","author":"GJ Holzmann","year":"2014","unstructured":"Holzmann, G.J.: Mars code. Commun. ACM 57(2), 64\u201373 (2014)","journal-title":"Commun. ACM"},{"key":"633_CR80","doi-asserted-by":"crossref","unstructured":"Hor\u00e1k, K., Bosansk\u00fd, B., Chatterjee, K.: Goal-HSVI: heuristic search value iteration for goal POMDPs. In: IJCAI, pp. 4764\u20134770. ijcai.org (2018)","DOI":"10.24963\/ijcai.2018\/662"},{"key":"633_CR81","unstructured":"Junges, S., \u00c1brah\u00e1m, E., Hensel, C., Jansen, N., Katoen, J.P., Quatmann, T., Volk, M.: Parameter synthesis for Markov models. CoRR abs\/1903.07993 (2019)"},{"key":"633_CR82","doi-asserted-by":"crossref","unstructured":"Junges, S., Jansen, N., Dehnert, C., Topcu, U., Katoen, J.P.: Safety-constrained reinforcement learning for mdps. In: TACAS, LNCS, vol. 9636, pp. 130\u2013146. Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_8"},{"key":"633_CR83","doi-asserted-by":"crossref","unstructured":"Junges, S., Jansen, N., Seshia, S.A.: Enforcing almost-sure reachability in pomdps. CoRR abs\/2007.00085 (2020)","DOI":"10.1007\/978-3-030-81688-9_28"},{"key":"633_CR84","unstructured":"Junges, S., Jansen, N., Wimmer, R., Quatmann, T., Winterer, L., Katoen, J.P., Becker, B.: Finite-state controllers of POMDPs using parameter synthesis. In: UAI, pp. 519\u2013529. AUAI Press (2018)"},{"issue":"1\u20132","key":"633_CR85","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0004-3702(98)00023-X","volume":"101","author":"LP Kaelbling","year":"1998","unstructured":"Kaelbling, L.P., Littman, M.L., Cassandra, A.R.: Planning and acting in partially observable stochastic domains. Artif. Intell. 101(1\u20132), 99\u2013134 (1998)","journal-title":"Artif. Intell."},{"key":"633_CR86","doi-asserted-by":"crossref","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: LICS, pp. 31\u201345. ACM (2016)","DOI":"10.1145\/2933575.2934574"},{"key":"633_CR87","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: TACAS, LNCS, vol. 4424, pp. 87\u2013101. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_9"},{"issue":"2","key":"633_CR88","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"JP Katoen","year":"2011","unstructured":"Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"issue":"2","key":"633_CR89","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10009-017-0456-3","volume":"20","author":"J Klein","year":"2018","unstructured":"Klein, J., Baier, C., Chrszon, P., Daum, M., Dubslaff, C., Kl\u00fcppelholz, S., M\u00e4rcker, S., M\u00fcller, D.: 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"},{"issue":"1","key":"633_CR90","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.: Optimal search for rationals. Inf. Process. Lett. 86(1), 23\u201326 (2003)","journal-title":"Inf. Process. Lett."},{"key":"633_CR91","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. In: TACAS, LNCS, vol. 2280, pp. 52\u201366. Springer (2002)","DOI":"10.1007\/3-540-46002-0_5"},{"key":"633_CR92","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: QEST, pp. 157\u2013166. IEEE Computer Society (2006)"},{"key":"633_CR93","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CAV, LNCS, vol. 6806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"4\u20136","key":"633_CR94","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 Asp. Comput. 24(4\u20136), 661\u2013670 (2012)","journal-title":"Formal Asp. Comput."},{"key":"633_CR95","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM. In: CAV, LNCS, vol. 2102, pp. 194\u2013206. Springer (2001)","DOI":"10.1007\/3-540-44585-4_17"},{"issue":"1","key":"633_CR96","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s00165-006-0015-2","volume":"19","author":"R Lanotte","year":"2007","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Formal Asp. Comput. 19(1), 93\u2013109 (2007)","journal-title":"Formal Asp. Comput."},{"key":"633_CR97","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Legay, A.: Statistical model checking: past, present, and future. In: ISoLA (1), LNCS, vol. 9952, pp. 3\u201315 (2016)","DOI":"10.1007\/978-3-319-47166-2_1"},{"issue":"1","key":"633_CR98","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1287\/opre.39.1.162","volume":"39","author":"WS Lovejoy","year":"1991","unstructured":"Lovejoy, W.S.: Computationally feasible bounds for partially observed Markov decision processes. Oper. Res. 39(1), 162\u2013175 (1991)","journal-title":"Oper. Res."},{"issue":"1\u20132","key":"633_CR99","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0004-3702(02)00378-8","volume":"147","author":"O Madani","year":"2003","unstructured":"Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and related stochastic optimization problems. Artif. Intell. 147(1\u20132), 5\u201334 (2003)","journal-title":"Artif. Intell."},{"issue":"2","key":"633_CR100","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/190.191","volume":"2","author":"MA Marsan","year":"1984","unstructured":"Marsan, M.A., Conte, G., Balbo, G.: A class of generalized stochastic petri nets for the performance evaluation of multiprocessor systems. ACM Trans. Comput. Syst. 2(2), 93\u2013122 (1984)","journal-title":"ACM Trans. Comput. Syst."},{"key":"633_CR101","unstructured":"Meuleau, N., Kim, K., Kaelbling, L.P., Cassandra, A.R.: Solving POMDPs by searching the space of finite policies. In: UAI, pp. 417\u2013426. Morgan Kaufmann (1999)"},{"issue":"3","key":"633_CR102","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/s11241-017-9269-4","volume":"53","author":"G Norman","year":"2017","unstructured":"Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. Real-Time Syst. 53(3), 354\u2013402 (2017)","journal-title":"Real-Time Syst."},{"key":"633_CR103","series-title":"Cambridge Series in Statistical and Probabilistic Mathematics","volume-title":"Markov Chains","author":"JR Norris","year":"1998","unstructured":"Norris, J.R.: Markov Chains. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (1998)"},{"issue":"1","key":"633_CR104","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/3156018","volume":"40","author":"F Olmedo","year":"2018","unstructured":"Olmedo, F., Gretz, F., Jansen, N., Kaminski, B.L., Katoen, J.P., McIver, A.: Conditioning in probabilistic programming. ACM Trans. Program. Lang. Syst. 40(1), 4:1\u20134:50 (2018)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"633_CR105","unstructured":"Pajarinen, J., Peltonen, J.: Periodic finite state controllers for efficient POMDP and DEC-POMDP planning. In: NIPS, pp. 2636\u20132644 (2011)"},{"key":"633_CR106","first-page":"2825","volume":"12","author":"F Pedregosa","year":"2011","unstructured":"Pedregosa, F., Varoquaux, G., Gramfort, A., Michel, V., Thirion, B., Grisel, O., Blondel, M., Prettenhofer, P., Weiss, R., Dubourg, V., VanderPlas, J., Passos, A., Cournapeau, D., Brucher, M., Perrot, M., Duchesnay, E.: Scikit-learn: machine learning in python. J. Mach. Learn. Res. 12, 2825\u20132830 (2011)","journal-title":"J. Mach. Learn. Res."},{"key":"633_CR107","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes. Wiley, New York (1994)"},{"key":"633_CR108","first-page":"50","volume":"9938","author":"T Quatmann","year":"2016","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.P.: Parameter synthesis for Markov models: faster than ever. ATVA LNCS 9938, 50\u201367 (2016)","journal-title":"ATVA LNCS"},{"key":"633_CR109","doi-asserted-by":"crossref","unstructured":"Quatmann, T., Junges, S., Katoen, J.P.: Markov automata with multiple objectives. In: CAV (1), LNCS, vol. 10426, pp. 140\u2013159. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_7"},{"key":"633_CR110","doi-asserted-by":"crossref","unstructured":"Quatmann, T., Katoen, J.P.: Sound value iteration. In: CAV (1), LNCS, vol. 10981, pp. 643\u2013661. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"633_CR111","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.cosrev.2015.03.001","volume":"15","author":"E Ruijters","year":"2015","unstructured":"Ruijters, E., Stoelinga, M.: Fault tree analysis: a survey of the state-of-the-art in modeling, analysis and tools. Comput. Sci. Rev. 15, 29\u201362 (2015)","journal-title":"Comput. Sci. Rev."},{"issue":"2","key":"633_CR112","first-page":"250","volume":"2","author":"R Segala","year":"1995","unstructured":"Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250\u2013273 (1995)","journal-title":"Nord. J. Comput."},{"key":"633_CR113","unstructured":"Somenzi, F.: CUDD 3.0.0. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/html\/. Also available at https:\/\/github.com\/ivmai\/cudd"},{"key":"633_CR114","doi-asserted-by":"crossref","unstructured":"Spel, J., Junges, S., Katoen, J.P.: Are parametric Markov chains monotonic? In: ATVA, LNCS, vol. 11781, pp. 479\u2013496. Springer (2019)","DOI":"10.1007\/978-3-030-31784-3_28"},{"key":"633_CR115","unstructured":"Sullivan, K.J., Dugan, J.B., Coppit, D.: The galileo fault tree analysis tool. In: FTCS, pp. 232\u2013235. IEEE Computer Society (1999)"},{"key":"633_CR116","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327\u2013338. IEEE Computer Society (1985)","DOI":"10.1109\/SFCS.1985.12"},{"issue":"1","key":"633_CR117","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1109\/TII.2017.2710316","volume":"14","author":"M Volk","year":"2018","unstructured":"Volk, M., Junges, S., Katoen, J.P.: Fast dynamic fault tree analysis by model checking techniques. IEEE Trans. Ind. Inform. 14(1), 370\u2013379 (2018)","journal-title":"IEEE Trans. Ind. Inform."},{"key":"633_CR118","doi-asserted-by":"crossref","unstructured":"van Dijk, T.: Sylvan: multi-core decision diagrams. Ph.D. thesis, University of Twente, Enschede, Netherlands (2016)","DOI":"10.1007\/s10009-016-0433-2"},{"issue":"2","key":"633_CR119","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"},{"key":"633_CR120","unstructured":"Wachter, B.: Refined probabilistic abstraction. Ph.D. thesis, Saarland University (2011)"},{"key":"633_CR121","unstructured":"Wimmer, R.: Symbolische Methoden f\u00fcr die probabilistische Verifikation: Zustandsraumreduktion und Gegenbeispiele. In: Ausgezeichnete Informatikdissertationen, LNI, vol. D-12, pp. 271\u2013280. GI (2011)"},{"key":"633_CR122","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Jansen, N., Vorpahl, A., \u00c1brah\u00e1m, E., Katoen, J.P., Becker, B.: High-level counterexamples for probabilistic automata. In: QEST, LNCS, vol. 8054, pp. 39\u201354. Springer (2013)","DOI":"10.1007\/978-3-642-40196-1_4"},{"key":"633_CR123","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Kortus, A., Herbstritt, M., Becker, B.: Probabilistic model checking and reliability of results. In: DDECS, pp. 207\u2013212. IEEE Computer Society (2008)","DOI":"10.1109\/DDECS.2008.4538787"},{"key":"633_CR124","unstructured":"Winkler, T., Junges, S., P\u00e9rez, G.A., Katoen, J.: On the complexity of reachability in parametric markov decision processes. In: CONCUR, LIPIcs, vol. 140, pp. 14:1\u201314:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"633_CR125","doi-asserted-by":"crossref","unstructured":"Winterer, L., Junges, S., Wimmer, R., Jansen, N., Topcu, U., Katoen, J.P., Becker, B.: Motion planning under partial observability using game-based abstraction. In: CDC, pp. 2201\u20132208. IEEE (2017)","DOI":"10.1109\/CDC.2017.8263971"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00633-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-021-00633-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00633-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T10:07:34Z","timestamp":1659434854000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-021-00633-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,6]]},"references-count":125,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["633"],"URL":"https:\/\/doi.org\/10.1007\/s10009-021-00633-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,6]]},"assertion":[{"value":"23 June 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 July 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}