Document Open Access Logo

A Quasi-Polynomial Black-Box Algorithm for Fixed Point Evaluation

Authors André Arnold, Damian Niwiński, Paweł Parys

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.9.pdf
  • Filesize: 0.62 MB
  • 23 pages

Document Identifiers

Author Details

André Arnold
  • Independent Researcher, Talence, France
Damian Niwiński
  • Institute of Informatics, University of Warsaw, Poland
Paweł Parys
  • Institute of Informatics, University of Warsaw, Poland

Funding

  • Parys, Paweł: Author supported by the National Science Centre, Poland (grant no. 2016/22/E/ST6/00041).

Cite AsGet BibTex

André Arnold, Damian Niwiński, and Paweł Parys. A Quasi-Polynomial Black-Box Algorithm for Fixed Point Evaluation. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.9

Abstract

We consider nested fixed-point expressions like μ z. ν y. μ x. f(x,y,z) evaluated over a finite lattice, and ask how many queries to a function f are needed to find the value. The previous upper bounds for a monotone function f of arity d over the lattice {0,1}ⁿ were of the order n^{𝒪(d)}, whereas a lower bound of Ω(n²/(lg n)) is known in case when at least one alternation between the least (μ) and the greatest (ν) fixed point occurs in the expression. Following a recent development for parity games, we show here that a quasi-polynomial number of queries is sufficient, namely n^{lg(d/lg n)+𝒪(1)}. The algorithm is an abstract version of several algorithms proposed recently by a number of authors, which involve (implicitly or explicitly) the structure of a universal tree. We then show a quasi-polynomial lower bound for the number of queries used by the algorithms in consideration.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Mu-calculus
  • Parity games
  • Quasi-polynomial time
  • Black-box algorithm

Metrics

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

References

  1. André Arnold and Damian Niwiński. Rudiments of μ-Calculus. Studies in Logic and the Foundations of Mathematics. Elsevier, 2001. Google Scholar
  2. Julien Bernet, David Janin, and Igor Walukiewicz. Permissive strategies: from parity games to safety games. RAIRO Theor. Informatics Appl., 36(3):261-275, 2002. URL: https://doi.org/10.1051/ita:2002013.
  3. Mikołaj Bojańczyk and Wojciech Czerwiński. An automata toolbox. Informal lecture notes, 2018. URL: https://www.mimuw.edu.pl/~bojan/upload/reduced-may-25.pdf.
  4. 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.
  5. 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.
  6. Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, and Alexander Svozil. Quasipolynomial set-based symbolic algorithms for parity games. In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018, volume 57 of EPiC Series in Computing, pages 233-253. EasyChair, 2018. URL: http://www.easychair.org/publications/paper/L8b1.
  7. Thomas Colcombet and Nathanaël Fijalkow. Universal graphs and good for games automata: New tools for infinite duration games. In Mikołaj Bojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11425 of Lecture Notes in Computer Science, pages 1-26. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_1.
  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, Paul W. Goldberg, and Christos H. Papadimitriou. The complexity of computing a Nash equilibrium. Commun. ACM, 52(2):89-97, 2009. URL: https://doi.org/10.1145/1461928.1461951.
  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 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.
  12. 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.
  13. 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.
  14. Daniel Hausmann and Lutz Schröder. Computing nested fixpoints in quasipolynomial time. CoRR, abs/1907.07020v2, 2019. URL: http://arxiv.org/abs/1907.07020v2.
  15. Daniel Hausmann and Lutz Schröder. Quasipolynomial computation of nested fixpoints. CoRR, abs/1907.07020v3, 2020. URL: http://arxiv.org/abs/1907.07020v3.
  16. 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.
  17. 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.
  18. 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.
  19. Marcin Jurdziński and Rémi Morvan. A universal attractor decomposition algorithm for parity games. CoRR, abs/2001.04333, 2020. URL: http://arxiv.org/abs/2001.04333.
  20. Marcin Jurdziński, Mike Paterson, and Uri Zwick. A deterministic subexponential algorithm for solving parity games. In Proceedings of the Seventeenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2006, Miami, Florida, USA, January 22-26, 2006, pages 117-123. ACM Press, 2006. URL: http://dl.acm.org/citation.cfm?id=1109557.1109571.
  21. 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.
  22. 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.
  23. 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.
  24. Paweł Parys. Some results on complexity of μ-calculus evaluation in the black-box model. RAIRO - Theor. Inf. and Applic., 47(1):97-109, 2013. URL: https://doi.org/10.1051/ita/2012030.
  25. Paweł Parys. Parity games: Zielonka’s algorithm in quasi-polynomial time. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 10:1-10:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.10.
  26. 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.
  27. Igor Walukiewicz. Monadic second order logic on tree-like structures. In Claude Puech and Rüdiger Reischuk, editors, STACS 96, 13th Annual Symposium on Theoretical Aspects of Computer Science, Grenoble, France, February 22-24, 1996, Proceedings, volume 1046 of Lecture Notes in Computer Science, pages 401-413. Springer, 1996. URL: https://doi.org/10.1007/3-540-60922-9_33.
  28. Shipei Zhang, Oleg Sokolsky, and Scott A. Smolka. On the parallel complexity of model checking in the modal mu-calculus. In Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), Paris, France, July 4-7, 1994, pages 154-163. IEEE Computer Society, 1994. URL: https://doi.org/10.1109/LICS.1994.316075.
  29. 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.
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