Abstract
It is well-known that the winning region of a parity game with n nodes and k priorities can be computed as a k-nested fixpoint of a suitable function; straightforward computation of this nested fixpoint requires \(\mathcal {O}(n^{\frac{k}{2}})\) iterations of the function. Calude et al.’s recent quasipolynomial-time parity game solving algorithm essentially shows how to compute the same fixpoint in only quasipolynomially many iterations by reducing parity games to quasipolynomially sized safety games. Universal graphs have been used to modularize this transformation of parity games to equivalent safety games that are obtained by combining the original game with a universal graph. We show that this approach naturally generalizes to the computation of solutions of systems of any fixpoint equations over finite lattices; hence, the solution of fixpoint equation systems can be computed by quasipolynomially many iterations of the equations. We present applications to modal fixpoint logics and games beyond relational semantics. For instance, the model checking problems for the energy \(\mu \)-calculus, finite latticed \(\mu \)-calculi, and the graded and the (two-valued) probabilistic \(\mu \)-calculus – with numbers coded in binary – can be solved via nested fixpoints of functions that differ substantially from the function for parity games but still can be computed in quasipolynomial time; our result hence implies that model checking for these \(\mu \)-calculi is in \(\textsc {QP}\). Moreover, we improve the exponent in known exponential bounds on satisfiability checking.
Work forms part of the DFG-funded project CoMoC (SCHR 1118/15-1, MI 717/7-1).
Chapter PDF
Similar content being viewed by others
Keywords
References
Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002), https://doi.org/10.1145/585265.585270
Amram, G., Maoz, S., Pistiner, O., Ringert, J.O.: Energy mu-calculus: Symbolic fixed-point algorithms for omega-regular energy games. CoRR abs/2005.00641 (2020), https://arxiv.org/abs/2005.00641
Arnold, A., Niwinski, D., Parys, P.: A quasi-polynomial black-box algorithm for fixed point evaluation. In: Computer Science Logic, CSL 2021. LIPIcs, vol. 183, pp. 9:1–9:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021), https://doi.org/10.4230/LIPIcs.CSL.2021.9
Baldan, P., König, B., Mika-Michalski, C., Padoan, T.: Fixpoint games on continuous lattices. In: Principles of Programming Languages, POPL 2021. Proceedings of the ACM on Programming Languages, vol. 3, pp. 26:1–26:29. ACM (2019), https://doi.org/10.1145/3290339
Bodlaender, H., Dinneen, M., Khoussainov, B.: On game-theoretic models of networks. In: Algorithms and Computation, ISAAC 2001. LNCS, vol. 2223, pp. 550–561. Springer (2001), https://doi.org/10.1007/3-540-45678-3_47
Boker, U., Lehtinen, K.: On the way to alternating weak automata. In: Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018. LIPIcs, vol. 122, pp. 21:1–21:22. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018), https://doi.org/10.4230/LIPIcs.FSTTCS.2018.21
Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: Automata, Languages and Programming, ICALP 2004. LNCS, vol. 3142, pp. 281–293. Springer (2004), https://doi.org/10.1007/978-3-540-27836-8_26
Bruse, F., Falk, M., Lange, M.: The fixpoint-iteration algorithm for parity games. In: Games, Automata, Logics and Formal Verification, GandALF 2014. EPTCS, vol. 161, pp. 116–130. Open Publishing Association (2014), https://doi.org/10.4204/EPTCS.161.12
Calude, C., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: Theory of Computing, STOC 2017. pp. 252–263. ACM (2017), https://doi.org/10.1145/3055399.3055409
Chatterjee, K., Doyen, L.: Energy parity games. Theor. Comput. Sci. 458, 49–60 (2012). https://doi.org/10.1016/j.tcs.2012.07.038
Chatterjee, K., Dvorák, W., Henzinger, M., Svozil, A.: Quasipolynomial set-based symbolic algorithms for parity games. In: Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2018. EPiC, vol. 57, pp. 233–253. EasyChair (2018), https://doi.org/10.29007/5z5k
Cîrstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic \(\mu \)-calculus. Log. Meth. Comput. Sci. 7 (2011), https://doi.org/10.2168/LMCS-7(3:3)2011
Colcombet, T., Fijalkow, N.: Universal graphs and good for games automata: New tools for infinite duration games. In: Foundations of Software Science and Computation Structures, FOSSACS 2019. LNCS, vol. 11425, pp. 1–26. Springer (2019), https://doi.org/10.1007/978-3-030-17127-8_1
Czerwinski, W., Daviaud, L., Fijalkow, N., Jurdzinski, M., Lazic, R., Parys, P.: Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. In: Symposium on Discrete Algorithms, SODA 2019. pp. 2333–2349. SIAM (2019), https://doi.org/10.1137/1.9781611975482.142
Daviaud, L., Jurdzinski, M., Lazic, R.: A pseudo-quasi-polynomial algorithm for mean-payoff parity games. In: Logic in Computer Science, LICS 2018. pp. 325–334. ACM (2018), https://doi.org/10.1145/3209108.3209162
Dawar, A., Grädel, E.: The descriptive complexity of parity games. In: Computer Science Logic, CSL 2008. LNCS, vol. 5213, pp. 354–368. Springer (2008), https://doi.org/10.1007/978-3-540-87531-4_26
Emerson, E.A., Jutla, C., Sistla, A.P.: On model checking for the \(\mu \)-calculus and its fragments. Theor. Comput. Sci. 258, 491–522 (2001), https://doi.org/10.1016/S0304-3975(00)00034-7
Enqvist, S., Seifan, F., Venema, Y.: Monadic second-order logic and bisimulation invariance for coalgebras. In: Logic in Computer Science, LICS 2015. pp. 353–365. IEEE (2015), https://doi.org/10.1109/LICS.2015.41
Fearnley, J., Jain, S., de Keijzer, B., Schewe, S., Stephan, F., Wojtczak, D.: An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space. STTT 21(3), 325–349 (2019), https://doi.org/10.1007/s10009-019-00509-3
Friedmann, O., Lange, M.: Deciding the unguarded modal \(\rm \mu \)-calculus. J. Appl. Non-Classical Log. 23, 353–371 (2013), https://doi.org/10.1080/11663081.2013.861181
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research, LNCS, vol. 2500. Springer (2002), https://doi.org/10.1007/3-540-36387-4
Hasuo, I., Shimizu, S., Cîrstea, C.: Lattice-theoretic progress measures and coalgebraic model checking. In: Principles of Programming Languages, POPL 2016. pp. 718–732. ACM (2016), https://doi.org/10.1145/2837614.2837673
Hausmann, D., Schröder, L.: Computing nested fixpoints in quasipolynomial time. CoRR abs/1907.07020 (2019), http://arxiv.org/abs/1907.07020
Hausmann, D., Schröder, L.: Game-based local model checking for the coalgebraic \(\mu \)-calculus. In: Concurrency Theory, CONCUR 2019. LIPIcs, vol. 140, pp. 35:1–35:16. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2019), https://doi.org/10.4230/LIPIcs.CONCUR.2019.35
Hausmann, D., Schröder, L.: Optimal satisfiability checking for arithmetic \(\mu \)-calculi. In: Foundations of Software Science and Computation Structures, FOSSACS 2019. LNCS, vol. 11425, pp. 277–294. Springer (2019), https://doi.org/10.1007/978-3-030-17127-8_16
Henzinger, T., Rajamani, S.: Fair bisimulation. In: Tools and Algorithms for Construction and Analysis of Systems, TACAS 2000. LNCS, vol. 1785, pp. 299–314. Springer (2000), https://doi.org/10.1007/3-540-46419-0_21
Jurdziński, M.: Small progress measures for solving parity games. In: Symposium on Theoretical Aspects of Computer Science, STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer (2000), https://doi.org/10.1007/3-540-46541-3_24
Jurdzinski, M., Lazic, R.: Succinct progress measures for solving parity games. In: Logic in Computer Science, LICS 2017. pp. 1–9. IEEE Computer Society (2017), https://doi.org/10.1109/LICS.2017.8005092
Kozen, D.: Results on the propositional \(\mu \)-calculus. Theor. Comput. Sci. 27, 333–354 (1983), https://doi.org/10.1016/0304-3975(82)90125-6
Kupferman, O., Lustig, Y.: Latticed simulation relations and games. In: Automated Technology for Verification and Analysis, ATVA 2007. LNCS, vol. 4762, pp. 316–330. Springer (2007), https://doi.org/10.1007/978-3-540-75596-8_23
Kupferman, O., Piterman, N., Vardi, M.: Fair equivalence relations. In: Verification: Theory and Practice. LNCS, vol. 2772, pp. 702–732. Springer (2003), https://doi.org/10.1007/978-3-540-39910-0_30
Kupferman, O., Sattler, U., Vardi, M.: The complexity of the graded \(\mu \)-calculus. In: Automated Deduction, CADE 2002. LNCS, vol. 2392, pp. 423–437. Springer (2002), https://doi.org/10.1007/3-540-45620-1_34
Lehtinen, K.: A modal \(\mu \) perspective on solving parity games in quasi-polynomial time. In: Logic in Computer Science, LICS 2018. pp. 639–648. ACM (2018), https://doi.org/10.1145/3209108.3209115
Liu, W., Song, L., Wang, J., Zhang, L.: A simple probabilistic extension of modal mu-calculus. In: International Joint Conference on Artificial Intelligence, IJCAI 2015. pp. 882–888. AAAI Press (2015), http://ijcai.org/proceedings/2015
Long, D.E., Browne, A., Clarke, E.M., Jha, S., Marrero, W.R.: An improved algorithm for the evaluation of fixpoint expressions. In: Computer Aided Verification, CAV 1994. LNCS, vol. 818, pp. 338–350. Springer (1994), https://doi.org/10.1007/3-540-58179-0_66
Mio, M.: On the equivalence of game and denotational semantics for the probabilistic \(\mu \)-calculus. Log. Methods Comput. Sci. 8 (2012), https://doi.org/10.2168/LMCS-8(2:7)2012
Parikh, R.: The logic of games and its applications. Ann. Discr. Math. 24, 111–140 (1985), https://doi.org/10.1016/S0304-0208(08)73078-0
Parys, P.: Parity games: Zielonka’s algorithm in quasi-polynomial time. In: Mathematical Foundations of Computer Science, MFCS 2019. LIPIcs, vol. 138, pp. 10:1–10:13. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019), https://doi.org/10.4230/LIPIcs.MFCS.2019.10
Peleg, D.: Concurrent dynamic logic. J. ACM 34, 450–479 (1987), https://doi.org/10.1145/23005.23008.
Rutten, J.: Universal coalgebra: A theory of systems. Theor. Comput. Sci. 249, 3–80 (2000), https://doi.org/10.1016/S0304-3975(00)00056-6
Seidl, H.: Fast and Simple Nested Fixpoints. Inf. Process. Lett. 59, 303–308 (1996), https://doi.org/10.1016/0020-0190(96)00130-5
Venema, Y.: Lectures on the modal \(\mu \)-calculus. Lecture notes, Institute for Logic, Language and Computation, Universiteit van Amsterdam (2008), https://staff.fnwi.uva.nl/y.venema/teaching/ml/notes/20201212-mu.pdf
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
© 2021 The Author(s)
About this paper
Cite this paper
Hausmann, D., Schröder, L. (2021). Quasipolynomial Computation of Nested Fixpoints. In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12651. Springer, Cham. https://doi.org/10.1007/978-3-030-72016-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-72016-2_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72015-5
Online ISBN: 978-3-030-72016-2
eBook Packages: Computer ScienceComputer Science (R0)