Document Open Access Logo

Checking History Determinism for Parity Automata Is in NP

Authors Karoliina Lehtinen , Keya Prakash , Michał Skrzypczak

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.64.pdf
  • Filesize: 0.81 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • History-determinism
  • parity automata
  • good-for-games

Metrics

Abstract

History-deterministic automata, often also called good-for-games, are an intermediate model between deterministic and nondeterministic automata, which are particularly well-suited for applications in verification and reactive synthesis. We show that deciding whether a parity automaton is history-deterministic is in NP. Our result matches an NP-hardness lower bound (Prakash 2024) and builds on insights from a fixed-parameter tractable algorithm (Lehtinen and Prakash 2025). This settles the complexity of the problem, which has been open since 2006.

Cite As Get BibTex

Karoliina Lehtinen, Keya Prakash, and Michał Skrzypczak. Checking History Determinism for Parity Automata Is in NP. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 64:1-64:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.64

Author Details

Karoliina Lehtinen
  • CNRS, Aix Marseille Univ., LIS, Marseille, France
Keya Prakash
  • Aix Marseille Univ., CNRS, LIS, Marseille, France
Michał Skrzypczak
  • University of Warsaw, Poland

Funding

  • Prakash, Keya: Supported by ANR grant QuaSy (ANR 23-CE48-0008).
  • Skrzypczak, Michał: Supported by Poland’s NCN grant Opus no. 2024/55/B/ST6/00318.

References

  1. Bader Abu Radi and Orna Kupferman. Minimization and Canonization of GFG Transition-Based Automata. Log. Methods Comput. Sci., 18(3), 2022. URL: https://doi.org/10.46298/lmcs-18(3:16)2022.
  2. Rohan Acharya, Marcin Jurdzinski, and Keya Prakash. Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata. In ICALP, volume 297 of LIPIcs, pages 124:1-124:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.124.
  3. Shaull Almagor and Orna Kupferman. Good-enough synthesis. In CAV (2), volume 12225 of Lecture Notes in Computer Science, pages 541-563. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_28.
  4. Marc Bagnol and Denis Kuperberg. Büchi Good-for-Games Automata Are Efficiently Recognizable. In FSTTCS, 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.
  5. Udi Boker, Denis Kuperberg, Orna Kupferman, and Michal Skrzypczak. Nondeterminism in the Presence of a Diverse or Unknown Future. In ICALP (2), volume 7966 of Lecture Notes in Computer Science, pages 89-100. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_11.
  6. Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak. On Succinctness and Recognisability of Alternating Good-for-Games Automata. arXiv, 2020. URL: https://arxiv.org/abs/2002.07278.
  7. 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.
  8. Sougata Bose, Thomas A. Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke. History-deterministic Timed Automata. Log. Methods Comput. Sci., 20(4), 2024. URL: https://doi.org/10.46298/LMCS-20(4:1)2024.
  9. J Richard Büchi and Lawrence H Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. Google Scholar
  10. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Generalized parity games. In FoSSaCS, 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.
  11. Thomas Colcombet and Christof Löding. The Non-deterministic Mostowski Hierarchy and Distance-Parity Automata. In Proc. of ICALP, volume 5126, pages 398-409, 2008. URL: https://doi.org/10.1007/978-3-540-70583-3_33.
  12. Rüdiger Ehlers and Sven Schewe. Natural colors of infinite words. In Anuj Dawar and Venkatesan Guruswami, editors, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, IIT Madras, Chennai, India, December 18-20, 2022, volume 250 of LIPIcs, pages 36:1-36:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2022.36.
  13. E. Allen Emerson. Automata, Tableaux and Temporal Logics (Extended Abstract). In Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 79-88. Springer, 1985. URL: https://doi.org/10.1007/3-540-15648-8_7.
  14. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A bit of nondeterminism makes pushdown automata expressive and succinct. In Proc. of MFCS, pages 53:1-53:20, 2021. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.53.
  15. Yuri Gurevich and Leo Harrington. Trees, Automata, and Games. In STOC, pages 60-65. ACM, 1982. URL: https://doi.org/10.1145/800070.802177.
  16. Thomas A. Henzinger, Orna Kupferman, and Sriram K. Rajamani. Fair Simulation. Inf. Comput., 173(1):64-81, 2002. URL: https://doi.org/10.1006/inco.2001.3085.
  17. Thomas A. Henzinger and Nir Piterman. Solving Games Without Determinization. In CSL, volume 4207 of Lecture Notes in Computer Science, pages 395-410. Springer, 2006. URL: https://doi.org/10.1007/11874683_26.
  18. Denis Kuperberg and Michal Skrzypczak. On Determinisation of Good-for-Games Automata. In ICALP (2), 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.
  19. O. Kupferman. Using the past for resolving the future. To appear, 2023. Google Scholar
  20. Orna Kupferman, Shmuel Safra, and Moshe Y Vardi. Relating Word and Tree Automata. Ann. Pure Appl. Logic, 138(1-3):126-146, 2006. Conference version in 1996. URL: https://doi.org/10.1016/J.APAL.2005.06.009.
  21. Karoliina Lehtinen and Keya Prakash. The 2-token theorem: Recognising history-deterministic parity automata efficiently. In Proceedings of the 57th Annual ACM Symposium on Theory of Computing, STOC 2025, Prague, Czechia, June 23-27, 2025, pages 1839-1850. ACM, 2025. URL: https://doi.org/10.1145/3717823.3718310.
  22. Christof Löding and Igor Walukiewicz. Minimal history-deterministic co-büchi automata: Congruences and passive learning. In LICS, pages 431-443. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00039.
  23. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2), 1975. Google Scholar
  24. Damian Niwinski and Igor Walukiewicz. Relating hierarchies of word and tree automata. In Michel Morvan, Christoph Meinel, and Daniel Krob, editors, STACS 98, 15th Annual Symposium on Theoretical Aspects of Computer Science, Paris, France, February 25-27, 1998, Proceedings, volume 1373 of Lecture Notes in Computer Science, pages 320-331. Springer, 1998. URL: https://doi.org/10.1007/BFB0028571.
  25. Keya Prakash. Checking History-Determinism is NP-hard for Parity Automata. In FoSSaCS (1), 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.
  26. Keya Prakash. History-deterministic parity automata : games, complexity, and the 2-token theorem. PhD thesis, January 2025. URL: http://webcat.warwick.ac.uk/record=b4197352.
  27. Bader Abu Radi and Orna Kupferman. Minimizing GFG transition-based automata. In ICALP, volume 132 of LIPIcs, pages 100:1-100:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.100.
  28. Bader Abu Radi, Orna Kupferman, and Ofer Leshkowitz. Easy complementation of history-deterministic büchi automata. In ATVA, volume 15054 of Lecture Notes in Computer Science, pages 67-88. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-78709-6_4.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact