Abstract
Parity games can be used to represent many different kinds of decision problems. In practice, tools that use parity games often rely on a specification in a higher-order logic from which the actual game can be obtained by means of an exploration. For many of these decision problems we are only interested in the solution for a designated vertex in the game. We formalise how to use on-the-fly solving techniques during the exploration process, and show that this can help to decide the winner of such a designated vertex in an incomplete game. Furthermore, we define partial solving techniques for incomplete parity games and show how these can be made resilient to work directly on the incomplete game, rather than on a set of safe vertices. We implement our techniques for symbolic parity games and study their effectiveness in practice, showing that speed-ups of several orders of magnitude are feasible and overhead (if unavoidable) is typically low.
Chapter PDF
Similar content being viewed by others
References
Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Hu, A., Vardi, M. (eds.) CAV. LNCS, vol. 1427, pp. 184–194. Springer (1998). https://doi.org/10.1007/BFb0028744
Benerecetti, M., Dell’Erba, D., Mogavero, F.: Solving parity games via priority promotion. Formal Methods Syst. Des. 52(2), 193–226 (2018). https://doi.org/10.1007/s10703-018-0315-1
Blom, S., Groote, J.F., Mauw, S., Serebrenik, A.: Analysing the BKE-security protocol with \(\rm {\mu }\)CRL. Electron. Notes Theor. Comput. Sci. 139(1), 49–90 (2005). https://doi.org/10.1016/j.entcs.2005.09.005
Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P.B. (eds.) CAV. LNCS, vol. 6174, pp. 354–359. Springer (2010). https://doi.org/10.1007/978-3-642-14295-6_31
Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992). https://doi.org/10.1145/136035.136043
Bunte, O., Groote, J.F., Keiren, J.J.A., Laveaux, M., Neele, T., de Vink, E.P., Wesselink, W., Wijs, A., Willemse, T.A.C.: The mCRL2 toolset for analysing concurrent systems - improvements in expressivity and usability. In: Vojnar, T., Zhang, L. (eds.) TACAS. LNCS, vol. 11428, pp. 21–39. Springer (2019). https://doi.org/10.1007/978-3-030-17465-1_2
Calude, C.S., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: Hatami, H., McKenzie, P., King, V. (eds.) STOC. pp. 252–263. ACM (2017). https://doi.org/10.1145/3055399.3055409
Chen, T., Ploeger, B., van de Pol, J., Willemse, T.A.C.: Equivalence checking for infinite systems using parameterized Boolean equation systems. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR. LNCS, vol. 4703, pp. 120–135. Springer (2007). https://doi.org/10.1007/978-3-540-74407-8_9
Ciardo, G., Marmorstein, R.M., Siminiceanu, R.: The saturation algorithm for symbolic state-space exploration. Int. J. Softw. Tools Technol. Transf. 8(1), 4–25 (2006). https://doi.org/10.1007/s10009-005-0188-7
Cleaveland, R., Klein, M., Steffen, B.: Faster model checking for the modal mu-calculus. In: von Bochmann, G., Probst, D.K. (eds.) CAV. LNCS, vol. 663, pp. 410–422. Springer (1992). https://doi.org/10.1007/3-540-56496-9_32
Cranen, S., Luttik, B., Willemse, T.A.C.: Proof graphs for parameterised Boolean equation systems. In: D’Argenio, P.R., Melgratti, H.C. (eds.) CONCUR. LNCS, vol. 8052, pp. 470–484. Springer (2013). https://doi.org/10.1007/978-3-642-40184-8_33
van Dijk, T.: Oink: An implementation and evaluation of modern parity game solvers. In: Beyer, D., Huisman, M. (eds.) TACAS. LNCS, vol. 10805, pp. 291–308. Springer (2018). https://doi.org/10.1007/978-3-319-89960-2_16
van Dijk, T., van de Pol, J.: Sylvan: multi-core framework for decision diagrams. Int. J. Softw. Tools Technol. Transf. 19(6), 675–696 (2017). https://doi.org/10.1007/s10009-016-0433-2
Eiríksson, Á.T., McMillan, K.L.: Using formal verification/analysis methods on the critical path in system design: A case study. In: Wolper, P. (ed.) CAV. LNCS, vol. 939, pp. 367–380. Springer (1995). https://doi.org/10.1007/3-540-60045-0_63
Groote, J.F., Willemse, T.A.C.: Model-checking processes with data. Sci. Comput. Program. 56(3), 251–273 (2005). https://doi.org/10.1016/j.scico.2004.08.002
Groote, J.F., Willemse, T.A.C.: Parameterised Boolean equation systems. Theor. Comput. Sci. 343(3), 332–369 (2005). https://doi.org/10.1016/j.tcs.2005.06.016
Huth, M., Kuo, J.H., Piterman, N.: Fatal attractors in parity games. In: Pfenning, F. (ed.) FOSSACS. LNCS, vol. 7794, pp. 34–49. Springer (2013). https://doi.org/10.1007/978-3-642-37075-5_3
Jurdziński, M., Lazić, R.: Succinct progress measures for solving parity games. In: LICS. pp. 1–9. IEEE Computer Society (2017). https://doi.org/10.1109/LICS.2017.8005092
Kant, G., van de Pol, J.: Efficient instantiation of parameterised Boolean equation systems to parity games. In: Wijs, A., Bosnacki, D., Edelkamp, S. (eds.) GRAPHITE. EPTCS, vol. 99, pp. 50–65 (2012). https://doi.org/10.4204/EPTCS.99.7
Kant, G., van de Pol, J.: Generating and solving symbolic parity games. In: Bosnacki, D., Edelkamp, S., Lluch-Lafuente, A., Wijs, A. (eds.) GRAPHITE. EPTCS, vol. 159, pp. 2–14 (2014). https://doi.org/10.4204/EPTCS.159.2
Laveaux, M.: Downloadable sources for the case study (2022). https://doi.org/10.5281/zenodo.5896966
Laveaux, M., Wesselink, W., Willemse, T.A.C.: On-the-fly solving for symbolic parity games. CoRR abs/2201.09607 (2022), https://arxiv.org/abs/2201.09607
Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci. Comput. Program. 46(3), 255–281 (2003). https://doi.org/10.1016/S0167-6423(02)00094-1
McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Logic 65(2), 149–184 (1993). https://doi.org/10.1016/0168-0072(93)90036-D
Miller, D.M.: Multiple-valued logic design tools. In: ISMVL. pp. 2–11. IEEE Computer Society (1993). https://doi.org/10.1109/ISMVL.1993.289589
Pang, J., Fokkink, W.J., Hofman, R.F.H., Veldema, R.: Model checking a cache coherence protocol of a java DSM implementation. J. Log. Algebraic Methods Program. 71(1), 1–43 (2007). https://doi.org/10.1016/j.jlap.2006.08.007
Remenska, D., Willemse, T.A.C., Verstoep, K., Templon, J., Bal, H.E.: Using model checking to analyze the system behavior of the LHC production grid. Future Gener. Comput. Syst. 29(8), 2239–2251 (2013). https://doi.org/10.1016/j.future.2013.06.004
Sanchez, L., Wesselink, W., Willemse, T.A.C.: A comparison of BDD-based parity game solvers. In: Orlandini, A., Zimmermann, M. (eds.) GandALF. EPTCS, vol. 277, pp. 103–117 (2018). https://doi.org/10.4204/EPTCS.277.8
Stasio, A.D., Murano, A., Vardi, M.Y.: Solving parity games: Explicit vs symbolic. In: Câmpeanu, C. (ed.) CIAA. LNCS, vol. 10977, pp. 159–172. Springer (2018). https://doi.org/10.1007/978-3-319-94812-6_14
Tanenbaum, A.S., Wetherall, D.: Computer networks, 5th Edition. Pearson (2011), https://www.worldcat.org/oclc/698581231
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1-2), 135–183 (1998). https://doi.org/10.1016/S0304-3975(98)00009-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
© 2022 The Author(s)
About this paper
Cite this paper
Laveaux, M., Wesselink, W., Willemse, T.A.C. (2022). On-The-Fly Solving for Symbolic Parity Games. In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol 13244. Springer, Cham. https://doi.org/10.1007/978-3-030-99527-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-99527-0_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99526-3
Online ISBN: 978-3-030-99527-0
eBook Packages: Computer ScienceComputer Science (R0)