Abstract
We consider parity games, a special form of two-player infinite-duration games on numerically labeled graphs, whose winning condition requires that the maximal value of a label occurring infinitely often during a play be of some specific parity. The problem of identifying the corresponding winning regions has a rather intriguing status from a complexity theoretic viewpoint, since it belongs to the class \({\textsc {UPTime}} \cap {\textsc {CoUPTime}}\), and still open is the question whether it can be solved in polynomial time. Parity games also have great practical interest, as they arise in many fields of theoretical computer science, most notably logic, automata theory, and formal verification. In this paper, we propose a new algorithm for the solution of this decision problem, based on the idea of promoting vertexes to higher priorities during the search for winning regions. The proposed approach has nice computational properties, exhibiting the best space complexity among the currently known solutions. Experimental results on both random games and benchmark families show that the technique is also very effective in practice.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Agrawal M, Kayal N, Saxena N (2004) PRIMES is in P. Ann Math 160(2):781–793
Alur R, Henzinger TA, Kupferman O (2002) Alternating-time temporal logic. J ACM 49(5):672–713
Apt K, Grädel E (2011) Lectures in game theory for computer scientists. Cambridge University Press, Cambridge
Benerecetti M, Dell’Erba D, Mogavero F (2016) Solving parity games via priority promotion. In Computer aided verification’16, LNCS 9780 (Part II). Springer, New York, pp 270–290
Benerecetti M, Mogavero F, Murano A (2013) Substructure temporal logic. In: Logic in computer science’13. IEEE Computer Society, pp 368–377
Benerecetti M, Mogavero F, Murano A (2015) Reasoning about substructures and games. Trans Comput Log 16(3):25:1–25:46
Berwanger D, Dawar A, Hunter P, Kreutzer S (2006) DAG-width and parity games. In: Symposium on theoretical aspects of computer science’06, LNCS 3884. Springer, New York, pp 524–536
Berwanger D, Grädel E (2001) Games and model checking for guarded logics. In: Logic for programming artificial intelligence and reasoning’01, LNCS 2250. Springer, New York, pp 70–84
Berwanger D, Grädel E (2004) Fixed-point logics and solitaire games. Theor Comput Sci 37(6):675–694
Berwanger D, Grädel E, Kaiser L, Rabinovich R (2012) Entanglement and the complexity of directed graphs. Theor Comput Sci 463:2–25
Calude CS, Jain S, Khoussainov B, Li W, Stephan F (2017) Deciding parity games in quasipolynomial time. In: Symposium on theory of computing’17. Association for Computing Machinery, pp 252–263
Chatterjee K, Doyen L (2012) Energy parity games. Theor Comput Sci 458:49–60
Chatterjee K, Doyen L, Henzinger TA, Raskin J-F (2010) Generalized mean-payoff and energy games. In Foundations of software technology and theoretical computer science’10, LIPIcs 8. Leibniz-Zentrum fuer Informatik, pp 505–516
Chatterjee K, Henzinger TA, Horn F (2010) Finitary winning in omega-regular games. Trans Comput Log 11(1):1:1–1:26
Chatterjee K, Henzinger TA, Jurdziński M (2005) Mean-payoff parity games. In: Logic in computer science’05. IEEE Computer Society, pp 178–187
Chatterjee K, Henzinger TA, Piterman N (2010) Strategy logic. Inf Comput 208(6):677–693
Condon A (1992) The complexity of stochastic games. Inf Comput 96(2):203–224
Ehrenfeucht A, Mycielski J (1979) Positional strategies for mean payoff games. Int J Game Theory 8(2):109–113
Emerson EA, Jutla CS (1991) Tree automata, mu-calculus, and determinacy. In: Foundation of computer science’91. IEEE Computer Society, pp 368–377
Emerson EA, Jutla CS, Sistla AP (1993) On model checking for the mu-calculus and its fragments. In: Computer aided verification’93, LNCS 697. Springer, New York, pp 385–396
Emerson EA, Jutla CS, Sistla AP (2001) On model checking for the \(\mu \)-calculus and its fragments. Theor Comput Sci 258(1–2):491–522
Emerson EA, Lei C-L (1986) Temporal reasoning under generalized fairness constraints. In: Symposium on theoretical aspects of computer science’86, LNCS 210. Springer, New York, pp 267–278
Fearnley J (2010) Non-oblivious strategy improvement. In: Logic for programming artificial intelligence and reasoning’10, LNCS 6355. Springer, New York, pp 212–230
Fearnley J, Jain S, Schewe S, Stephan F, Wojtczak D (2017) An ordered approach to solving parity games in quasi polynomial time and quasi linear space. In: SPIN symposium on model checking of software’2017. Association for Computing Machinery, pp 112–121
Fearnley J, Lachish O (2011) Parity games on graphs with medium tree-width. In: Mathematical foundations of computer science’11, LNCS 6907. Springer, New York, pp 303–314
Fearnley J, Schewe S (2012) Time and parallelizability results for parity games with bounded treewidth. In: International colloquium on automata, languages, and programming’12, LNCS 7392. Springer, pp 189–200
Fellows MR, Koblitz N (1992) Self-witnessing polynomial-time complexity and prime factorization. In: Conference on structure in complexity theory’92. IEEE Computer Society, pp 107–110
Fellows MR, Koblitz N (1992) Self-witnessing polynomial-time complexity and prime factorization. Des Codes Crypt 2(3):231–235
Fijalkow N, Zimmermann M (2012) Cost-parity and cost-streett games. In: Foundations of software technology and theoretical computer science’12, LIPIcs 18. Leibniz-Zentrum fuer Informatik, pp 124–135
Fijalkow N, Zimmermann M (2014) Cost-parity and cost-streett games. Log Methods Comput Sci 10(2):1–29
Friedmann O, Lange M (2009) Solving parity games in practice. In: Automated technology for verification and analysis’09, LNCS 5799. Springer, pp 182–196
Grädel E, Thomas W, Wilke T (2002) Automata, logics, and infinite games: a guide to current research. LNCS 2500. Springer, New York
Gurvich VA, Karzanov AV, Khachivan LG (1990) Cyclic games and an algorithm to find minimax cycle means in directed graphs. USSR Comput Math Math Phys 28(5):85–91
Jurdziński M (1998) Deciding the winner in parity games is in UP \(\cap \) co-UP. Inf Process Lett 68(3):119–124
Jurdziński M (2000) Small progress measures for solving parity games. In: Symposium on theoretical aspects of computer science’00, LNCS 1770. Springer, pp 290–301
Jurdziński M, Lazic R (2017) Succinct progress measures for solving parity games. In: Logic in computer science’17. Association for Computing Machinery. Accepted for publication, pp 1–9
Jurdziński M, Paterson M, Zwick U (2006) A deterministic subexponential algorithm for solving parity games. In: Symposium on discrete algorithms’06. Society for Industrial and Applied Mathematics, pp 117–123
Jurdziński M, Paterson M, Zwick U (2008) A Deterministic Subexponential Algorithm for Solving Parity Games. SIAM J Comput 38(4):1519–1532
Klarlund N, Kozen D (1991) Rabin measures and their applications to fairness and automata theory. In: Logic in computer science’91. IEEE Computer Society, pp 256–265
Kupferman O, Vardi MY (1998) Weak alternating automata and tree automata emptiness. In: Symposium on theory of computing’98. Association for Computing Machinery, pp 224–233
Martin AD (1975) Borel determinacy. Ann Math 102(2):363–371
Martin AD (1985) A purely inductive proof of Borel determinacy. In: Symposia in pure mathematics’82, recursion theory. American Mathematical Society and Association for Symbolic Logic, pp 303–308
McNaughton R (1993) Infinite games played on finite graphs. Ann Pure Appl Log 65:149–184
Mogavero F, Murano A, Perelli G, Vardi MY (2012) What makes ATL* decidable? A decidable fragment of strategy logic. In: Concurrency theory’12, LNCS 7454. Springer, Berlin, pp 193–208
Mogavero F, Murano A, Perelli G, Vardi MY (2014) Reasoning about strategies: on the model-checking problem. Trans Comput Log 15(4):341–3442
Mogavero F, Murano A, Sorrentino L (2013) On promptness in parity games. In: Logic for programming artificial intelligence and reasoning’13, LNCS 8312. Springer, New York, pp 601–618
Mogavero F, Murano A, Vardi MY (2010) Reasoning about strategies. In: Foundations of software technology and theoretical computer science’10, LIPIcs 8. Leibniz-Zentrum fuer Informatik, pp 133–144
Mostowski AW (1984) Regular expressions for infinite trees and a standard form of automata. In: Symposium on computation theory’84, LNCS 208. Springer, New York, pp 157–168
Mostowski AW (1991) Games with forbidden positions. Technical report, University of Gdańsk, Gdańsk, Poland
Obdrzálek J (2003) Fast mu-calculus model checking when tree-width is bounded. In: Computer aided verification’03, LNCS 2725. Springer, New York, pp 80–92
Obdrzálek J (2007) Clique-width and parity games. In: Computer science logic’07, LNCS 4646. Springer, New York, pp 54–68
Schewe S (2007) Solving parity games in big steps. In: Foundations of software technology and theoretical computer science’07, LNCS 4855. Springer, New York, pp 449–460
Schewe S (2008) An optimal strategy improvement algorithm for solving parity and payoff games. In: Computer science logic’08, LNCS 5213. Springer, New York, pp 369–384
Schewe S (2008) ATL* satisfiability is 2EXPTIME-complete. In: International colloquium on automata, languages, and programming’08, LNCS 5126. Springer, New York, pp 373–385
Schewe S, Finkbeiner B (2006) Satisfiability and finite model property for the alternating-time \(\mu \)-calculus. In: Computer science logic’06, LNCS 6247. Springer, New York, pp 591–605
Vöge J, Jurdziński M (2000) A discrete strategy improvement algorithm for solving parity games. In: Computer aided verification’00, LNCS 1855. Springer, New York, pp 202–215
Wilke T (2001) Alternating tree automata, parity games, and modal \(\mu \)-calculus. Bull Belg Math Soc 8(2):359–391
Zielonka W (1998) Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor Comput Sci 200(1–2):135–183
Zwick U, Paterson M (1996) The complexity of mean payoff games on graphs. Theor Comput Sci 158(1–2):343–359
Author information
Authors and Affiliations
Corresponding author
Additional information
This work is based on [4], which appeared in CAV’16.
Rights and permissions
About this article
Cite this article
Benerecetti, M., Dell’Erba, D. & Mogavero, F. Solving parity games via priority promotion. Form Methods Syst Des 52, 193–226 (2018). https://doi.org/10.1007/s10703-018-0315-1
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-018-0315-1