Document Open Access Logo

A Technique to Speed up Symmetric Attractor-Based Algorithms for Parity Games

Authors K. S. Thejaswini, Pierre Ohlmann, Marcin Jurdziński

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2022.44.pdf
  • Filesize: 0.91 MB
  • 20 pages

Document Identifiers

Author Details

K. S. Thejaswini
  • Department of Computer Science, University of Warwick, Coventry, UK
Pierre Ohlmann
  • University of Warsaw, Poland
Marcin Jurdziński
  • Department of Computer Science, University of Warwick, Coventry, UK

Funding

EPSRC grant EP/P020992/1 (Solving Parity Games in Theory and Practice).
  • Ohlmann, Pierre: Project BOBR that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 948057).

Acknowledgements

We thank Rémi Morvan for contributing to several simulating discussions. We are grateful to Aditya Prakash for proof reading the current version of the paper, and to Nathanaël Fijalkow and Olivier Serre for doing the same with an earlier version of the paper. We also thank anonymous referees for pointing out some missing references from our previous draft as well as for their valuable comments to improve our current presentation. The authors are listed in reverse alphabetical order.

Cite AsGet BibTex

K. S. Thejaswini, Pierre Ohlmann, and Marcin Jurdziński. A Technique to Speed up Symmetric Attractor-Based Algorithms for Parity Games. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 44:1-44:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSTTCS.2022.44

Abstract

The classic McNaughton-Zielonka algorithm for solving parity games has excellent performance in practice, but its worst-case asymptotic complexity is worse than that of the state-of-the-art algorithms. This work pinpoints the mechanism that is responsible for this relative underperformance and proposes a new technique that eliminates it. The culprit is the wasteful manner in which the results obtained from recursive calls are indiscriminately discarded by the algorithm whenever subgames on which the algorithm is run change. Our new technique is based on firstly enhancing the algorithm to compute attractor decompositions of subgames instead of just winning strategies on them, and then on making it carefully use attractor decompositions computed in prior recursive calls to reduce the size of subgames on which further recursive calls are made. We illustrate the new technique on the classic example of the recursive McNaughton-Zielonka algorithm, but it can be applied to other symmetric attractor-based algorithms that were inspired by it, such as the quasi-polynomial versions of the McNaughton-Zielonka algorithm based on universal trees.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Design and analysis of algorithms
  • Theory of computation → Logic and verification
Keywords
  • Parity games
  • Attractor decomposition
  • Quasipolynomial Algorithms
  • Universal trees

Metrics

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

Related Versions

