Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata

Authors Rohan Acharya, Marcin Jurdziński , Aditya Prakash



PDF
Thumbnail PDF

File

LIPIcs.ICALP.2024.124.pdf
  • Filesize: 0.72 MB
  • 18 pages

Document Identifiers

Author Details

Rohan Acharya
  • University of Warwick, Coventry, UK
Marcin Jurdziński
  • University of Warwick, Coventry, UK
Aditya Prakash
  • University of Warwick, Coventry, UK

Acknowledgements

We thank Udi Boker, Denis Kuperberg, and Karoliina Lehtinen for several insightful exchanges. We are grateful to the reviewers for their feedback and suggestions on how to improve the paper.

Cite AsGet BibTex

Rohan Acharya, Marcin Jurdziński, and Aditya Prakash. Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 124:1-124:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ICALP.2024.124

Abstract

Our main technical contribution is a polynomial-time determinisation procedure for history-deterministic Büchi automata, which settles an open question of Kuperberg and Skrzypczak, 2015. A key conceptual contribution is the lookahead game, which is a variant of Bagnol and Kuperberg’s token game, in which Adam is given a fixed lookahead. We prove that the lookahead game is equivalent to the 1-token game. This allows us to show that the 1-token game characterises history-determinism for semantically-deterministic Büchi automata, which paves the way to our polynomial-time determinisation procedure.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • History determinism
  • Good-for-games
  • Automata over infinite words
  • Games

Metrics

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

References

  1. Bader Abu Radi and Orna Kupferman. Minimization and Canonization of GFG Transition-Based Automata. Logical Methods in Computer Science, 18(3), 2022. URL: https://doi.org/10.46298/lmcs-18(3:16)2022.
  2. Rohan Acharya, Marcin Jurdziński, and Aditya Prakash. Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata. CoRR, abs/2310.13498, 2024. URL: https://doi.org/10.48550/arXiv.2310.13498.
  3. Marc Bagnol and Denis Kuperberg. Büchi Good-for-Games Automata Are Efficiently Recognizable. In Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, volume 122 of LIPIcs, pages 16:1-16:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2018.16.
  4. Udi Boker, Thomas Henzinger, Karoliina Lehtinen, and Aditya Prakash. History-Determinism vs. Fair Simulation, To appear. Google Scholar
  5. Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michal Skrzypczak. On the Succinctness of Alternating Parity Good-for-Games Automata. CoRR, abs/2009.14437, 2020. URL: https://arxiv.org/abs/2009.14437.
  6. Udi Boker and Karoliina Lehtinen. When a Little Nondeterminism Goes a Long Way: An Introduction to History-Determinism. ACM SIGLOG News, 10(1):24-51, 2023. URL: https://doi.org/10.1145/3584676.3584682.
  7. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding Parity Games in Quasi-polynomial Time. SIAM J. Comput., 51(2):17-152, 2022. URL: https://doi.org/10.1137/17m1145288.
  8. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Generalized Parity Games. In Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, volume 4423 of Lecture Notes in Computer Science, pages 153-167. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71389-0_12.
  9. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-36387-4.
  10. Yuri Gurevich and Leo Harrington. Trees, Automata, and Games. In Symposium on Theory of Computing, STOC 1982, pages 60-65. ACM, 1982. URL: https://doi.org/10.1145/800070.802177.
  11. Thomas A. Henzinger and Nir Piterman. Solving Games Without Determinization. In Computer Science Logic, CSL 2006, volume 4207 of Lecture Notes in Computer Science, pages 395-410. Springer, 2006. URL: https://doi.org/10.1007/11874683_26.
  12. Marcin Jurdzinski. Small Progress Measures for Solving Parity Games. In STACS 2000, volume 1770 of Lecture Notes in Computer Science, pages 290-301. Springer, 2000. URL: https://doi.org/10.1007/3-540-46541-3_24.
  13. Marcin Jurdzinski and Ranko Lazic. Succinct Progress Measures for Solving Parity Games. In Symposium on Logic in Computer Science, LICS 2017, pages 1-9. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005092.
  14. Denis Kuperberg and Michal Skrzypczak. On Determinisation of Good-for-Games Automata. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, volume 9135 of Lecture Notes in Computer Science, pages 299-310. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_24.
  15. Orna Kupferman. Using the Past for Resolving the Future. Frontiers Comput. Sci., 4, 2022. URL: https://doi.org/10.3389/fcomp.2022.1114625.
  16. Karoliina Lehtinen, Pawel Parys, Sven Schewe, and Dominik Wojtczak. A Recursive Approach to Solving Parity Games in Quasipolynomial Time. Log. Methods Comput. Sci., 18(1), 2022. URL: https://doi.org/10.46298/lmcs-18(1:8)2022.
  17. Donald A. Martin. Borel Determinacy. Annals of Mathematics, 102(2):363-371, 1975. URL: http://www.jstor.org/stable/1971035.
  18. Aditya Prakash. Checking History-Determinism is NP-hard for Parity Automata. In Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, volume 14574 of Lecture Notes in Computer Science, pages 212-233. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57228-9_11.
  19. Aditya Prakash and K. S. Thejaswini. On History-Deterministic One-Counter Nets. In Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, volume 13992 of Lecture Notes in Computer Science, pages 218-239. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_11.
  20. Bader Abu Radi and Orna Kupferman. On Semantically-Deterministic Automata. In International Colloquium on Automata, Languages, and Programming, ICALP 2023, volume 261 of LIPIcs, pages 109:1-109:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.109.
  21. Bader Abu Radi, Orna Kupferman, and Ofer Leshkowitz. A Hierarchy of Nondeterminism. In Mathematical Foundations of Computer Science, MFCS 2021, volume 202 of LIPIcs, pages 85:1-85:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.85.
  22. Sven Schewe. Minimising Good-For-Games Automata Is NP-Complete. In Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020, volume 182 of LIPIcs, pages 56:1-56:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2020.56.
  23. Igor Walukiewicz. Monadic Second-Order Logic on Tree-like Structures. Theor. Comput. Sci., 275(1-2):311-346, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00185-2.