Abstract
The state space explosion problem is among the largest impediments to the performance of any model checker. Modelling languages for compositional systems contribute to this problem by placing each instruction of an instruction sequence onto a dedicated transition, giving concurrent processes opportunities to interleave after every instruction. Users wishing to avoid the excessive number of interleavings caused by this default can choose to explicitly declare instruction sequences as atomic, which however requires careful considerations regarding the impact this might have on the model as well as on the properties that are to be checked. We instead propose a preprocessing technique that automatically identifies instruction sequences that can safely be considered atomic. This is done in the context of concurrent variable-decorated Markov Decision Processes. Our approach is compatible with any off-the-shelf probabilistic model checker. We prove that our transformation preserves maximal reachability probabilities and present case studies to illustrate its usefulness.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Source sets: a foundation for optimal dynamic partial order reduction. J. ACM 64(4), 25:1–25:49 (2017). https://doi.org/10.1145/3073408
Baier, C., Grosser, M., Ciesinski, F.: Partial order reduction for probabilistic systems. In: 2004 Proceedings First International Conference on the Quantitative Evaluation of Systems, QEST 2004, pp. 230–239, September 2004. https://doi.org/10.1109/QEST.2004.1348037
Baier, C., D’Argenio, P., Groesser, M.: Partial order reduction for probabilistic branching time. Electron. Notes Theor. Comput. Sci. 153(2), 97–116 (2006). https://doi.org/10.1016/j.entcs.2005.10.034. Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL 2005)
Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 11–14 September 2006, Riverside, California, USA. pp. 125–126. IEEE Computer Society (2006). https://doi.org/10.1109/QEST.2006.59
Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.: 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
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984). https://doi.org/10.1145/828.833
D’Argenio, P.R., Niebert, P.: Partial order reduction on concurrent probabilistic programs. In: 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), 27–30 September 2004, Enschede, The Netherlands, pp. 240–249. IEEE Computer Society (2004). https://doi.org/10.1109/QEST.2004.1348038
Díaz, Á.F., Baier, C., Earle, C.B., Fredlund, L.: Static partial order reduction for probabilistic concurrent systems. In: Ninth International Conference on Quantitative Evaluation of Systems. QEST 2012, London, United Kingdom, 17–20 September 2012, pp. 104–113. IEEE Computer Society (2012). https://doi.org/10.1109/QEST.2012.22
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, 12–14 January 2005, Long Beach, California, USA, pp. 110–121. ACM (2005). https://doi.org/10.1145/1040305.1040315
Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 3–26. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68270-9_1
Giro, S., D’Argenio, P.R., Ferrer Fioriti, L.M.: Partial order reduction for probabilistic systems: a revision for distributed schedulers. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 338–353. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04081-8_23
Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-60761-7
Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.: A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods Syst. Des. 43(2), 191–232 (2013). https://doi.org/10.1007/s10703-012-0167-z
Hartmanns, A.: On the analysis of stochastic timed systems. Ph.D. thesis, Saarland University (2015). https://doi.org/10.22028/D291-26597
Hermanns, H., Kwiatkowska, M.Z., Norman, G., Parker, D., Siegle, M.: On the use of mtbdds for performability analysis and verification of stochastic systems. J. Log. Algebr. Program. 56(1–2), 23–67 (2003). https://doi.org/10.1016/S1567-8326(02)00066-8
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Katz, S., Peled, D.A.: Defining conditional independence using collapses. Theor. Comput. Sci. 101(2), 337–359 (1992). https://doi.org/10.1016/0304-3975(92)90054-J
Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-56922-7_34
Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1st edn. Wiley, New York (1994). https://doi.org/10.1002/9780470316887
Teige, T.: Stochastic satisfiability modulo theories: a symbolic technique for the analysis of probabilistic hybrid systems. Ph.D. thesis, Carl von Ossietzky University of Oldenburg (2012). https://oops.uni-oldenburg.de/id/eprint/1389
Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-53863-1_36
Acknowledgments
This work is partly supported by the DFG as part of CRC 248 (see perspicuous-computing.science) and by the ERC Advanced Investigators Grant 695614 (POWVER).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Fox, G., Stan, D., Hermanns, H. (2019). Syntactic Partial Order Compression for Probabilistic Reachability. In: Enea, C., Piskac, R. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2019. Lecture Notes in Computer Science(), vol 11388. Springer, Cham. https://doi.org/10.1007/978-3-030-11245-5_21
Download citation
DOI: https://doi.org/10.1007/978-3-030-11245-5_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-11244-8
Online ISBN: 978-3-030-11245-5
eBook Packages: Computer ScienceComputer Science (R0)