References

  1. Massimo Benerecetti, Daniele Dell'Erba, and Fabio Mogavero. Solving parity games via priority promotion. Formal Methods Syst. Des., 52(2):193-226, 2018. URL: https://doi.org/10.1007/s10703-018-0315-1.
  2. Massimo Benerecetti, Daniele Dell'Erba, and Fabio Mogavero. Robust worst cases for parity games algorithms. Inf. Comput., 272:104501, 2020. URL: https://doi.org/10.1016/j.ic.2019.104501.
  3. Massimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero, Sven Schewe, and Dominik Wojtczak. Priority promotion with parysian flair. CoRR, abs/2105.01738, 2021. URL: http://arxiv.org/abs/2105.01738.
  4. J. C. Bradfield and I. Walukiewicz. The mu-calculus and Model Checking, pages 871-919. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_26.
  5. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasi-polynomial time. SIAM Journal on Computing, 51(2):STOC17-152-STOC17-188, 2022. URL: https://doi.org/10.1137/17M1145288.
  6. W. Czerwiński, L. Daviaud, N. Fijalkow, M. Jurdziński, R. Lazić, and P. Parys. Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. In 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.
  7. L. Daviaud, M. Jurdziński, and K. Lehtinen. Alternating weak automata from universal trees. In 30th International Conference on Concurrency Theory, CONCUR 2019, volume 140 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:14, Amsterdam, the Netherlands, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
  8. Laure Daviaud, Marcin Jurdzinski, and K. S. Thejaswini. The strahler number of a parity game, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.123.
  9. Anuj Dawar and Erich Grädel. The descriptive complexity of parity games. In Michael Kaminski and Simone Martini, editors, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings, volume 5213 of Lecture Notes in Computer Science, pages 354-368. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-87531-4_26.
  10. 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: https://doi.org/10.1109/SFCS.1991.185392.
  11. E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model-checking for fragments of μ-calculus. In Costas Courcoubetis, editor, Computer Aided Verification, 5th International Conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993, Proceedings, volume 697 of Lecture Notes in Computer Science, pages 385-396. Springer, 1993. URL: https://doi.org/10.1007/3-540-56922-7_32.
  12. Kousha Etessami, Thomas Wilke, and Rebecca A. Schuller. Fair simulation relations, parity games, and state space reduction for büchi automata. In Automata, Languages and Programming, 28th International Colloquium, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings, volume 2076 of Lecture Notes in Computer Science, pages 694-707. Springer, 2001. URL: https://doi.org/10.1007/3-540-48224-5_57.
  13. Oliver Friedmann. Recursive algorithm for parity games requires exponential time. RAIRO Theor. Informatics Appl., 45(4):449-457, 2011. URL: https://doi.org/10.1051/ita/2011124.
  14. Maciej Gazda and Tim A. C. Willemse. Zielonka’s recursive algorithm: dull, weak and solitaire games and tighter bounds. In Gabriele Puppis and Tiziano Villa, editors, Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2013, Borca di Cadore, Dolomites, Italy, 29-31th August 2013, volume 119 of EPTCS, pages 7-20, 2013. URL: https://doi.org/10.4204/EPTCS.119.4.
  15. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-36387-4.
  16. Ichiro Hasuo, Shunsuke Shimizu, and Corina Cîrstea. Lattice-theoretic progress measures and coalgebraic model checking. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 718-732. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837673.
  17. M. Jurdziński. Small progress measures for solving parity games. In 17th Annual Symposium on Theoretical Aspects of Computer Science, volume 1770 of LNCS, pages 290-301, Lille, France, 2000. Springer. URL: https://doi.org/10.1007/3-540-46541-3_24.
  18. M. Jurdziński and R. Lazić. Succinct progress measures for solving parity games. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-9, Reykjavik, Iceland, 2017. IEEE Computer Society. Google Scholar
  19. M. Jurdziński, M. Paterson, and U. Zwick. A deterministic subexponential algorithm for solving parity games. SIAM Journal on Computing, 38(4):1519-1532, 2008. Google Scholar
  20. Marcin Jurdziński, Rémi Morvan, and K. S. Thejaswini. Universal Algorithms for Parity Games and Nested Fixpoints. CoRR, abs/2001.04333, 2020. URL: http://arxiv.org/abs/2001.04333.
  21. J. J. A. Keiren. Benchmarks for parity games. In FSEN, volume 9392 of LNCS, pages 127-142, Tehran, Iran, 2015. Springer. URL: https://doi.org/10.1007/978-3-319-24644-4_9.
  22. Ruben Lapauw, Maurice Bruynooghe, and Marc Denecker. Improving parity game solvers with justifications. In Verification, Model Checking, and Abstract Interpretation, pages 449-470, Berlin, Heidelberg, 2020. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-39322-9_21.
  23. K. Lehtinen. A modal μ perspective on solving parity games in quasi-polynomial time. In 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 639-648, Oxford, UK, 2018. IEEE. URL: https://doi.org/10.1145/3209108.3209115.
  24. K. Lehtinen, S. Schewe, and D. Wojtczak. Improving the complexity of Parys' recursive algorithm, 2019. URL: http://arxiv.org/abs/1904.11810.
  25. Karoliina Lehtinen, Paweł Parys, Sven Schewe, and Dominik Wojtczak. A Recursive Approach to Solving Parity Games in Quasipolynomial Time. Logical Methods in Computer Science, Volume 18, Issue 1, January 2022. URL: https://doi.org/10.46298/lmcs-18(1:8)2022.
  26. R. McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65(2):149-184, 1993. URL: https://doi.org/10.1016/0168-0072(93)90036-D.
  27. P. Parys. Parity games: Zielonka’s algorithm in quasi-polynomial time. In MFCS 2019, volume 138 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1-10:13, Aachen, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.10.
  28. N. Piterman. From nondeterministic buchi and streett automata to deterministic parity automata. In 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), pages 255-264, 2006. URL: https://doi.org/10.1109/LICS.2006.28.
  29. Sven Schewe and Bernd Finkbeiner. Synthesis of asynchronous systems. In Proceedings of the 16th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR'06, pages 127-142, Berlin, Heidelberg, 2006. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-71410-1_10.
  30. K. S. Thejaswini, Marcin Jurdziński, and Pierre Ohlmann. A technique to speed up symmetric attractor-based algorithms for parity games. CoRR, abs/2010.08288, 2020. URL: http://arxiv.org/abs/2010.08288.
  31. T. van Dijk. Oink: An implementation and evaluation of modern parity game solvers. In Tools and Algorithms for the Construction and Analysis of Systems, 24th International Conference, TACAS 2018, volume 10805 of LNCS, pages 291-308, Thessaloniki, Greece, 2018. Springer. URL: https://doi.org/10.1007/978-3-319-89960-2_16.
  32. Tom van Dijk. A parity game tale of two counters. In Jérôme Leroux and Jean-François Raskin, editors, Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2019, Bordeaux, France, 2-3rd September 2019, volume 305 of EPTCS, pages 107-122, 2019. URL: https://doi.org/10.4204/EPTCS.305.8.
  33. W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 200(1-2):135-183, 1998. URL: https://doi.org/10.1016/S0304-3975(98)00009-7.
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