Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Riding the Storm in a Probabilistic Model Checking Landscape

  • Chapter
  • First Online:
Principles of Verification: Cycling the Probabilistic Landscape

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 15261))

  • 60 Accesses

Abstract

Probabilistic model checking is a formal verification technique to check whether stochastic models satisfy properties of interest. Along with a rich theory, the community has developed mature tool support, which in turn has been applied to a set of industrial case studies. This paper demonstrates various abilities of the probabilistic model checker Storm by a set of simple and more accessible examples.

This work was partially funded by NWO Veni grant ProMiSe (222.147), NWO Open Science Fund StormAE (OSF23.2.093), and a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 74.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    In 2016, Storm was available as an alpha-version under heavy development by Joost-Pieter Katoen and the authors of this paper.

  2. 2.

    also: scheduler or strategy.

  3. 3.

    also: actions.

  4. 4.

    https://github.com/moves-rwth/storm/commit/9da2eaf.

  5. 5.

    In a reaction to a long standing series of jokes, we are especially proud that Storm can be compiled within a few minutes.

  6. 6.

    See, e.g., the “Nacht der Professoren”.

  7. 7.

    The example is based on a puzzle of FiveThirtyEight.

  8. 8.

    Unless accidents occur.

  9. 9.

    Markov Decision Processes - Computerphile, youtube.com/watch?v=2iF9PRriA7w.

  10. 10.

    The model checker Uppaal has been used in 2017 to retroactively plan commutes of Kim G. Larsen between the towns of Danmark and Uppsala in 1995.

  11. 11.

    Abstracting good reasons: road blocks, coffee-deprivation, following famous cyclists.

  12. 12.

    We want to highlight that pMCs models that use rational functions as transition probabilities are somewhat rare in the literature: The use of polynomials is more standard.

  13. 13.

    https://elfstedentocht.frl/en.

  14. 14.

    The model is intentionally simple and does not accurately reflect the physical process of freezing or melting ice layers.

References

  1. de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University, USA (1997)

    Google Scholar 

  2. Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 88–104. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-40903-8_8

    Chapter  Google Scholar 

  3. Andriushchenko, R., et al.: Tools at the frontiers of quantitative verification. CoRR arxiv:2405.13583 (2024). https://doi.org/10.48550/ARXIV.2405.13583

  4. Andriushchenko, R., Češka, M., Junges, S., Katoen, J.-P.: Inductive synthesis for probabilistic programs reaches new horizons. In: TACAS 2021. LNCS, vol. 12651, pp. 191–209. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72016-2_11

    Chapter  Google Scholar 

  5. Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963–999. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_28

    Chapter  Google Scholar 

  6. Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003). https://doi.org/10.1109/TSE.2003.1205180

    Article  Google Scholar 

  7. Baier, C., Hermanns, H., Katoen, J.-P.: The 10,000 facets of MDP model checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 420–451. Springer, Cham (2019). https://doi.org/10.1007/978-3-319-91908-9_21

    Chapter  Google Scholar 

  8. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    Google Scholar 

  9. Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.P.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812–830 (2006). https://doi.org/10.1109/TSE.2006.104

    Article  Google Scholar 

  10. Brázdil, 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–114. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11936-6_8

    Chapter  Google Scholar 

  11. 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–168. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_9

    Chapter  Google Scholar 

  12. Ceska, M., Hensel, C., Junges, S., Katoen, J.P.: Counterexample-guided inductive synthesis for probabilistic systems. Formal Aspects Comput. 33(4–5), 637–667 (2021). https://doi.org/10.1007/S00165-021-00547-2

    Article  MathSciNet  Google Scholar 

  13. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Convex optimization for parameter synthesis in MDPs. IEEE Trans. Autom. Control 67(12), 6333–6348 (2022). https://doi.org/10.1109/TAC.2021.3133265

    Article  MathSciNet  Google Scholar 

  14. Dai, P., Weld, D.S.M., Goldsmith, J.: Topological value iteration algorithms. J. Artif. Intell. Res. 42, 181–209 (2011)

    MathSciNet  Google Scholar 

  15. Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592–600. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_31

    Chapter  Google Scholar 

  16. 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–113. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21455-4_3

    Chapter  Google Scholar 

  17. Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 317–332. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33386-6_25

    Chapter  Google Scholar 

  18. 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–317. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06410-9_22

    Chapter  Google Scholar 

  19. Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593–598. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_51

    Chapter  Google Scholar 

  20. Hartmanns, A., Junges, S., Katoen, J.P., Quatmann, T.: Multi-cost bounded tradeoff analysis in MDP. J. Autom. Reason. 64(7), 1483–1522 (2020). https://doi.org/10.1007/S10817-020-09574-9

    Article  MathSciNet  Google Scholar 

  21. Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner’s guide to MDP model checking algorithms. In: TACAS (1). Lecture Notes in Computer Science, vol. 13993, pp. 469–488. Springer, Heidelberg (2023). https://doi.org/10.1007/978-3-031-30823-9_24

  22. Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 344–350. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_20

    Chapter  Google Scholar 

  23. 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–610 (2022). https://doi.org/10.1007/S10009-021-00633-Z

    Article  Google Scholar 

  24. 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–362. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46419-0_24

    Chapter  Google Scholar 

  25. Jansen, N., Junges, S., Katoen, J.P.: Parameter synthesis in Markov models: a gentle survey. In: Principles of Systems Design. Lecture Notes in Computer Science, vol. 13660, pp. 407–437. Springer, Heidelberg (2022). https://doi.org/10.1007/978-3-031-22337-2_20

  26. Junges, S., et al.: Parameter synthesis for Markov models: covering the parameter space. Formal Methods Syst. Des. 62(1), 181–259 (2024). https://doi.org/10.1007/S10703-023-00442-X

    Article  Google Scholar 

  27. Katoen, J.P.: The probabilistic model checking landscape. In: LICS, pp. 31–45. ACM (2016). https://doi.org/10.1145/2933575.2934574

  28. 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–104 (2011). https://doi.org/10.1016/J.PEVA.2010.04.001

    Article  Google Scholar 

  29. Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Formal Methods Syst. Des. 36(3), 246–280 (2010). https://doi.org/10.1007/S10703-010-0097-6

    Article  Google Scholar 

  30. Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking and autonomy. Ann. Rev. Control. Rob. Auton. Syst. 5, 385–410 (2022). https://doi.org/10.1146/ANNUREV-CONTROL-042820-010947

    Article  Google Scholar 

  31. 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–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  32. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997). https://doi.org/10.1007/S100090050010

    Article  Google Scholar 

  33. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991). https://doi.org/10.1016/0890-5401(91)90030-6

    Article  MathSciNet  Google Scholar 

  34. Meggendorfer, T.: PET - a partial exploration tool for probabilistic verification. In: ATVA. LNCS, vol. 13505, pp. 320–326. Springer, Heidelberg (2022). https://doi.org/10.1007/978-3-031-19992-9_20

  35. Quatmann, T., Katoen, J.-P.: Multi-objective optimization of long-run average and total rewards. In: TACAS 2021. LNCS, vol. 12651, pp. 230–249. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72016-2_13

    Chapter  Google Scholar 

  36. Volk, M., Junges, S., Katoen, J.P.: Fast dynamic fault tree analysis by model checking techniques. IEEE Trans. Ind. Inf. 14(1), 370–379 (2018). https://doi.org/10.1109/TII.2017.2710316

    Article  Google Scholar 

  37. Watanabe, K., van der Vegt, M., Hasuo, I., Rot, J., Junges, S.: Pareto curves for compositionally model checking string diagrams of MDPs. In: TACAS (2). Lecture Notes in Computer Science, vol. 14571, pp. 279–298. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-57249-4_14

