Document Open Access Logo

Beyond Value Iteration for Parity Games: Strategy Iteration with Universal Trees

Authors Zhuan Khye Koh , Georg Loho

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.63.pdf
  • Filesize: 0.76 MB
  • 15 pages

Document Identifiers

Author Details

Zhuan Khye Koh
  • Department of Mathematics, London School of Economics and Political Science, United Kingdom
Georg Loho
  • Discrete Mathematics and Mathematical Programming, University of Twente, The Netherlands

Funding

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).

Acknowledgements

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.

Cite AsGet BibTex

Zhuan Khye Koh and Georg Loho. Beyond Value Iteration for Parity Games: Strategy Iteration with Universal Trees. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 63:1-63:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.63

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Design and analysis of algorithms
  • Theory of computation → Logic and verification
  • Mathematics of computing → Discrete mathematics
Keywords
  • parity games
  • strategy iteration
  • value iteration
  • progress measure
  • universal trees

Metrics

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

Related Versions

References

  1. Ravindra K. Ahuja, Thomas L. Magnanti, and James B. Orlin. Network flows. Theory, algorithms, and applications. Englewood Cliffs, NJ: Prentice Hall, 1993. Google Scholar
  2. Massimo Benerecetti, Daniele Dell'Erba, and Fabio Mogavero. Solving parity games via priority promotion. Formal Methods Syst. Des., 52(2):193-226, 2018. Google Scholar
  3. 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.
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. 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.
  13. A. J. Hoffman and R. M. Karp. On nonterminating stochastic games. Manage. Sci., 12(5):359-370, 1966. Google Scholar
  14. Marcin Jurdzinski. Deciding the winner in parity games is in UP ∩ co-UP. Inf. Process. Lett., 68(3):119-124, 1998. Google Scholar
  15. 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. Google Scholar
  16. 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. Google Scholar
  17. Marcin Jurdzinski, Mike Paterson, and Uri Zwick. A deterministic subexponential algorithm for solving parity games. SIAM J. Comput., 38(4):1519-1532, 2008. Google Scholar
  18. 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.
  19. 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. Google Scholar
  20. Matthias Mnich, Heiko Röglin, and Clemens Rösner. New deterministic algorithms for solving parity games. Discret. Optim., 30:73-95, 2018. Google Scholar
  21. 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.
  22. 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. Google Scholar
  23. Anuj Puri. Theory of hybrid systems and discrete event systems. PhD thesis, EECS Department, University of California, Berkeley, 1995. Google Scholar
  24. 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. Google Scholar
  25. Sven Schewe. Solving parity games in big steps. J. Comput. Syst. Sci., 84:243-262, 2017. Google Scholar
  26. 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. Google Scholar
  27. Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135-183, 1998. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact