Learning Methods for Statistical Model Checking of DTMC

Mohagheghi, Mohammadsadegh; Salehi, Khayyam

doi:10.15388/26-INFOR619

Informatica

Learning Methods for Statistical Model Checking of DTMC

Mohammadsadegh Mohagheghi Khayyam Salehi

https://doi.org/10.15388/26-INFOR619

Pub. online: 11 February 2026 Type: Research Article

Open Access

Received
1 January 2025

Accepted
1 February 2026

Published
11 February 2026

Abstract

Statistical model checking offers an alternative to traditional model checking for large stochastic systems, addressing state space explosion and approximating quantitative properties. This paper proposes machine learning approaches using decision trees to approximate zero-reachability states, offering both computational efficiency and interpretability. Statistical analysis is used as an alternative approach to establish simulation run length bounds to control computation errors. Experimental results across standard Markov models demonstrate that our decision structures maintain high correctness (99% in most cases), reduce runtime, and have minimal memory overhead. Even when some methods show limitations, alternative approaches within our framework yield effective results.

References

Agha, G., Palmskog, K. (2018). A survey of statistical model checking. ACM Transactions on Modeling and Computer Simulation (TOMACS), 28(1), 1–39.

Aichernig, B.K., Tappler, M. (2017). Probabilistic black-box reachability checking. In: Runtime Verification: 17th International Conference, RV 2017, Seattle, WA, USA, September 13–16, 2017, Proceedings 17. Springer, pp. 50–67.

Arora, S., Rao, M.P. (2020). The Bouquet algorithm for model checking unbounded until properties. In: 2020 International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE, pp. 113–120.

Ashok, P., Křetínskỳ, J., Weininger, M. (2019). PAC statistical model checking for Markov decision processes and stochastic games. In: Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15–18, 2019, Proceedings, Part I 31. Springer, pp. 497–519.

Ashok, P., Daca, P., Křetínskỳ, J., Weininger, M. (2020). Statistical model checking: black or white? In: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part I 9. Springer, pp. 331–349.

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

Baier, C., Hermanns, H., Katoen, J.-P. (2019). The 10,000 facets of MDP model checking. In: Computing and Software Science: State of the Art and Perspectives, pp. 420–451.

Bao, Y., Chen, M., Zhu, Q., Wei, T., Mallet, F., Zhou, T. (2017). Quantitative performance evaluation of uncertainty-aware hybrid AADL designs using statistical model checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 36(12), 1989–2002.

Bertrand, N., Bordais, B., Hélouët, L., Mari, T., Parreaux, J., Sankur, O. (2019). Performance evaluation of metro regulations using probabilistic model-checking. In: Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: Third International Conference, RSSRail 2019, Lille, France, June 4–6, 2019, Proceedings 3. Springer, pp. 59–76.

Bortolussi, L., Milios, D., Sanguinetti, G. (2015). Machine learning methods in statistical model checking and system design–tutorial. In: Runtime Verification: 6th International Conference, RV 2015, Vienna, Austria, September 22–25, 2015. Proceedings. Springer, pp. 323–341.

Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Křetínskỳ, J., Kwiatkowska, M., Parker, D., Ujma, M. (2014). Verification of Markov decision processes using learning algorithms. In: Automated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3–7, 2014, Proceedings 12. Springer, pp. 98–114.

Brázdil, T., Chatterjee, K., Chmelík, M., Fellner, A., Křetínskỳ, J. (2015). Counterexample explanation by learning small strategies in Markov decision processes. In: Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015, Proceedings, Part I 27. Springer, pp. 158–177.

Bryant, R.E. (1986). Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 100(8), 677–691.

Budde, C.E., D’Argenio, P.R., Hartmanns, A., Sedwards, S. (2020a). An efficient statistical model checker for nondeterminism and rare events. International Journal on Software Tools for Technology Transfer, 22(6), 759–780.

Budde, C.E., Hartmanns, A., Klauck, M., Křetínskỳ, J., Parker, D., Quatmann, T., Turrini, A., Zhang, Z. (2020b). On correctness, precision, and performance in quantitative verification: QComp 2020 competition report. In: International Symposium on Leveraging Applications of Formal Methods. Springer, pp. 216–241.

Calinescu, R., Paterson, C., Johnson, K. (2019). Efficient parametric model checking using domain knowledge. IEEE Transactions on Software Engineering, 47(6), 1114–1133.

Casaluce, R., Burattin, A., Chiaromonte, F., Vandin, A. (2022). Process mining meets statistical model checking: towards a novel approach to model validation and enhancement. In: International Conference on Business Process Management. Springer, pp. 243–256.

Clarke, E.M., Zuliani, P. (2011). Statistical model checking for cyber-physical systems. In: Automated Technology for Verification and Analysis: 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11–14, 2011. Proceedings 9. Springer, pp. 1–12.

Clarke, E.M., Henzinger, T.A., Veith, H. (2018). Introduction to model checking. In: Handbook of Model Checking, pp. 1–26.

Cleaveland, M., Ruchkin, I., Sokolsky, O., Lee, I. (2022). Monotonic safety for scalable and data-efficient probabilistic safety analysis. In: 2022 ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS). IEEE, pp. 92–103.

Daca, P., Henzinger, T.A., Křetínskỳ, J., Petrov, T. (2017). Faster statistical model checking for unbounded temporal properties. ACM Transactions on Computational Logic (TOCL), 18(2), 1–25.

David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Van Vliet, J., Wang, Z. (2011). Statistical model checking for networks of priced timed automata. In: Formal Modeling and Analysis of Timed Systems: 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21–23, 2011. Proceedings 9. Springer, pp. 80–96.

David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Sedwards, S. (2015). Statistical model checking for biological systems. International Journal on Software Tools for Technology Transfer, 17, 351–367.

Dehnert, C., Junges, S., Katoen, J.-P., Volk, M. (2017). A storm is coming: a modern probabilistic model checker. In: Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Proceedings, Part II 30. Springer, pp. 592–600.

D’argenio, P.R., Fraire, J.A., Hartmanns, A., Raverta, F. (2022). Comparing statistical and analytical routing approaches for delay-tolerant networks. In: Quantitative Evaluation of Systems: 19th International Conference, QEST 2022, Warsaw, Poland, September 12–16, 2022, Proceedings. Springer. pp. 337–355.

Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., Steinmetz, M. (2020). Deep statistical model checking. In: Formal Techniques for Distributed Objects, Components, and Systems: 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15–19, 2020, Proceedings 40. Springer, pp. 96–114.

Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., Steinmetz, M. (2022). Analyzing neural network behavior through deep statistical model checking. International Journal on Software Tools for Technology Transfer, 25, 407–426.

Hahn, E.M., Hartmanns, A. (2016). A comparison of time-and reward-bounded probabilistic model checking techniques. In: Dependable Software Engineering: Theories, Tools, and Applications: Second International Symposium, SETTA 2016, Beijing, China, November 9–11, 2016, Proceedings 2. Springer. pp. 85–100.

Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E. (2019). The quantitative verification benchmark set. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, pp. 344–350.

Henriques, D., Martins, J.G., Zuliani, P., Platzer, A., Clarke, E.M. (2012). Statistical model checking for Markov decision processes. In: 2012 Ninth international conference on quantitative evaluation of systems, IEEE, pp. 84–93.

Karna, A.K., Chen, Y., Yu, H., Zhong, H., Zhao, J. (2018). The role of model checking in software engineering. Frontiers of Computer Science, 12, 642–668.

Kim, Y., Kim, M. (2012). Hybrid statistical model checking technique for reliable safety critical systems. In: 2012 IEEE 23rd International Symposium on Software Reliability Engineering, IEEE, pp. 51–60.

Kwiatkowska, M., Norman, G., Parker, D. (2011). PRISM 4.0: Verification of probabilistic real-time systems. In: Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14–20, 2011. Proceedings 23. Springer. pp. 585–591.

Kwiatkowska, M., Norman, G., Parker, D. (2012). The PRISM benchmark suite. In: 9th International Conference on Quantitative Evaluation of SysTems. IEEE CS Press, pp. 203–204.

Kwiatkowska, M., Norman, G., Parker, D., Sproston, J. (2006). Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design, 29(1), 33–78.

Larsen, K., Legay, A., Nolte, G., Schlüter, M., Stoelinga, M., Steffen, B. (2022). Formal methods meet machine learning (F3ML). In: International Symposium on Leveraging Applications of Formal Methods. Springer, pp. 393–405.

Legay, A., Viswanathan, M. (2015). Statistical model checking: challenges and perspectives. International Journal on Software Tools for Technology Transfer, 17, 369–376.

Legay, A., Delahaye, B., Bensalem, S. (2010). Statistical model checking: an overview. In: Runtime Verification, Vol. 10. Springer Berlin Heidelberg, pp. 122–135.

Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R. (2019). Statistical model checking. In: Computing and Software Science: State of the Art and Perspectives. Springer, pp. 478–504.

Milton, J.S., Arnold, J.C. (2002). Introduction to Probability and Statistics: Principles and Applications for Engineering and the Computing Sciences. McGraw-Hill Higher Education.

Mohagheghi, M., Chaboki, B. (2020). Dirac-based reduction techniques for quantitative analysis of discrete-time markov models. In: Topics in Theoretical Computer Science. Springer, pp. 1–16.

Mohagheghi, M., Salehi, K. (2020). Improving graph-based methods for computing qualitative properties of markov decision processes. Indonesian Journal of Electrical Engineering and Computer Science, 17(3), 1571–1577.

Mohagheghi, M., Salehi, K. (2024). Improving probabilistic bisimulation for MDPs using machine learning. Mathematics Interdisciplinary Research, 9(2), 151–169.

Mohagheghi, M., Karimpour, J., Isazadeh, A. (2020). Prioritizing methods to accelerate probabilistic model checking of discrete-time Markov models. The Computer Journal, 63(1), 105–122.

Murphy, K.P. (2022). Probabilistic machine learning: an introduction. MIT press.

Norman, G., Shmatikov, V. (2006). Analysis of probabilistic contract signing. Journal of Computer Security, 14(6), 561–589.

Norman, G., Parker, D., Kwiatkowska, M., Shukla, S. (2005). Evaluating the reliability of NAND multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(10), 1629–1637.

Pasupa, K., Sunhem, W. (2016). A comparison between shallow and deep architecture classifiers on small dataset. In: 2016 8th International Conference on Information Technology and Electrical Engineering (ICITEE). IEEE, pp. 1–6.

Qin, X., Xian, Y., Zutshi, A., Fan, C., Deshmukh, J.V. (2022). Statistical verification of cyber-physical systems using surrogate models and conformal inference. In: 2022 ACM/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS). IEEE, pp. 116–126.

Salehi, K., Karimpour, J., Izadkhah, H., Isazadeh, A. (2019). Channel capacity of concurrent probabilistic programs. Entropy, 21(9), 885.

Sen, K., Viswanathan, M., Agha, G. (2004). Statistical model checking of black-box probabilistic systems. In: Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13–17, 2004. Proceedings 16. Springer, pp. 202–215.

Sen, K., Viswanathan, M., Agha, G. (2005). On statistical model checking of stochastic systems. In: Computer Aided Verification: 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005. Proceedings 17. Springer, pp. 266–280.

Song, J., Baek, Y.-M., Jin, M., Jee, E., Bae, D.-H. (2017). Sos gap slicer: Slicing sos goal and prism models for change-responsive verification of sos. In: 2017 24th Asia-Pacific Software Engineering Conference (APSEC), IEEE, pp. 546–551.

Tadjudin, S., Landgrebe, D.A. (1996). A decision tree classifier design for high-dimensional data with limited training samples. In: IGARSS’96. 1996 International Geoscience and Remote Sensing Symposium, Vol. 1, IEEE, pp. 790–792.

Wang, J., Sun, J., Yuan, Q., Pang, J. (2018). Learning probabilistic models for model checking: an evolutionary approach and an empirical study. International Journal on Software Tools for Technology Transfer, 20(6), 689–704.

Wang, Y., Nalluri, S., Bonakdarpour, B., Pajic, M. (2021). Statistical model checking for hyperproperties. In: 2021 IEEE 34th Computer Security Foundations Symposium (CSF), IEEE, pp. 1–16.

Younes, H.L., Simmons, R.G. (2002). Probabilistic verification of discrete event systems using acceptance sampling. In: Computer Aided Verification: 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27–31, 2002 Proceedings 14. Springer, pp. 223–235.

Younes, H.L., Clarke, E.M., Zuliani, P. (2010). Statistical verification of probabilistic properties with unbounded until. In: Brazilian Symposium on Formal Methods. Springer. pp. 144–160.

Younes, H.L., Kwiatkowska, M., Norman, G., Parker, D. (2006). Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer, 8, 216–228.

Zuliani, P. (2015). Statistical model checking for biological applications. International Journal on Software Tools for Technology Transfer, 17, 527–536.

Biographies

Mohagheghi Mohammadsadegh

mohagheghi@vru.ac.ir

M. Mohagheghi received his PhD in computer science from University of Tabriz in 2019, his master’s in computer science from Sharif University of technology in 2008 and BSc in software engineering from Shahidbeheshty University in 2006. He is currently a faculty member of computer science in Vali-e-Asr University of Rafsanjan, Iran. His main research interests include formal verification of stochastic and real-time systems, probabilistic model checking and machine learning.

Salehi Khayyam

https://orcid.org/0000-0002-3379-798X

kh.salehi@sku.ac.ir

K. Salehi received his PhD in computer science from University of Tabriz in 2019, MSc and BSc in computer science from Sharif University of Technology and Yazd University in 2010 and 2007, respectively. He is currently an assistant professor of computer science in Shahrekord University, Iran. His main research involves machine learning and formal methods, as well as scientific computation.

Full article Related articles

Open access article under the CC BY license.

Keywords

statistical model checking machine learning decision tree classifiers probabilistic systems reachability probability

Metrics

since January 2020

112

Article info
views

Full article
views

PDF
downloads

XML
downloads

RSS

Authors

Abstract

References

Biographies

Export citation

Copy and paste formatted citation

Download citation in file