Abstract
Partial-order reduction (POR) is a well-established technique to combat the problem of state-space explosion. We propose POR techniques that are sound for parity games, a well-established formalism for solving a variety of decision problems. As a consequence, we obtain the first POR method that is sound for model checking for the full modal \(\mu \)-calculus. Our technique is applied to, and implemented for the fixed point logic called parameterised Boolean equation systems, which provides a high-level representation of parity games. Experiments indicate that substantial reductions can be achieved.
Chapter PDF
Similar content being viewed by others
References
Anderson, T.E.: The Performance of Spin Lock Alternatives for Shared-Memory Multiprocessors. IEEE Transactions on Parallel & Distributed Systems 1(1), 6–16 (1990). https://doi.org/10.1109/71.80120
Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)
Bønneland, F.M., Jensen, P.G., Larsen, K.G., Muñiz, M.: Partial Order Reduction for Reachability Games. In: CONCUR 2019. vol. 140, pp. 23:1–23:15 (2019). https://doi.org/10.4230/LIPIcs.CONCUR.2019.23
Bønneland, F.M., Jensen, P.G., Larsen, K.G., Mũniz, M., Srba, J.: Stubborn Set Reduction for Two-Player Reachability Games. arXiv:1912.09875 (2019)
Bunte, O., Groote, J.F., Keiren, J.J.A., Laveaux, M., Neele, T., de Vink, E.P., Wesselink, J.W., Wijs, A.W., Willemse, T.A.C.: The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability. In: TACAS 2019. LNCS, vol. 11428, pp. 21–39 (2019). https://doi.org/10.1007/978-3-030-17465-1_2
Cranen, S., Luttik, B., Willemse, T.A.C.: Proof graphs for parameterised Boolean equation systems. In: CONCUR 2013. LNCS, vol. 8052, pp. 470–484 (2013). https://doi.org/10.1007/978-3-642-40184-8_33
Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A Partial Order Approach to Branching Time Logic Model Checking. Information and Computation 150(2), 132–152 (1999). https://doi.org/10.1006/inco.1998.2778
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems, LNCS, vol. 1032. Springer (1996). https://doi.org/10.1007/3-540-60761-7
Groote, J.F., Sellink, M.P.A.: Confluence for process verification. Theoretical Computer Science 170(1-2), 47–81 (1996). https://doi.org/10.1016/s0304-3975(96)00175-2
Groote, J.F., Willemse, T.A.C.: Parameterised boolean equation systems. Theoretical Computer Science 343(3), 332–369 (2005). https://doi.org/10.1016/j.tcs.2005.06.016
Heimbold, D., Luckham, D.: Debugging ada tasking programs. IEEE Software 2(2), 47–57 (1985). https://doi.org/10.1109/MS.1985.230351
Hesselink, W.H.: Invariants for the construction of a handshake register. Inf. Process. Lett. 68(4), 173–177 (1998). https://doi.org/10.1016/S0020-0190(98)00158-6
Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design 9(1-2), 41–75 (1996). https://doi.org/10.1007/BF00625968
Kan, S., Huang, Z., Chen, Z., Li, W., Huang, Y.: Partial order reduction for checking LTL formulae with the next-time operator. Journal of Logic and Computation 27(4), 1095–1131 (2017). https://doi.org/10.1093/logcom/exw004
Keiren, J.J.A., Wesselink, J.W., Willemse, T.A.C.: Liveness Analysis for Parameterised Boolean Equation Systems. In: ATVA 2014. LNCS, vol. 8837, pp. 219–234 (2014). https://doi.org/10.1007/978-3-319-11936-6_16
Kozen, D.: Results on the propositional \(\mu \)-calculus. Theoretical Computer Science 27(3), 333–354 (1982). https://doi.org/10.1016/0304-3975(82)90125-6
Laarman, A., Pater, E., van de Pol, J., Hansen, H.: Guard-based partial-order reduction. STTT 18(4), 427–448 (2016). https://doi.org/10.1007/s10009-014-0363-9
Lann, G.L.: Distributed systems - towards a formal approach. IFIP 1977, 155–160 (1977)
Liebke, T., Wolf, K.: Taking Some Burden Off an Explicit CTL Model Checker. In: Petri Nets 2019. LNCS, vol. 11522, pp. 321–341 (2019). https://doi.org/10.1007/978-3-030-21571-2_18
Milner, R.: A Calculus of Communicating Systems, LNCS, vol. 92. Springer (1980)
Neele, T., Valmari, A., Willemse, T.A.C.: The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction. In: FoSSaCS 2020. LNCS, vol. 2077 (2020). https://doi.org/10.1007/978-3-030-45231-5_25
Neele, T., Willemse, T.A.C., Groote, J.F.: Solving Parameterised Boolean Equation Systems with Infinite Data Through Quotienting. In: FACS 2018. LNCS, vol. 11222, pp. 216–236 (2018). https://doi.org/10.1007/978-3-030-02146-7_11
Neele, T., Willemse, T.A.C., Groote, J.F.: Finding compact proofs for infinite-data parameterised Boolean equation systems. Science of Computer Programming 188, 102389 (2020). https://doi.org/10.1016/j.scico.2019.102389
Neele, T., Willemse, T.A.C., Wesselink, W.: Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems (Technical Report). Tech. rep., Eindhoven University of Technology (2019)
Pelánek, R.: BEEM: Benchmarks for Explicit Model Checkers. In: SPIN 2007. LNCS, vol. 4595, pp. 263–267 (2007). https://doi.org/10.1007/978-3-540-73370-6_17
Peled, D.: All from One, One for All: on Model Checking Using Representatives. In: CAV 1993. LNCS, vol. 697, pp. 409–423 (1993). https://doi.org/10.1007/3-540-56922-7_34
Peled, D.: Combining partial order reductions with on-the-fly model-checking. FMSD 8(1), 39–64 (1996). https://doi.org/10.1007/BF00121262
Ramakrishna, Y.S., Smolka, S.A.: Partial-Order Reduction in the Weak Modal Mu-Calculus. In: CONCUR 1997. LNCS, vol. 1243, pp. 5–24 (1997). https://doi.org/10.1007/3-540-63141-0_2
Siegel, S.F.: What’s Wrong with On-the-Fly Partial Order Reduction. In: CAV 2019. LNCS, vol. 11562, pp. 478–495 (2019). https://doi.org/10.1007/978-3-030-25543-5_27
Valmari, A.: A Stubborn Attack on State Explosion. Formal Methods in System Design 1(4), 297–322 (1992). https://doi.org/10.1007/BF00709154
Valmari, A.: The state explosion problem. In: ACPN 1996. LNCS, vol. 1491, pp. 429–528 (1996). https://doi.org/10.1007/3-540-65306-6_21
Valmari, A.: Stubborn Set Methods for Process Algebras. In: POMIV 1996. DIMACS, vol. 29, pp. 213–231 (1997). https://doi.org/10.1090/dimacs/029/12
Valmari, A., Hansen, H.: Stubborn Set Intuition Explained. ToPNoC 10470(12), 140–165 (2017). https://doi.org/10.1007/978-3-662-55862-1_7
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Neele, T., Willemse, T.A.C., Wesselink, W. (2020). Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12079. Springer, Cham. https://doi.org/10.1007/978-3-030-45237-7_19
Download citation
DOI: https://doi.org/10.1007/978-3-030-45237-7_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45236-0
Online ISBN: 978-3-030-45237-7
eBook Packages: Computer ScienceComputer Science (R0)
