A Theory of Hanoi Omega-Automata and Games
For researchers and tool developers using the HOA format, this work establishes precise computational boundaries for key decision problems, revealing that symbolic encoding introduces higher complexity than previously assumed.
This paper provides the first systematic investigation into the theoretical complexity of decision problems for HOA-encoded automata and games, proving that non-emptiness is NP-complete, language inclusion is PSPACE-complete (EXPSPACE-complete for Emerson-Lei), and solving Hanoi Omega-Games ranges from Π2-completeness to PSPACE-completeness.
The Hanoi Omega-Automata (HOA) format has established itself as the definitive standard for encoding $ω$-regular automata in modern synthesis tools. While HOA is widely adopted due to its succinct symbolic representation, using Boolean formulas as transition guards and transition-based coloring, the exact computational cost of these features has remained understudied. This paper provides the first systematic investigation into the theoretical complexity of decision problems for HOA-encoded automata and games. We establish that the structural features of HOA, specifically the symbolic encoding of large alphabets, make classical problems more complex than in traditional formats. We prove that the non-emptiness problem is NP-complete for all standard acceptance conditions, with hardness arising directly from the Boolean transition guards. For language inclusion, we show that the problem is PSPACE-complete under most conditions but becomes EXPSPACE-complete for Emerson-Lei acceptance. Furthermore, we formalize Hanoi Omega-Games (HOG), where the underlying arena is a deterministic HOA with atomic propositions partitioned into inputs and outputs. We provide tight complexity bounds for solving HOGs, ranging from $Π_2$-completeness for parity and safety conditions to PSPACE-completeness for Muller and Emerson-Lei objectives. Finally, we generalize our techniques to symbolic games where transitions are guarded by formulas in arbitrary decidable first-order theories.