Parity Games: Another View on Lehtinen’s Algorithm

Author Paweł Parys

Thumbnail PDF


  • Filesize: 490 kB
  • 15 pages

Document Identifiers

Author Details

Paweł Parys
  • Institute of Informatics, University of Warsaw, Poland

Cite AsGet BibTex

Paweł Parys. Parity Games: Another View on Lehtinen’s Algorithm. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Recently, five quasi-polynomial-time algorithms solving parity games were proposed. We elaborate on one of the algorithms, by Lehtinen (2018). Czerwiński et al. (2019) observe that four of the algorithms can be expressed as constructions of separating automata (of quasi-polynomial size), that is, automata that accept all plays decisively won by one of the players, and rejecting all plays decisively won by the other player. The separating automata corresponding to three of the algorithms are deterministic, and it is clear that deterministic separating automata can be used to solve parity games. The separating automaton corresponding to the algorithm of Lehtinen is nondeterministic, though. While this particular automaton can be used to solve parity games, this is not true for every nondeterministic separating automaton. As a first (more conceptual) contribution, we specify when a nondeterministic separating automaton can be used to solve parity games. We also repeat the correctness proof of the Lehtinen’s algorithm, using separating automata. In this part, we prove that her construction actually leads to a faster algorithm than originally claimed in her paper: its complexity is n^{O(log n)} rather than n^{O(log d ⋅ log n)} (where n is the number of nodes, and d the number of priorities of a considered parity game), which is similar to complexities of the other quasi-polynomial-time algorithms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Algorithmic game theory
  • Parity games
  • quasi-polynomial time
  • separating automata
  • good-for-games automata


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Massimo Benerecetti, Daniele Dell'Erba, and Fabio Mogavero. Solving parity games via priority promotion. Formal Methods in System Design, 52(2):193-226, 2018. URL:
  2. Julien Bernet, David Janin, and Igor Walukiewicz. Permissive strategies: From parity games to safety games. ITA, 36(3):261-275, 2002. URL:
  3. Henrik Björklund and Sergei G. Vorobyov. A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. Discrete Applied Mathematics, 155(2):210-229, 2007. URL:
  4. Mikołaj Bojańczyk and Wojciech Czerwiński. An Automata Toolbox, February 2018. URL:
  5. Anca Browne, Edmund M. Clarke, Somesh Jha, David E. Long, and Wilfredo R. Marrero. An Improved Algorithm for the Evaluation of Fixpoint Expressions. Theor. Comput. Sci., 178(1-2):237-255, 1997. URL:
  6. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Hamed Hatami, Pierre McKenzie, and Valerie King, editors, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017, pages 252-263. ACM, 2017. URL:
  7. Thomas Colcombet and Nathanaël Fijalkow. Universal Graphs and Good for Games Automata: New Tools for Infinite Duration Games. In Mikołaj Bojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11425 of Lecture Notes in Computer Science, pages 1-26. Springer, 2019. URL:
  8. Anne Condon. The Complexity of Stochastic Games. Inf. Comput., 96(2):203-224, 1992. URL:
  9. Wojciech Czerwiński, Laure Daviaud, Nathanaël Fijalkow, Marcin Jurdziński, Ranko Lazić, and Paweł Parys. Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. In Timothy M. Chan, editor, Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2019, San Diego, California, USA, January 6-9, 2019, pages 2333-2349. SIAM, 2019. URL:
  10. Constantinos Daskalakis and Christos H. Papadimitriou. Continuous Local Search. In Dana Randall, editor, Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2011, San Francisco, California, USA, January 23-25, 2011, pages 790-804. SIAM, 2011. URL:
  11. E. Allen Emerson and Charanjit S. Jutla. Tree Automata, Mu-Calculus and Determinacy (Extended Abstract). In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, pages 368-377. IEEE Computer Society, 1991. URL:
  12. E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model checking for the μ-calculus and its fragments. Theor. Comput. Sci., 258(1-2):491-522, 2001. URL:
  13. John Fearnley. Exponential Lower Bounds for Policy Iteration. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 551-562. Springer, 2010. URL:
  14. John Fearnley, Sanjay Jain, Sven Schewe, Frank Stephan, and Dominik Wojtczak. An ordered approach to solving parity games in quasi polynomial time and quasi linear space. In Hakan Erdogmus and Klaus Havelund, editors, Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, Santa Barbara, CA, USA, July 10-14, 2017, pages 112-121. ACM, 2017. URL:
  15. Wladimir Fridman and Martin Zimmermann. Playing Pushdown Parity Games in a Hurry. In Marco Faella and Aniello Murano, editors, Proceedings Third International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2012, Napoli, Italy, September 6-8, 2012., volume 96 of EPTCS, pages 183-196, 2012. URL:
  16. Oliver Friedmann, Thomas Dueholm Hansen, and Uri Zwick. Subexponential lower bounds for randomized pivoting rules for the simplex algorithm. In Lance Fortnow and Salil P. Vadhan, editors, Proceedings of the 43rd ACM Symposium on Theory of Computing, STOC 2011, San Jose, CA, USA, 6-8 June 2011, pages 283-292. ACM, 2011. URL:
  17. Hugo Gimbert and Rasmus Ibsen-Jensen. A short proof of correctness of the quasi-polynomial time algorithm for parity games. CoRR, abs/1702.01953, 2017. URL:
  18. Matthew Hague, Roland Meyer, Sebastian Muskalla, and Martin Zimmermann. Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems. In Igor Potapov, Paul G. Spirakis, and James Worrell, editors, 43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018, August 27-31, 2018, Liverpool, UK, volume 117 of LIPIcs, pages 57:1-57:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL:
  19. Thomas A. Henzinger and Nir Piterman. Solving Games Without Determinization. In Zoltán Ésik, editor, Computer Science Logic, volume 4207 of Lecture Notes in Computer Science, pages 395-410, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL:
  20. Marcin Jurdziński. Deciding the Winner in Parity Games is in UP ∩ co-UP. Inf. Process. Lett., 68(3):119-124, 1998. URL:
  21. Marcin Jurdziński. Small Progress Measures for Solving Parity Games. In Horst Reichel and Sophie Tison, editors, STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Lille, France, February 2000, Proceedings, volume 1770 of Lecture Notes in Computer Science, pages 290-301. Springer, 2000. URL:
  22. Marcin Jurdziński and Ranko Lazić. Succinct progress measures for solving parity games. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-9. IEEE Computer Society, 2017. URL:
  23. Marcin Jurdziński, Mike Paterson, and Uri Zwick. A Deterministic Subexponential Algorithm for Solving Parity Games. SIAM J. Comput., 38(4):1519-1532, 2008. URL:
  24. Bakhadyr Khoussainov. A Brief Excursion to Parity Games. In Mizuho Hoshi and Shinnosuke Seki, editors, Developments in Language Theory - 22nd International Conference, DLT 2018, Tokyo, Japan, September 10-14, 2018, Proceedings, volume 11088 of Lecture Notes in Computer Science, pages 24-35. Springer, 2018. URL:
  25. Karoliina Lehtinen. A modal μ perspective on solving parity games in quasi-polynomial time. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 639-648. ACM, 2018. URL:
  26. Andrzej W. Mostowski. Games with forbidden positions. Technical Report 78, Uniwersytet Gdański, 1991. Google Scholar
  27. Paweł Parys. Parity Games: Zielonka’s Algorithm in Quasi-Polynomial Time. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 10:1-10:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL:
  28. Michael Oser Rabin. Automata on Infinite Objects and Church’s Problem. American Mathematical Society, Boston, MA, USA, 1972. Google Scholar
  29. Sven Schewe. Solving parity games in big steps. J. Comput. Syst. Sci., 84:243-262, 2017. URL:
  30. Helmut Seidl. Fast and Simple Nested Fixpoints. Inf. Process. Lett., 59(6):303-308, 1996. URL:
  31. Jens Vöge and Marcin Jurdziński. A Discrete Strategy Improvement Algorithm for Solving Parity Games. In E. Allen Emerson and A. Prasad Sistla, editors, Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, volume 1855 of Lecture Notes in Computer Science, pages 202-215. Springer, 2000. URL:
  32. Wiesław Zielonka. Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees. Theor. Comput. Sci., 200(1-2):135-183, 1998. URL:
  33. Uri Zwick and Mike Paterson. The Complexity of Mean Payoff Games on Graphs. Theor. Comput. Sci., 158(1&2):343-359, 1996. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail