Parity Games: Zielonka’s Algorithm in Quasi-Polynomial Time

Author Paweł Parys



PDF
Thumbnail PDF

File

LIPIcs.MFCS.2019.10.pdf
  • Filesize: 438 kB
  • 13 pages

Document Identifiers

Author Details

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

Acknowledgements

The author would like to thank Wojciech Czerwiński, Laure Daviaud, Marcin Jurdziński, Eryk Kopczyński, Ranko Lazić, Karoliina Lehtinen, and Igor Walukiewicz for all the discussions that preceded writing of this paper, and the anonymous reviewers of all versions of this paper for their valuable comments.

Cite As Get BibTex

Paweł Parys. Parity Games: Zielonka’s Algorithm in Quasi-Polynomial Time. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 10:1-10:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.MFCS.2019.10

Abstract

Calude, Jain, Khoussainov, Li, and Stephan (2017) proposed a quasi-polynomial-time algorithm solving parity games. After this breakthrough result, a few other quasi-polynomial-time algorithms were introduced; none of them is easy to understand. Moreover, it turns out that in practice they operate very slowly. On the other side there is Zielonka’s recursive algorithm, which is very simple, exponential in the worst case, and the fastest in practice. We combine these two approaches: we propose a small modification of Zielonka’s algorithm, which ensures that the running time is at most quasi-polynomial. In effect, we obtain a simple algorithm that solves parity games in quasi-polynomial time. We also hope that our algorithm, after further optimizations, can lead to an algorithm that shares the good performance of Zielonka’s algorithm on typical inputs, while reducing the worst-case complexity on difficult inputs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Algorithmic game theory
Keywords
  • Parity games
  • Zielonka’s algorithm
  • quasi-polynomial time

Metrics

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

References

  1. Massimo Benerecetti, Daniele Dell'Erba, and Fabio Mogavero. Robust Exponential Worst Cases for Divide-et-Impera Algorithms for Parity Games. In Patricia Bouyer, Andrea Orlandini, and Pierluigi San Pietro, editors, Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2017, Roma, Italy, 20-22 September 2017., volume 256 of EPTCS, pages 121-135, 2017. URL: https://doi.org/10.4204/EPTCS.256.9.
  2. 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: https://doi.org/10.1007/s10703-018-0315-1.
  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: https://doi.org/10.1016/j.dam.2006.04.029.
  4. Mikołaj Bojańczyk and Wojciech Czerwiński. An Automata Toolbox, February 2018. URL: https://www.mimuw.edu.pl/~bojan/papers/toolbox-reduced-feb6.pdf.
  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: https://doi.org/10.1016/S0304-3975(96)00228-9.
  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: https://doi.org/10.1145/3055399.3055409.
  7. Anne Condon. The Complexity of Stochastic Games. Inf. Comput., 96(2):203-224, 1992. URL: https://doi.org/10.1016/0890-5401(92)90048-K.
  8. 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: https://doi.org/10.1137/1.9781611975482.142.
  9. 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: https://doi.org/10.1137/1.9781611973082.62.
  10. 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: https://doi.org/10.1016/S0304-3975(00)00034-7.
  11. 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: https://doi.org/10.1007/978-3-642-14162-1_46.
  12. John Fearnley. Efficient Parallel Strategy Improvement for Parity Games. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 137-154. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_8.
  13. 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: https://doi.org/10.1145/3092282.3092286.
  14. Oliver Friedmann. Recursive algorithm for parity games requires exponential time. RAIRO - Theor. Inf. and Applic., 45(4):449-457, 2011. URL: https://doi.org/10.1051/ita/2011124.
  15. 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: https://doi.org/10.1145/1993636.1993675.
  16. Maciej Gazda. Fixpoint Logic, Games, and Relations of Consequence. PhD thesis, Eindhoven University of Technology, 2016. URL: https://pure.tue.nl/ws/files/16681817/20160315_Gazda.pdf.
  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: http://arxiv.org/abs/1702.01953.
  18. Marcin Jurdziński. Deciding the Winner in Parity Games is in UP ∩ co-UP. Inf. Process. Lett., 68(3):119-124, 1998. URL: https://doi.org/10.1016/S0020-0190(98)00150-1.
  19. 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: https://doi.org/10.1007/3-540-46541-3_24.
  20. 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: https://doi.org/10.1109/LICS.2017.8005092.
  21. 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: https://doi.org/10.1137/070686652.
  22. Jeroen J. A. Keiren. Benchmarks for Parity Games. In Mehdi Dastani and Marjan Sirjani, editors, Fundamentals of Software Engineering - 6th International Conference, FSEN 2015 Tehran, Iran, April 22-24, 2015, Revised Selected Papers, volume 9392 of Lecture Notes in Computer Science, pages 127-142. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24644-4_9.
  23. 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: https://doi.org/10.1007/978-3-319-98654-8_3.
  24. 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: https://doi.org/10.1145/3209108.3209115.
  25. Karoliina Lehtinen, Sven Schewe, and Dominik Wojtczak. Improving the complexity of Parys' recursive algorithm. CoRR, abs/1904.11810, 2019. URL: http://arxiv.org/abs/1904.11810.
  26. Yao Liu, Zhenhua Duan, and Cong Tian. An Improved Recursive Algorithm for Parity Games. In 2014 Theoretical Aspects of Software Engineering Conference, TASE 2014, Changsha, China, September 1-3, 2014, pages 154-161. IEEE Computer Society, 2014. URL: https://doi.org/10.1109/TASE.2014.24.
  27. Donald A. Martin. Borel determinacy. The Annals of Mathematics, 102(2):363-371, 1975. Google Scholar
  28. Robert McNaughton. Infinite Games Played on Finite Graphs. Ann. Pure Appl. Logic, 65(2):149-184, 1993. URL: https://doi.org/10.1016/0168-0072(93)90036-D.
  29. Michael Oser Rabin. Automata on Infinite Objects and Church’s Problem. American Mathematical Society, Boston, MA, USA, 1972. Google Scholar
  30. Sven Schewe. Solving parity games in big steps. J. Comput. Syst. Sci., 84:243-262, 2017. URL: https://doi.org/10.1016/j.jcss.2016.10.002.
  31. Helmut Seidl. Fast and Simple Nested Fixpoints. Inf. Process. Lett., 59(6):303-308, 1996. URL: https://doi.org/10.1016/0020-0190(96)00130-5.
  32. Tom van Dijk. Oink: An Implementation and Evaluation of Modern Parity Game Solvers. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I, volume 10805 of Lecture Notes in Computer Science, pages 291-308. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89960-2_16.
  33. Maks Verver. Practical Improvements to Parity Game Solving. Master’s thesis, University of Twente, 2013. URL: http://essay.utwente.nl/64985/1/practical-improvements-to-parity-game-solving.pdf.
  34. 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: https://doi.org/10.1007/10722167_18.
  35. 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: https://doi.org/10.1016/S0304-3975(98)00009-7.
  36. Uri Zwick and Mike Paterson. The Complexity of Mean Payoff Games on Graphs. Theor. Comput. Sci., 158(1&2):343-359, 1996. URL: https://doi.org/10.1016/0304-3975(95)00188-3.
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