Using splitter ordering heuristics to improve bisimulation in probabilistic model checking

• Autorzy: Mohagheghi Mohammadsadegh , Salehi Khayyam

Identyfikatory

DOI

10.7494/csci.2025.26.2.6411

• Języki publikacji: EN

Abstrakty

EN

Model checking is used to verify computer-based and cyber-physical systems, but faces challenges due to state space explosion. Bisimulation minimization reduces states in transition systems, easing this issue. Probabilistic bisimulation further simplifies models with stochastic behaviors. Recent techniques aim to improve the time complexity of iterative methods in computing probabilistic bisimulation for stochastic systems with nondeterministic behaviors. In this paper, we propose several techniques to accelerate iterative processes to partition the state space of a given probabilistic model to its bisimulation classes. The first technique applies two ordering heuristics for choosing splitter blocks. The second technique uses hash tables to reduce the running time and the average time complexity of the standard iterative method. The proposed approaches are implemented and run on several conventional case studies and reduce the running time by one order of magnitude on average.

Słowa kluczowe

EN

probabilistic bisimulation; Markov decision process; model checking; splitter ordering

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2025
• Tom: T. 26 (2)
• Strony: 49--75
• Opis fizyczny: Bibliogr. 45 poz., rys., tab., wykr.

Twórcy

autor

Mohagheghi Mohammadsadegh

• Vali-e-Asr University of Rafsanjan, Department of Computer Science, Rafsanjan, Iran

autor

Salehi Khayyam

• Shahrekord University, Department of Computer Science, Shahrekord, Iran

Bibliografia