Download references

Acknowledgements

We are grateful to the many contributors to Storm and refer to our Git repository for a complete list. Furthermore, we want to highlight that the research on probabilistic model checking and the development of tool support has been actively pursued by an active and friendly community of researchers whose efforts have also shaped the contents of this paper. Last but not least, the authors would like to thank Joost-Pieter Katoen for his warm leadership and guidance during the last decade. His leadership goes well beyond his impressive and well-recognised academic achievements and includes the need for a healthy work-life balance, good coffee and good music.

Author information

Authors and Affiliations

  1. Radboud University, Nijmegen, The Netherlands

    Sebastian Junges

  2. RWTH Aachen University, Aachen, Germany

    Christian Hensel & Tim Quatmann

  3. Eindhoven University of Technology, Eindhoven, The Netherlands

    Matthias Volk

Authors
  1. Christian Hensel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sebastian Junges
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tim Quatmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Matthias Volk
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sebastian Junges .

Editor information

Editors and Affiliations

  1. Ruhr University Bochum and Radboud University Nijmegen, Bochum, Germany

    Nils Jansen

  2. Radboud University Nijmegen, Nijmegen, The Netherlands

    Sebastian Junges

  3. Saarland University and University College London, Saarbrücken, Germany

    Benjamin Lucien Kaminski

  4. University of Oldenburg, Oldenburg, Germany

    Christoph Matheja

  5. RWTH Aachen University, Aachen, Germany

    Thomas Noll

  6. RWTH Aachen University, Aachen, Germany

    Tim Quatmann

  7. University of Twente and Radboud University Nijmegen, Enschede, The Netherlands

    Mariëlle Stoelinga

  8. Eindhoven University of Technology, Eindhoven, The Netherlands

    Matthias Volk

Rights and permissions

Reprints and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Hensel, C., Junges, S., Quatmann, T., Volk, M. (2025). Riding the Storm in a Probabilistic Model Checking Landscape. In: Jansen, N., et al. Principles of Verification: Cycling the Probabilistic Landscape . Lecture Notes in Computer Science, vol 15261. Springer, Cham. https://doi.org/10.1007/978-3-031-75775-4_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-75775-4_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-75774-7

  • Online ISBN: 978-3-031-75775-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation