Upper bound of Policies for Statistical Model Checking of Markov Decision Processes

Document Type : Original Article

Author

Vali-e-Asr University of Rafsanjan

Abstract

State explosion is a predominant challenge of model checking in all variants. Statistical model checking (SMC) is proposed to tackle this problem, which leads to promising results in most cases. Computing near-optimal policies for resolving non-deterministic choices is the main obstacle for applying SMC in the verification of Markov decision processes (MDPs). Although several solutions are available to cope with this problem they mainly suffer from memory limitation or non-accurate results with the given confidence level. In this paper, we define a criterion for the fitness of policies. We propose a novel method that provides an upper-bound for the number of policies needed to guarantee the precision of computed values with the desired level of confidence. The proposed criterion relies on statistical analysis on a set of randomly generated policies. It considers the mean and expected values of the computed reachability probabilities for the states of the model to determine an appropriate upper bound for the number of policies. We run a set of experiments for the proposed method.

Keywords

References

  1. Baier, C., &Katoen, J. P. (2008). Principles of model checking. MIT press, Cambridge, United States.
  2. Baier, C., Hermanns, H., &Katoen, JP. (2019). The 10,000 Facets of MDP Model Checking. Computing and Software Science. Lecture Notes in Computer Science, vol 10000. Springer, Cham, Switzerland. doi:10.1007/978-3-319-91908-9_21.
  3. Hartmanns, A., Junges, S., Quatmann, T., &Weininger, M. (2023). A Practitioner’s Guide to MDP Model Checking Algorithms. Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023. Lecture Notes in Computer Science, vol 13993. Springer, Cham,doi:10.1007/978-3-031-30823-9_24.
  4. Hartmanns, A., &Kaminski, B.L. (2020). Optimistic Value Iteration. Computer Aided Verification. CAV 2020. Lecture Notes in Computer Science, vol 12225. Springer, Cham, Switzerland. doi:10.1007/978-3-030-53291-8_26.
  5. Younes, H.L.S., &Simmons, R.G. (2002). Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling. Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Germany. doi:10.1007/3-540-45657-0_17.
  6. D’Argenio, P., Legay, A., Sedwards, S., &Traonouez, L. M. (2015). Smart sampling for lightweight verification of markov decision processes. International Journal on Software Tools for Technology Transfer, 17(4), 469– doi:10.1007/s10009-015-0383-0.
  7. Hartmanns, A.: On the analysis of stochastic timed systems. Ph.D. thesis, Saarland University, Germany (2015)
  8. Legay, A., Sedwards, S., &Traonouez, (2015). Scalable Verification of Markov Decision Processes. In: Canal, C., Idani, A. (eds) Software Engineering and Formal Methods. SEFM 2014. Lecture Notes in Computer Science, vol 8938. Springer, Cham, Switzerland. doi:10.1007/978-3-319-15201-1_23.
  9. Kanav, S., Křetínský, J., Larsen, K.G. (2025). Statistical Model Checking the 2024 Edition!.Bridging the Gap Between AI and Reality. AISoLA 2024. Lecture Notes in Computer Science, vol 15217. Springer, Cham, doi:10.1007/978-3-031-75434-0_21.
  10. Bogdoll, J., Hartmanns, A., &Hermanns, H. (2012). Simulation and Statistical Model Checking for Modestly Nondeterministic Models. Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance. MMB&DFT 2012. Lecture Notes in Computer Science, vol 7201. Springer, Berlin, doi:10.1007/978-3-642-28540-0_20.
  11. Henriques, D., Martins, J. G., Zuliani, P., Platzer, A., & Clarke, E. M. (2012). Statistical Model Checking for Markov Decision Processes. 2012 Ninth International Conference on Quantitative Evaluation of Systems, 84–93. doi:10.1109/qest.2012.19.
  12. Budde, C. E., D’Argenio, P. R., Hartmanns, A., &Sedwards, S. (2020). An efficient statistical model checker for nondeterminism and rare events. International Journal on Software Tools for Technology Transfer, 22(6), 759– doi:10.1007/s10009-020-00563-2.
  13. Budde, C.E., Hartmanns, A., Meggendorfer, T., Weininger, &, Wienhöft, P. (2025). Sound Statistical Model Checking for Probabilities and Expected Rewards. Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2025. Lecture Notes in Computer Science, vol 15696. Springer, Cham, Switzerland. doi:10.1007/978-3-031-90643-5_9.
  14. Parmentier, M., Legay, A., Chenoy, F. (2024). Optimized Smart Sampling. Bridging the Gap Between AI and Reality. AISoLA 2023. Lecture Notes in Computer Science, vol 14380. Springer, Cham, Switzerland. doi:10.1007/978-3-031-46002-9_10.
  15. Kwiatkowska, M., Norman, G., &Segala, (2001). Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM. Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Germany. doi:10.1007/3-540-44585-4_17.
  16. Reijsbergen, D., de Boer, P.-T., Scheinhardt, W., &Haverkort, B. (2014). On hypothesis testing for statistical model checking. International Journal on Software Tools for Technology Transfer, 17(4), 377–395. doi:10.1007/s10009-014-0350-1.
  17. Okamoto, M. (1959). Some inequalities relating to the partial sum of binomial probabilities. Annals of the Institute of Statistical Mathematics, 10(1), 29–35. doi:10.1007/BF02883985.
  18. Kearns, M., Mansour, Y., & Ng, A. Y. (2002). A sparse sampling algorithm for near-optimal planning in large Markov decision processes. Machine Learning, 49(2–3), 193– doi:10.1023/A:1017932429737.
  19. Ashok, P., Křetínský, &, Weininger, M. (2019). PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games. Computer Aided Verification. CAV 2019. Lecture Notes in Computer Science, vol 11561. Springer, Cham, Switzerland. doi:10.1007/978-3-030-25540-4_29.
  20. Budde, C.E., D’Argenio, P.R., Fraire, J.A., Hartmanns, A., Zhang, Z. (2025). Modest Models and Tools for Real Stochastic Timed Systems. Principles of Verification: Cycling the Probabilistic Landscape. Lecture Notes in Computer Science, vol 15261. Springer, Cham, doi:10.1007/978-3-031-75775-4_6.
  21. Rataj, A., &Woźna-Szcześniak, B. (2018). Extrapolation of an Optimal Policy using Statistical Probabilistic Model Checking.FundamentaInformaticae, 157(4), 443– doi:10.3233/FI-2018-1637.
  22. Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., &Steinmetz, M. (2020). Deep Statistical Model Checking. Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2020. Lecture Notes in Computer Science, vol 12136. Springer, Cham, Switzerland. doi:10.1007/978-3-030-50086-3_6.
  23. Kwiatkowska, M., Norman, G., &Parker, D. (2011). PRISM 4.0: Verification of Probabilistic Real-Time Systems. Computer Aided Verification. CAV 2011. Lecture Notes in Computer Science, vol 6806. Springer, Berlin, Germany. doi:10.1007/978-3-642-22110-1_47.
  24. Agarwal, C., Guha, S., Křetínský, J., &Pazhamalai, M. (2025). PAC statistical model checking of mean payoff in discrete- and continuous-time MDP. Formal Methods in System Design, 66(2), 195–237. doi:10.1007/s10703-024-00463-0.
  25. Perez, M., Somenzi, F., & Trivedi, A. (2024). A PAC Learning Algorithm for LTL and Omega-Regular Objectives in MDPs. Proceedings of the AAAI Conference on Artificial Intelligence, 38(19), 21510–21517. doi:10.1609/aaai.v38i19.30148.
  26. Azeem, M., Chakraborty, D., Kanav, S., Křetínský, J., Mohagheghi, M., Mohr, S., &&Weininger, M. (2025). 1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization. Verification, Model Checking, and Abstract Interpretation. VMCAI 2025. Lecture Notes in Computer Science, vol 15530. Springer, Cham, Switzerland. doi:10.1007/978-3-031-82703-7_5
  27. Clarke, E. M., Henzinger, T. A., Veith, H., &Bloem, R. (Eds.). (2018). Handbook of Model Checking. Springer International Publishing, Cham, Switzerland. doi:10.1007/978-3-319-10575-8.
  28. D’argenio, P. R., Fraire, J., Hartmanns, A., &Raverta, F. (2025). Comparing Statistical, Analytical, and Learning-Based Routing Approaches for Delay-Tolerant Networks. ACM Transactions on Modeling and Computer Simulation, 35(2). doi:10.1145/3665927.
  29. Meggendorfer, T., Weininger, M., &Wienhöft, P. (2026). What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes. Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems. QEST+FORMATS 2025. Lecture Notes in Computer Science, vol 16143. Springer, Cham, Switzerland. doi:10.1007/978-3-032-05792-1_11
  30. Legay, A., Sedwards, S., &Traonouez, LM. (2016). Plasma Lab: A Modular Statistical Model Checking Platform. Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science(), vol 9952. Springer, Cham, Switzerland. doi:10.1007/978-3-319-47166-2_6.
  31. Safari, M. (2025). 'Experimental analysis, statistical modeling and optimization of the edge effects associated with laser-bent perforated sheets', Contributions of Science and Technology for Engineering, 2(3), pp. 37-44. doi: 10.22080/cste.2025.28804.1019
  32. Hensel, C., Junges, S., Katoen, J. P., Quatmann, T., & Volk, M. (2022). The probabilistic model checker Storm. International Journal on Software Tools for Technology Transfer, 24(4), 589–610. doi:10.1007/s10009-021-00633-z.
  33. Stephens, M. A. (1974). EDF statistics for goodness of fit and some comparisons. Journal of the American Statistical Association, 69(347), 730–737. doi:10.1080/01621459.1974.10480196.
Contributions of Science and Technology for Engineering
Volume 3, Issue 1
February 2026
Pages 31-40

Files

History

  • Receive Date: 03 April 2025
  • Revise Date: 01 August 2025
  • Accept Date: 29 September 2025
  • First Publish Date: 29 September 2025
  • Publish Date: 12 February 2026

Share

How to cite

Statistics