Improving Probabilistic Bisimulation for MDPs Using Machine Learning

Document Type : Original Scientific Paper

Authors

1 ‎Department of Computer Science, ‎Vali-e-Asr University of Rafsanjan, ‎Rafsanjan‎, ‎I‎. ‎R‎. ‎Iran

2 ‎Department of Computer Science, Shahrekord University, ‎Shahrekord‎, ‎I‎. ‎R‎. ‎Iran

Abstract

‎The utilization of model checking has been suggested as a formal verification technique for analyzing critical systems‎. ‎However‎, ‎the primary challenge in applying to complex systems is the state space explosion problem‎. ‎To address this issue‎, ‎bisimulation minimization has emerged as a prominent method for reducing the number of states in a system‎, ‎aiming to overcome the difficulties associated with the state space explosion problem‎. ‎For systems with stochastic behaviors‎, ‎probabilistic bisimulation is employed to minimize a given model‎, ‎obtaining its equivalent form with fewer states‎. ‎In this paper‎, ‎we propose a novel technique to partition the state space of a given probabilistic model to its bisimulation classes‎. ‎This technique uses the PRISM program of a given model and constructs some small versions of the model to train a classifier‎. ‎It then applies supervised machine learning techniques to approximately classify the related partition‎. ‎The resulting partition is then used to accelerate the standard bisimulation technique‎, ‎significantly reducing the running time of the method‎. ‎The experimental results show that the approach can decrease significantly the running time compared to state-of-the-art tools‎.

Keywords

Main Subjects

References

[1] E. M. Clarke, T. A. Henzinger and H. Veith, Introduction to model checking, Handbook of model checking (2018) 1 - 26.
[2] C. Baier and J. P. Katoen, Principles of Model Checking, MIT press, 2008.
[3] J. P. Katoen, The probabilistic model checking landscape, In: Proc. of the 31st Annual ACM-IEEE Symp. on Logic in Comput. Sci. (2016) 31- 45, https://doi.org/10.1145/2933575.2934574.
[4] K. L. McMillan, Symbolic Model Checking, Springer, 1993.
[5] D. A. Parker, Implementation of Symbolic Model Checking for Probabilistic Systems, Ph.D. thesis, University of Birmingham, 2003.
[6] E. M. Clarke, D. E. Long and K. L. McMillan, Compositional model checking, In: Proc. of the 4th IEEE Symp. on Logic in Comput. Sci. (1989) 353 - 362, https://doi.org/10.1109/LICS.1989.39190.
[7] L. Feng, M. Kwiatkowska and D. Parker, Compositional verification of probabilistic systems using learning, In: Proc. 7th Int. Conf. on Quantitative Evaluation of Systems, IEEE CS Press (2010) 133 - 142, https://doi.org/10.1109/QEST.2010.24.
[8] G. Agha and K. Palmskog, A survey of statistical model checking, ACM Trans. Model. Comput. Simul. 28 (2018) 1 - 39, https://doi.org/10.1145/3158668.
[9] A. Legay, A. Lukina, L. M. Traonouez, J. Yang, S. A. Smolka and R. Grosu, Statistical model checking, Computing and software science: state of the art and perspectives, Springer (2019) 478 - 504.
[10] A. Legay and M. Viswanathan, Statistical model checking: challenges and perspectives, Int. J. Softw. Tools Technol. Transfer 17 (2015) 369 - 376, https://doi.org/10.1007/s10009-015-0384-z.
[11] F. Ciesinski, C. Baier, M. Größer and J. Klein, Reduction techniques for model checking markov decision processes, In: Proc. 5th Int. Conf. on Quantitative Evaluation of Systems, IEEE CS Press. (2008) 45 - 54, https://doi.org/10.1109/QEST.2008.45.
[12] H. Hansen, M. Kwiatkowska and H. Qu, Partial order reduction for model checking markov decision processes under unconditional fairness, In: Proc. 8th Int. Conf. on Quantitative Evaluation of Systems (2011) 203 - 212, https://doi.org/10.1109/QEST.2011.35.
[13] M. Kwiatkowska, G. Norman and D. Parker, Symmetry reduction for probabilistic model checking, In: Proc. 18th Int. Conf. Computer aided verification, Springer (2006) 234 - 248.
[14] C. Baier, P. R. D’Argenio and H. Hermanns, On the probabilistic bisimulation spectrum with silent moves, Acta Inform. 57 (2020) 465 - 512, https://doi.org/10.1007/s00236-020-00379-2.
[15] K. Salehi, A. A. Noroozi, S. Amir-Mohammadian and M. Mohagheghi, An automated quantitative information flow analysis for concurrent programs, In: Proc. 19th Int. Conf. on Quantitative Evaluation of Systems, Springer (2022) 43 - 63.
[16] J. F. Groote, J. Rivera Verduzco and E. P. De Vink, An efficient algorithm to determine probabilistic bisimulation, Algorithms 11 (2018) p. 131, https://doi.org/10.3390/a11090131.
[17] S. Cattani and R. Segala, Decision algorithms for probabilistic bisimulation, In: Proc. 13th Int. Conf. on Concurrency Theory, Springer (2002) 371-385.
[18] K. G. Larsen and A. Skou, Bisimulation through probabilistic testing, Inform. and Comput. 94 (1991) 1 - 28.
[19] R. Segala, Modeling and Verification of Randomized Distributed Real-Time Systems, Ph.D. thesis, Massachusetts Institute of Technology, 1995.
[20] M. I. A Stoelinga, Alea Jacta Est: Verification of Probabilistic, Real-Time and Parametric Systems, Ph.D. thesis, Radboud University, Nijmegen, 2002.
[21] M. Mohagheghi and K. Salehi, Splitter orderings for probabilistic bisimulation, arXiv:2307.08614 (2023)
[22] M. Kwiatkowska, G. Norman and D. Parker, Prism 4.0: Verification of probabilistic real-time systems, In: Proc. Int. Conf. on Computer aided verification, Springer (2011) 585 - 591.
[23] C. Hensel, S. Junges, J. P. Katoen, T. Quatmann and M. Volk, The probabilistic model checker storm, Int. J. Softw. Tools Technol. Transfer 24 (2022) 589 - 610, https://doi.org/10.1007/s10009-021-00633-z.
[24] O. Bunte, J. F. Groote, J. J. A. Keiren, M. Laveaux, T. Neele, E. P. de Vink, W. Wesselink, A. Wijs and T. A. C. Willemse, The mcrl2 toolset for analysing concurrent systems: improvements in expressivity and usability, In: Proc. 25th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (2019) 21–39.
[25] C. Shields and B. N. Levine, A protocol for anonymous communication over the internet, In: Proc. ACM Conf. Comput. Commun. Secur. (2000) 33-42, https://doi.org/10.1145/352600.352607.
[26] A. A. Noroozi, K. Salehi, J. Karimpour and A. Isazadeh, Secure information flow analysis using the prism model checker, Int. Conf. on Information Systems Security, Springer (2019) 154 - 172.
[27] K. Salehi, J. Karimpour, H. Izadkhah and A. Isazadeh, Channel capacity of concurrent probabilistic programs, Entropy 21 (2019) p. 885, https://doi.org/10.3390/e21090885.
[28] M. K. Reiter and A. D. Rubin, Crowds: anonymity for web transactions, ACM Trans. Inf. Syst. Secur. 1 (1998) 66 - 92,
https://doi.org/10.1145/290163.290168.
[29] M. G. Reed, P. F. Syverson and D. M. Goldschlag, Anonymous connections and onion routing, IEEE J. Sel. Areas Commun. 16 (1998) 482 - 494, https://doi.org/10.1109/49.668972.
Mathematics Interdisciplinary Research
Volume 9, Issue 2
June 2024
Pages 151-169

Files

Share

How to cite

Statistics