Document Open Access Logo

The Strahler Number of a Parity Game

Authors Laure Daviaud , Marcin Jurdziński , K. S. Thejaswini

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2020.123.pdf
  • Filesize: 0.49 MB
  • 19 pages

Document Identifiers

Author Details

Laure Daviaud
  • CitAI, Department of Computer Science, City, University of London, UK
Marcin Jurdziński
  • Department of Computer Science, University of Warwick, Coventry, UK
K. S. Thejaswini
  • Department of Computer Science, University of Warwick, Coventry, UK

Funding

This work has been supported by the EPSRC grant EP/P020992/1 (Solving Parity Games in Theory and Practice). It has started when the third author was supported by the Department of Computer Science at the University of Warwick as a visiting student from Chennai Mathematical Institute, India.

Acknowledgements

We thank colleagues in the following human chain for contributing to our education on the Strahler number of a tree: the first and the second authors have learnt it from the third author, who has learnt it from K Narayan Kumar, who has learnt it from Dmitry Chistikov, who has learnt it from Radu Iosif and Stefan Kiefer at a workshop on Infinite-State Systems, which has been organized and hosted by Joël Ouaknine and Prakash Panangaden at Bellairs Research Institute.

Cite AsGet BibTex

Laure Daviaud, Marcin Jurdziński, and K. S. Thejaswini. The Strahler Number of a Parity Game. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 123:1-123:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ICALP.2020.123

Abstract

The Strahler number of a rooted tree is the largest height of a perfect binary tree that is its minor. The Strahler number of a parity game is proposed to be defined as the smallest Strahler number of the tree of any of its attractor decompositions. It is proved that parity games can be solved in quasi-linear space and in time that is polynomial in the number of vertices n and linear in (d/(2k))^k, where d is the number of priorities and k is the Strahler number. This complexity is quasi-polynomial because the Strahler number is at most logarithmic in the number of vertices. The proof is based on a new construction of small Strahler-universal trees. It is shown that the Strahler number of a parity game is a robust, and hence arguably natural, parameter: it coincides with its alternative version based on trees of progress measures and - remarkably - with the register number defined by Lehtinen (2018). It follows that parity games can be solved in quasi-linear space and in time that is polynomial in the number of vertices and linear in (d/(2k))^k, where k is the register number. This significantly improves the running times and space achieved for parity games of bounded register number by Lehtinen (2018) and by Parys (2020). The running time of the algorithm based on small Strahler-universal trees yields a novel trade-off k ⋅ lg(d/k) = O(log n) between the two natural parameters that measure the structural complexity of a parity game, which allows solving parity games in polynomial time. This includes as special cases the asymptotic settings of those parameters covered by the results of Calude, Jain Khoussainov, Li, and Stephan (2017), of Jurdziński and Lazić (2017), and of Lehtinen (2018), and it significantly extends the range of such settings, for example to d = 2^O(√{lg n}) and k = O(√{lg n}).

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Theory and algorithms for application domains
  • Theory of computation → Design and analysis of algorithms
  • Theory of computation → Logic and verification
Keywords
  • parity game
  • attractor decomposition
  • progress measure
  • universal tree
  • Strahler number

Metrics

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

Related Versions

References

  1. P. Baldan, B. König, C. Mika-Michalski, and T. Padoan. Fixpoint games on continuous lattices. Proceedings of the ACM on Programming Languages, 3(POPL, January 2019):26:1-26:29, 2019. Google Scholar
  2. J. C. Bradfield and I. Walukiewicz. Handbook of Model Checking, chapter The mu-calculus and model checking, pages 871-919. Springer, 2018. Google Scholar
  3. C. S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. In STOC 2017, pages 252-263, Montreal, QC, Canada, 2017. ACM. Google Scholar
  4. 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 Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2019, pages 2333-2349, San Diego, CA, 2019. SIAM. Google Scholar
  5. L. Daviaud, M. Jurdziński, and R. Lazić. A pseudo-quasi-polynomial algorithm for mean-payoff parity games. In 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 325-334, Oxford, UK, 2018. ACM. Google Scholar
  6. 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
  7. L. Daviaud, M. Jurdziński, and K. S. Thejaswini. The Strahler number of a parity game, 2020. URL: http://arxiv.org/abs/2003.08627.
  8. E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy. In 32nd Annual Symposium on Foundations of Computer Science, pages 368-377, San Juan, Puerto Rico, 1991. IEEE Computer Society. Google Scholar
  9. E. A. Emerson, C. S. Jutla, and P. Sistla. On model-checking for fragments of μ-calculus. In CAV 1993, volume 697 of LNCS, pages 385-396, Elounda, Greece, 1993. Springer. Google Scholar
  10. A. P. Ershov. On programming of arithmetic operations. Communications of the ACM, 1(8):3-6, 1958. Google Scholar
  11. J. Esparza, M. Luttenberger, and M. Schlund. A brief history of Strahler numbers - with a preface. Technical report, Technical University of Munich, 2016. Google Scholar
  12. J. Fearnley. Exponential lower bounds for policy iteration. In ICALP 2010, volume 6199 of LNCS, pages 551-562, Bordeaux, France, 2010. Springer. Google Scholar
  13. J. Fearnley, S. Jain, B. de Keijzer, S. Schewe, F. Stephan, and D. Wojtczak. An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space. International Journal on Software Tools for Technology Transfer, 21(3):325-349, 2019. Google Scholar
  14. O. Friedmann. An exponential lower bound for the parity game strategy improvement algorithm as we know it. In LICS 2009, pages 145-156, Los Angeles, CA, USA, 2009. IEEE Computer Society. Google Scholar
  15. O. Friedmann. A subexponential lower bound for Zadeh’s pivoting rule for solving linear programs and games. In IPCO 2011, volume 6655 of LNCS, pages 192-206, New York, NY, USA, 2011. Springer. Google Scholar
  16. O. Friedmann, T. D. Hansen, and U. Zwick. Subexponential lower bounds for randomized pivoting rules for the simplex algorithm. In STOC 2011, pages 283-292, San Jose, CA, USA, 2011. ACM. Google Scholar
  17. E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. Google Scholar
  18. D. Hausmann and L. Schröder. Computing nested fixpoints in quasipolynomial time, 2019. URL: http://arxiv.org/abs/1907.07020.
  19. 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. Google Scholar
  20. 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
  21. M. Jurdziński and R. Morvan. A universal attractor decomposition algorithm for parity games, 2020. URL: http://arxiv.org/abs/2001.04333.
  22. 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
  23. D. E. Knuth. The Art of Computer Programming. Addison-Wesley, 1973. Google Scholar
  24. 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. Google Scholar
  25. K. Lehtinen and U. Boker. Register games, April 2020. URL: http://arxiv.org/abs/1902.10654.
  26. K. Lehtinen, S. Schewe, and D. Wojtczak. Improving the complexity of Parys' recursive algorithm, 2019. URL: http://arxiv.org/abs/1904.11810.
  27. R. McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65(2):149-184, 1993. Google Scholar
  28. 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. Google Scholar
  29. P. Parys. Parity games: Another view on Lehtinen’s algorithm. In 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, volume 152 of LIPIcs, pages 32:1-32:15, Barcelona, Spain, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
  30. X. G. Viennot. Trees everywhere. In 15th Colloquium on Trees in Algebra and Programming, volume 431 of LNCS, pages 18-41, Copenhagen, Denmark, 1990. Springer. Google Scholar
  31. J. Vöge and M. Jurdziński. A discrete strategy improvement algorithm for solving parity games. In CAV 2000, volume 1855 of LNCS, pages 202-215, Chicago, IL, USA, 2000. Springer. Google Scholar
  32. W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science, 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