• [1] Abadi M., Gordon A.D.: A bisimulation method for cryptographic protocols. In: C. Hankin (ed.),Programming Languages and Systems. ESOP 1998, LectureNotes in Computer Science, vol. 1381, pp. 12–26, Springer, Berlin, Heidelberg,1998. doi: 10.1007/bfb0053560.
• [2] Abate A., Giacobbe M., Schnitzer Y.: Bisimulation Learning. In: A. Gurfinkel,V. Ganesh (eds.), 36th International Conference, CAV 2024 Montreal, QC, Canada, July 24–27, 2024 Proceedings, Part III, pp. 161–183, Springer, Cham, 2024. doi: 10.1007/978-3-031-65633-0_8.
• [3] Agha G., Palmskog K.: A survey of statistical model checking, ACM Transactions on Modeling and Computer Simulation (TOMACS), vol. 28(1), 6, 2018.doi: 10.1145/3158668.
• [4] Baier C., D’Argenio P.R., Hermanns H.: On the probabilistic bisimulation spectrum with silent moves, Acta Informatica, vol. 57(3), pp. 465–512, 2020.doi: 10.1007/s00236-020-00379-2.
• [5] Baier C., Engelen B., Majster-Cederbaum M.: Deciding bisimilarity and similarity for probabilistic processes, Journal of Computer and System Sciences, vol. 60(1), pp. 187–231, 2000. doi: 10.1006/jcss.1999.1683.
• [6] Baier C., Hermanns H., Katoen J.P.: The 10,000 facets of MDP model checking. In: B. Steffen, G. Woeginger (eds.), Computing and Software Science: State of the Art and Perspectives, pp. 420–451, Springer, 2019. doi: 10.1007/978-3-319-91908-9_21.
• [7] Baier C., Katoen J.P.: Principles of model checking, MIT Press, 2008.
• [8] Bisping B.: Process Equivalence Problems as Energy Games. In: C. Enea, A. Lal(eds.), Computer Aided Verification. 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part I, pp. 85–106, Springer NatureSwitzerland, Cham, 2023. doi: 10.1007/978-3-031-37706-8_5.
• [9] Budde C.E., Hartmanns A., Klauck M., Křetínsk`y J., Parker D., Quatmann T.,Turrini A., Zhang Z.: On correctness, precision, and performance in quantitative verification: QComp 2020 competition report. In: T. Margaria, B. Steffen (eds.), Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part IV, pp. 216–241, Springer, 2020. doi: 10.1007/978-3-030-83723-5_15.
• [10] Bunte O., Groote J.F., Keiren J.J.A., Laveaux M., Neele T., de Vink E.P.,Wesselink W.,et al.: The mCRL2 toolset for analysing concurrent systems. In: T. Vojnar, L. Zhang (eds.),Tools and Algorithms for the Construction and Analysis of Systems. 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part II, pp. 21–39, Springer, 2019. doi: 10.1007/978-3-030-17465-1_2.
• [11] Castro P.S.: Scalable methods for computing state similarity in deterministic Markov decision processes. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34(06), pp. 10069–10076, 2020. doi: 10.1609/aaai.v34i06.6564.
• [12] Cattani S., Segala R.: Decision algorithms for probabilistic bisimulation. In: L. Brim, M. Křetínský, A. Kučera, P. Jančar (eds.), CONCUR 2002 – Concurrency Theory. 13th International Conference, Brno, Czech Republic, Au-gust 20–23, 2002. Proceedings, pp. 371–386, Springer, 2002. doi: 10.1007/3-540-45694-5_25.
• [13] Ciesinski F., Baier C., Größer M., Klein J.: Reduction techniques for model checking Markov decision processes. In: 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp. 45–54, IEEE, 2008. doi: 10.1109/qest.2008.45.
• [14] Clarke E.M., Henzinger T.A., Veith H.: Introduction to model checking. In: E.M. Clarke, T.A. Henzinger, H. Veith, R. Bloem (eds.), Handbook of Model Checking, pp. 1–26, Springer, 2018. doi: 10.1007/978-3-319-10575-8_1.
• [15] Clarke E.M., Henzinger T.A., Veith H., Bloem R. (eds.): Handbook of model checking, Springer, 2018.
• [16] Dehnert C., Junges S., Katoen J.P., Volk M.: A STORM is coming: A modern probabilistic model checker. In: R. Majumdar, V. Kunčak (eds.), Computer Aided Verification. 29th International Conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Proceedings, Part II, pp. 592–600, Springer, 2017. doi: 10.1007/978-3-319-63390-9_31.
• [17] Dehnert C., Katoen J.P., Parker D.: SMT-based bisimulation minimisation of Markov models. In: R. Giacobazzi, J. Berdine, I. Mastroeni (eds.),Verification, Model Checking, and Abstract Interpretation. 14th International Conference, VMCAI 2013, Rome, Italy, January 20–22, 2013, Proceedings, pp. 28–47, Springer, 2013. doi: 10.1007/978-3-642-35873-9_5.
• [18] Deifel H.P., Milius S., Schröder L., Wißmann T.: Generic partition refinement and weighted tree automata. In: M.H. ter Beek, A. McIver, J.N. Oliveira(eds.), Formal Methods – The Next 30 Years. Third World Congress, FM 2019, Porto, Portugal, October 7–11, 2019, Proceedings, pp. 280–297, Springer, 2019.doi: 10.1007/978-3-030-30942-8_18.
• [19] Dijk van T., Pol van de J.: Multi-core symbolic bisimulation minimisation, International Journal on Software Tools for Technology Transfer, vol. 20(2), pp. 157–177, 2018. doi: 10.1007/s10009-017-0468-z.
• [20] Feng L., Kwiatkowska M., Parker D.: Compositional verification of probabilistic systems using learning. In: 2010 Seventh International Conference on the Quantitative Evaluation of Systems, pp. 133–142, IEEE, 2010. doi: 10.1109/qest.2010.24.
• [21] Fisler K., Vardi M.Y.: Bisimulation minimization and symbolic model checking, Formal Methods in System Design, vol. 21(1), pp. 39–78, 2002. doi: 10.1023/a:1016091902809.
• [22] Forejt V., Kwiatkowska M., Norman G., Parker D.: Automated verification techniques for probabilistic systems. In: M. Bernardo, V. Issarny (eds.),Formal Methods for Eternal Networked Software Systems. 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011, Bertinoro, Italy, June 13–18, 2011, Advanced Lectures, pp. 53–113, Springer, 2011. doi: 10.1007/978-3-642-21455-4_3.
• [23] Garavel H., Lang F.: Equivalence Checking 40 Years After: A Review of Bisimulation Tools. In: N. Jansen, M. Stoelinga, P. van den Bos (eds.),A Journey from Process Algebra via Timed Automata to Model Learning. Essays Dedicatedto Frits Vaandrager on the Occasion of His 60th Birthday, pp. 213–265, Springer,2022. doi: 10.1007/978-3-031-15629-8_13.
• [24] Groote J.F., Rivera Verduzco J., De Vink E.P.: An efficient algorithm to determine probabilistic bisimulation, Algorithms, vol. 11(9), 131, 2018. doi: 10.3390/a11090131.
• [25] Hansen H., Kwiatkowska M., Qu H.: Partial order reduction for model checking Markov decision processes under unconditional fairness. In: 2011 Eighth International Conference on Quantitative Evaluation of SysTems, pp. 203–212, IEEE,2011. doi: 10.1109/qest.2011.35.
• [26] Hensel C., Junges S., Katoen J.P., Quatmann T., Volk M.: The probabilistic model checker STORM, International Journal on Software Tools for Technology Transfer, vol. 24(4), pp. 589–610, 2022.
• [27] Jacobs J., Wißmann T.: Fast coalgebraic bisimilarity minimization, Proceedings of the ACM on Programming Languages, vol. 7(POPL), pp. 1514–1541, 2023.doi: 10.1145/3571245.
• [28] Kamaleson N.: Model reduction techniques for probabilistic verification of Markovchains, Ph.D. thesis, University of Birmingham, 2018.
• [29] Katoen J.P.: The probabilistic model checking landscape. In: LICS ’16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science,pp. 31–45, 2016. doi: 10.1145/2933575.2934574.
• [30] Klein J., Baier C., Chrszon P., Daum M., Dubslaff C., Klüppelholz S., Märcker S.,Müller D.: Advances in symbolic probabilistic model checking with PRISM. In: M. Chechik, J.-F. Raskin (eds.),Tools and Algorithms for the Construction and Analysis of Systems. 22nd International Conference, TACAS 2016, Held as Partof the European Joint Conferences on Theory and Practice of Software, ETAPS2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings, pp. 349–366, Springer, 2016. doi: 10.1007/978-3-662-49674-9_20.
• [31] Kwiatkowska M., Norman G., Parker D.: Symmetry reduction for probabilistic model checking. In: T. Ball, R.B. Jones (eds.), Computer Aided Verification.18th International Conference, CAV 2006, Seattle, WA, USA, August 17–20, 2006, Proceedings, pp. 234–248, Springer, 2006. doi: 10.1007/11817963_23.
• [32] Kwiatkowska M., Norman G., Parker D.: PRISM 4.0: Verification of probabilistic real-time systems. In: G. Gopalakrishnan, S. Qadeer (eds.), Computer Aided Verification. 23rd International Conference, CAV 2011, Snowbird, UT, USA,July 14–20, 2011, Proceedings, pp. 585–591, Springer, 2011. doi: 10.1007/978-3-642-22110-1_47.
• [33] Larsen K.G., Legay A.: Statistical model checking: Past, present, and future. In: T. Margaria, B. Steffen (eds.), Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I,pp. 3–15, Springer, 2016. doi: 10.1007/978-3-319-47166-2_1.
• [34] Larsen K.G., Skou A.: Bisimulation through probabilistic testing, Information and computation, vol. 94(1), 1991. doi: 10.1016/0890-5401(91)90030-6.
• [35] Mohagheghi M.: Probabilistic Bisimulation, https://github.com/sadeghrk/prism/tree/improved-bisimulation.
• [36] Mohagheghi M., Karimpour J., Isazadeh A.: Improving modified policy iteration for probabilistic model checking, Computer Science, vol. 23(1), 2022.doi: 10.7494/csci.2022.23.1.4139.
• [37] Mohagheghi M., Salehi K.: Improving Probabilistic Bisimulation for MDPs Using Machine Learning, Mathematics Interdisciplinary Research, vol. 9(2), pp. 151–169, 2024. doi: 10.22052/mir.2023.253367.1431.
• [38] Noroozi A.A., Karimpour J., Isazadeh A.: Bisimulation for Secure Information Flow Analysis of Multi-Threaded Programs, Mathematical and Computational Applications, vol. 24(2), 64, 2019. doi: 10.3390/mca24020064.
• [39] Parker D.A.: Implementation of symbolic model checking for probabilistic systems, Ph.D. thesis, University of Birmingham, 2003.
• [40] Philippou A., Lee I., Sokolsky O.: Weak bisimulation for probabilistic systems. In: C. Palamidessi (ed.), CONCUR 2000 – Concurrency Theory. 11th International Conference, University Park, PA, USA, August 22–25, 2000 Proceedings, pp. 334–349, Springer, 2000. doi: 10.1007/3-540-44618-4_25.
• [41] Salehi K., Noroozi A.A., Amir-Mohammadian S.: Quantifying information leak-age of probabilistic programs using the PRISM model checker. In: Proceedings of the 15th International Conference on Emerging Security Information, Systems and Technologies (SECURWARE 2021), pp. 47–52, 2021.
• [42] Salehi K., Noroozi A.A., Amir-Mohammadian S., Mohagheghi M.: An Automated Quantitative Information Flow Analysis for Concurrent Programs. In: E. Ábrahám, M. Paolieri (eds.), Quantitative Evaluation of Systems. 19th International Conference, QEST 2022, Warsaw, Poland, September 12–16, 2022, Proceedings, pp. 43–63, Springer, 2022. doi: 10.1007/978-3-031-16336-4_3.
• [43] Sanada T., Kojima R., Komorida Y., Muroya K., Hasuo I.: Explicit Hopcroft’s Trick in Categorical Partition Refinement. In: B. König, H. Urbat(eds.), Coalgebraic Methods in Computer Science. 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Luxembourg City, Luxembourg, April 6–7, 2024, Proceedings, pp. 135–155, 2024. doi: 10.1007/978-3-031-66438-0_7.
• [44] Segala R.: Modeling and verification of randomized distributed real-time systems, Ph.D. thesis, Massachusetts Institute of Technology, 1995.
• [45] Stoelinga M.I.A.: Alea jacta est: verification of probabilistic, real-time and parametric systems, Ph.D. thesis, Radboud University, Nijmegen, 2002

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa nr POPUL/SP/0154/2024/02 w ramach programu "Społeczna odpowiedzialność nauki II" - moduł: Popularyzacja nauki (2025).