Beyond Value Iteration for Parity Games: Strategy Iteration with Universal Trees
Parity games have witnessed several new quasi-polynomial algorithms since the breakthrough result of Calude et al. (STOC 2017). The combinatorial object underlying these approaches is a universal tree, as identified by Czerwiński et al. (SODA 2019). By proving a quasi-polynomial lower bound on the size of a universal tree, they have highlighted a barrier that must be overcome by all existing approaches to attain polynomial running time. This is due to the existence of worst case instances which force these algorithms to explore a large portion of the tree.
As an attempt to overcome this barrier, we propose a strategy iteration framework which can be applied on any universal tree. It is at least as fast as its value iteration counterparts, while allowing one to take bigger leaps in the universal tree. Our main technical contribution is an efficient method for computing the least fixed point of 1-player games. This is achieved via a careful adaptation of shortest path algorithms to the setting of ordered trees. By plugging in the universal tree of Jurdziński and Lazić (LICS 2017), or the Strahler universal tree of Daviaud et al. (ICALP 2020), we obtain instantiations of the general framework that take time O(mn²log nlog d) and O(mn²log³ n log d) respectively per iteration.
parity games
strategy iteration
value iteration
progress measure
universal trees
Theory of computation~Design and analysis of algorithms
Theory of computation~Logic and verification
Mathematics of computing~Discrete mathematics
63:1-63:15
Regular Paper
This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 757481-ScaleOpt).
https://arxiv.org/abs/2108.13338
We are grateful for the helpful comments and support by L{á}szló A. Végh. We would also like to thank Xavier Allamigeon, Nathanaël Fijalkow and Marcin Jurdzi{ń}ski for inspiring discussions.
Zhuan Khye
Koh
Zhuan Khye Koh
Department of Mathematics, London School of Economics and Political Science, United Kingdom
https://personal.lse.ac.uk/kohz3/
https://orcid.org/0000-0002-4450-8506
Georg
Loho
Georg Loho
Discrete Mathematics and Mathematical Programming, University of Twente, The Netherlands
https://lohomath.github.io/
https://orcid.org/0000-0001-6500-385X
10.4230/LIPIcs.MFCS.2022.63
Ravindra K. Ahuja, Thomas L. Magnanti, and James B. Orlin. Network flows. Theory, algorithms, and applications. Englewood Cliffs, NJ: Prentice Hall, 1993.
Massimo Benerecetti, Daniele Dell'Erba, and Fabio Mogavero. Solving parity games via priority promotion. Formal Methods Syst. Des., 52(2):193-226, 2018.
Massimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero, Sven Schewe, and Dominik Wojtczak. Priority promotion with parysian flair. arXiv, abs/2105.01738, 2021. URL: http://arxiv.org/abs/2105.01738.
http://arxiv.org/abs/2105.01738
Henrik Björklund, Sven Sandberg, and Sergei G. Vorobyov. A discrete subexponential algorithm for parity games. In 20th Annual Symposium on Theoretical Aspects of Computer Science, STACS, volume 2607 of Lecture Notes in Computer Science, pages 663-674, 2003.
Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC, pages 252-263, 2017.
Wojciech Czerwinski, Laure Daviaud, Nathanaël Fijalkow, Marcin Jurdzinski, Ranko Lazic, and Pawel Parys. Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. In Proceedings of the 30th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA, pages 2333-2349, 2019.
Laure Daviaud, Marcin Jurdzinski, and K. S. Thejaswini. The strahler number of a parity game. In 47th International Colloquium on Automata, Languages, and Programming, ICALP, volume 168 of LIPIcs, pages 123:1-123:19, 2020.
E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy. In 32nd Annual Symposium on Foundations of Computer Science, FOCS, pages 368-377, 1991.
E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model-checking for fragments of μ-calculus. In 5th International Conference on Computer-Aided Verification, CAV, volume 697 of Lecture Notes in Computer Science, pages 385-396, 1993.
John Fearnley, Sanjay Jain, Bart de Keijzer, Sven Schewe, Frank Stephan, and Dominik Wojtczak. An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space. Int. J. Softw. Tools Technol. Transf., 21(3):325-349, 2019.
Oliver Friedmann. An exponential lower bound for the parity game strategy improvement algorithm as we know it. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS, pages 145-156, 2009.
Oliver Friedmann. Exponential Lower Bounds for Solving Infinitary Payoff Games and Linear Programs. PhD thesis, University of Munich, 2011. URL: http://files.oliverfriedmann.de/theses/phd.pdf.
http://files.oliverfriedmann.de/theses/phd.pdf
A. J. Hoffman and R. M. Karp. On nonterminating stochastic games. Manage. Sci., 12(5):359-370, 1966.
Marcin Jurdzinski. Deciding the winner in parity games is in UP ∩ co-UP. Inf. Process. Lett., 68(3):119-124, 1998.
Marcin Jurdzinski. Small progress measures for solving parity games. In 17th Annual Symposium on Theoretical Aspects of Computer Science, STACS, volume 1770 of Lecture Notes in Computer Science, pages 290-301, 2000.
Marcin Jurdzinski and Ranko Lazic. Succinct progress measures for solving parity games. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 1-9, 2017.
Marcin Jurdzinski, Mike Paterson, and Uri Zwick. A deterministic subexponential algorithm for solving parity games. SIAM J. Comput., 38(4):1519-1532, 2008.
Orna Kupferman and Moshe Y. Vardi. Weak alternating automata and tree automata emptiness. In Proceedings of the Thirtieth Annual ACM Symposium on Theory of Computing, STOC '98, pages 224-233, New York, NY, USA, 1998. Association for Computing Machinery. URL: https://doi.org/10.1145/276698.276748.
https://doi.org/10.1145/276698.276748
Karoliina Lehtinen. A modal μ perspective on solving parity games in quasi-polynomial time. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 639-648, 2018.
Matthias Mnich, Heiko Röglin, and Clemens Rösner. New deterministic algorithms for solving parity games. Discret. Optim., 30:73-95, 2018.
Pierre Ohlmann. Monotonic Graphs for Parity and Mean-Payoff Games. PhD thesis, University of Paris, 2021. URL: https://www.irif.fr/~ohlmann/contents/these.pdf.
https://www.irif.fr/~ohlmann/contents/these.pdf
Pawel Parys. Parity games: Zielonka’s algorithm in quasi-polynomial time. In 44th International Symposium on Mathematical Foundations of Computer Science, MFCS, volume 138 of LIPIcs, pages 10:1-10:13, 2019.
Anuj Puri. Theory of hybrid systems and discrete event systems. PhD thesis, EECS Department, University of California, Berkeley, 1995.
Sven Schewe. An optimal strategy improvement algorithm for solving parity and payoff games. In 22nd International Workshop on Computer Science Logic, CSL, volume 5213 of Lecture Notes in Computer Science, pages 369-384, 2008.
Sven Schewe. Solving parity games in big steps. J. Comput. Syst. Sci., 84:243-262, 2017.
Jens Vöge and Marcin Jurdzinski. A discrete strategy improvement algorithm for solving parity games. In 12th International Conference on Computer-Aided Verification, CAV, volume 1855 of Lecture Notes in Computer Science, pages 202-215, 2000.
Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135-183, 1998.
Zhuan Khye Koh and Georg Loho
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode