{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:16:16Z","timestamp":1783545376237,"version":"3.55.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>This tutorial paper presents a hands-on perspective on probabilistic model checking with the Storm model checker. Storm is a decade-old model checker that excels in performance and a rich Python-based ecosystem, which makes it easy to integrate in various workflows. This tutorial focuses on Markov decision processes (MDP), which are popular in a variety of fields. It demonstrates the basic workflow, from Python-based modeling, model checking with a variety of properties, to the extraction of policies. Further, it showcases the support for recent topics that focus on different types of uncertainty, such as interval MDP and POMDP, and the ability to quickly implement simple algorithms on top of existing data structures.<\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_25","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:21:33Z","timestamp":1779024093000},"page":"524-549","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Probabilistic Model Checking Taken by\u00a0Storm"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3810-4185","authenticated-orcid":false,"given":"Matthias","family":"Volk","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4774-7609","authenticated-orcid":false,"given":"Linus","family":"Heck","sequence":"additional","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-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2843-5511","authenticated-orcid":false,"given":"Tim","family":"Quatmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"856","DOI":"10.1007\/978-3-030-81685-8_40","volume-title":"Computer Aided Verification","author":"R Andriushchenko","year":"2021","unstructured":"Andriushchenko, R., \u010ce\u0161ka, M., Junges, S., Katoen, J.-P., Stupinsk\u00fd, \u0160: PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 856\u2013869. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_40"},{"key":"25_CR2","doi-asserted-by":"publisher","unstructured":"Andriushchenko, R., Ceska, M., Junges, S., Mac\u00e1k, F.: Small decision trees for MDPs with deductive synthesis. In: CAV (2). LNCS, vol. 15932, pp. 169\u2013192. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98679-6_8","DOI":"10.1007\/978-3-031-98679-6_8"},{"key":"25_CR3","doi-asserted-by":"publisher","unstructured":"Ashok, P., Jackermeier, M., K\u0159et\u00ednsk\u00fd, J., Weinhuber, C., Weininger, M., Yadav, M.: dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts. In: CAV 2021. LNCS, vol. 12759, pp. 326\u2013345. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_17","DOI":"10.1007\/978-3-030-72013-1_17"},{"issue":"3","key":"25_CR4","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/S10009-023-00704-3","volume":"25","author":"T Badings","year":"2023","unstructured":"Badings, T., Sim\u00e3o, T.D., Suilen, M., Jansen, N.: Decision-making under uncertainty: beyond probabilities. Int. J. Softw. Tools Technol. Transf. 25(3), 375\u2013391 (2023). https:\/\/doi.org\/10.1007\/S10009-023-00704-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"25_CR5","doi-asserted-by":"publisher","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model Checking Probabilistic Systems. In: CAV 2021. LNCS, vol. 12759, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"25_CR6","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"issue":"10","key":"25_CR7","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.P.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Software Eng. 32(10), 812\u2013830 (2006). https:\/\/doi.org\/10.1109\/TSE.2006.104","journal-title":"IEEE Trans. Software Eng."},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-662-54580-5_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2017","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: Quantitative Model and Tool Interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151\u2013168. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-030-83723-5_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends","author":"CE Budde","year":"2021","unstructured":"Budde, C.E., Hartmanns, A., Klauck, M., K\u0159et\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Turrini, A., Zhang, Z.: On Correctness, Precision, and Performance in Quantitative Verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12479, pp. 216\u2013241. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_15"},{"key":"25_CR10","unstructured":"Ceska, M., Junges, S., van der Maas, L., Mac\u00e1k, F., Quatmann, T.: Fast computation of conditional probabilities in MDPs and Markov chain families (2026). submitted"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated Verification Techniques for Probabilistic Systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53\u2013113. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_3"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: A Web-Based Probabilistic Model Checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22"},{"key":"25_CR13","doi-asserted-by":"publisher","unstructured":"Hartmanns, A.: An overview of Modest models and tools for real stochastic timed systems. In: MARS. EPTCS 355, pp. 1\u201312 (2022). https:\/\/doi.org\/10.4204\/EPTCS.355.1","DOI":"10.4204\/EPTCS.355.1"},{"key":"25_CR14","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"},{"issue":"7","key":"25_CR15","doi-asserted-by":"publisher","first-page":"1483","DOI":"10.1007\/S10817-020-09574-9","volume":"64","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Junges, S., Katoen, J.P., Quatmann, T.: Multi-cost bounded tradeoff analysis in MDP. J. Autom. Reason. 64(7), 1483\u20131522 (2020). https:\/\/doi.org\/10.1007\/S10817-020-09574-9","journal-title":"J. Autom. Reason."},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner\u2019s guide to MDP model checking algorithms. In: TACAS (1). Lecture Notes in Computer Science, vol. 13993, pp. 469\u2013488. Springer (2023). doi: 10.1007\/978-3-031-30823-9_24","DOI":"10.1007\/978-3-031-30823-9_24"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-030-53291-8_26","volume-title":"Computer Aided Verification","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic Value Iteration. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 488\u2013511. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26"},{"issue":"4","key":"25_CR18","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/S10009-021-00633-Z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/S10009-021-00633-Z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Hensel, C., Junges, S., Quatmann, T., Volk, M.: Riding the Storm in a probabilistic model checking landscape. In: Principles of Verification (2). Lecture Notes in Computer Science, vol. 15261, pp. 98\u2013114. Springer (2024). doi: 10.1007\/978-3-031-75775-4_5","DOI":"10.1007\/978-3-031-75775-4_5"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-46419-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: A Markov Chain Model Checker. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 347\u2013362. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46419-0_24"},{"issue":"2","key":"25_CR21","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1287\/MOOR.1040.0129","volume":"30","author":"GN Iyengar","year":"2005","unstructured":"Iyengar, G.N.: Robust dynamic programming. Math. Oper. Res. 30(2), 257\u2013280 (2005). https:\/\/doi.org\/10.1287\/MOOR.1040.0129","journal-title":"Math. Oper. Res."},{"issue":"1","key":"25_CR22","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/S10703-023-00442-X","volume":"62","author":"S Junges","year":"2024","unstructured":"Junges, S., et al.: Parameter synthesis for Markov models: covering the parameter space. Formal Methods Syst. Des. 62(1), 181\u2013259 (2024). https:\/\/doi.org\/10.1007\/S10703-023-00442-X","journal-title":"Formal Methods Syst. Des."},{"key":"25_CR23","doi-asserted-by":"publisher","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: LICS, pp. 31\u201345. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934574","DOI":"10.1145\/2933575.2934574"},{"issue":"2","key":"25_CR24","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. Evaluation 68(2), 90\u2013104 (2011). https:\/\/doi.org\/10.1016\/J.PEVA.2010.04.001","journal-title":"Perform. Evaluation"},{"key":"25_CR25","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1146\/annurev-control-042820-010947","volume":"5","author":"M Kwiatkowska","year":"2022","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking and autonomy. Annu. Rev. Control. Robotics Auton. Syst. 5, 385\u2013410 (2022)","journal-title":"Annu. Rev. Control. Robotics Auton. Syst."},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking: Applications and trends. In: Principles of Formal Quantitative Analysis. Lecture Notes in Computer Science, vol. 15760, pp. 158\u2013173. Springer (2025). doi: 10.1007\/978-3-031-97439-7_7","DOI":"10.1007\/978-3-031-97439-7_7"},{"issue":"2","key":"25_CR27","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/S10009-004-0140-2","volume":"6","author":"MZ Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. Int. J. Softw. Tools Technol. Transf. 6(2), 128\u2013142 (2004). https:\/\/doi.org\/10.1007\/S10009-004-0140-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"25_CR28","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"},{"issue":"1\u20132","key":"25_CR29","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/S100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997). https:\/\/doi.org\/10.1007\/S100090050010","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"25_CR30","unstructured":"Leerkes, P., Melse, I., Heck, L., Volk, M., Junges, S.: Stormvogel: probabilistic model checking for almost everyone (2025). https:\/\/repository.ubn.ru.nl\/handle\/2066\/325553"},{"issue":"1\u20132","key":"25_CR31","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). https:\/\/doi.org\/10.1016\/S0004-3702(02)00378-8","journal-title":"Artif. Intell."},{"key":"25_CR32","doi-asserted-by":"publisher","unstructured":"Meggendorfer, T.: PET - A partial exploration tool for probabilistic verification. ATVA. Lecture Notes in Computer Science 13505, 320\u2013326 (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_20. Springer","DOI":"10.1007\/978-3-031-19992-9_20"},{"key":"25_CR33","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics (1994). Wiley. https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"25_CR34","unstructured":"Quatmann, T.: Verification of multi-objective Markov models. Ph.D. thesis, RWTH Aachen University, Germany (2023). https:\/\/publications.rwth-aachen.de\/record\/971553"},{"key":"25_CR35","doi-asserted-by":"publisher","unstructured":"Spaan, M.T.J.: Partially observable Markov decision processes. In: Reinforcement Learning, Adaptation, Learning, and Optimization, vol. 12, pp. 387\u2013414. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-27645-3_12","DOI":"10.1007\/978-3-642-27645-3_12"},{"key":"25_CR36","unstructured":"Volk, M., Heck, L., Junges, S., Katoen, J.P., Quatmann, T.: Probabilistic model checking taken by storm. CoRR abs\/2603.15559 (2026). https:\/\/arxiv.org\/abs\/2603.15559"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:30:47Z","timestamp":1783542647000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_25"}},"subtitle":["A Tutorial on the Probabilistic Model Checker Storm"],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The models and Jupyter notebooks of this tutorial are publicly available in the artifact at\n                      \n                      .","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data availability"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}