Checking History Determinism for Parity Automata Is in NP
Karoliina Lehtinen, Keya Prakash, Michal Skrzypczak
2026年份
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
它引用的顶会 Paper3
- Good-Enough SynthesisShaull Almagor, Orna KupfermanCAV 2020 · 被引用 10 次
- The 2-Token Theorem: Recognising History-Deterministic Parity Automata EfficientlyKaroliina Lehtinen, Aditya PrakashSTOC 2025 · 被引用 3 次
- Minimal History-Deterministic Co-Büchi Automata: Congruences and Passive LearningChristof Löding, Igor WalukiewiczLICS 2025 · 被引用 3 次
相关 Paper
- Good-for-games ω-Pushdown AutomataKaroliina Lehtinen, Martin ZimmermannLICS 2020 · 被引用 7 次
- 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 次
- Making Streett Determinization TightCong Tian, Wensheng Wang, Zhenhua DuanLICS 2020 · 被引用 2 次
- Positional ω-regular languagesAntonio Casares, Pierre OhlmannLICS 2024 · 被引用 1 次
