Checking History Determinism for Parity Automata Is in NP
Karoliina Lehtinen, Keya Prakash, Michal Skrzypczak
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.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext bda86e97-a649-4530-891b-176c2d38852cBuilds on3
- Good-Enough SynthesisShaull Almagor, Orna KupfermanCAV 2020 · 10 citations
- The 2-Token Theorem: Recognising History-Deterministic Parity Automata EfficientlyKaroliina Lehtinen, Aditya PrakashSTOC 2025 · 3 citations
- Minimal History-Deterministic Co-Büchi Automata: Congruences and Passive LearningChristof Löding, Igor WalukiewiczLICS 2025 · 3 citations
Related papers
- Good-for-games ω-Pushdown AutomataKaroliina Lehtinen, Martin ZimmermannLICS 2020 · 7 citations
- Layered Automata: A Canonical Model for Automata over Infinite WordsAntonio Casares, Christof Löding, Igor WalukiewiczLICS 2026
- DFAMiner: Mining Minimal Separating DFAs from Labelled SamplesDaniele Dell'Erba, Yong Li, Sven ScheweFM 2024 · 4 citations
- Making Streett Determinization TightCong Tian, Wensheng Wang, Zhenhua DuanLICS 2020 · 2 citations
- Positional ω-regular languagesAntonio Casares, Pierre OhlmannLICS 2024 · 1 citation
