A Theory of Hanoi Omega-Automata and Games

TL;DR

This paper analyzes the computational complexity of decision problems for Hanoi Omega-Automata (HOA) and introduces Hanoi Omega-Games, providing tight bounds and exploring their theoretical properties.

Contribution

It offers the first systematic complexity analysis of HOA decision problems and formalizes Hanoi Omega-Games with precise complexity bounds.

Findings

Non-emptiness is NP-complete for HOA.

Language inclusion is PSPACE-complete, EXPSPACE-complete for Emerson-Lei.

HOG solving complexity ranges from $$-completeness to PSPACE-completeness.

Abstract

The Hanoi Omega-Automata (HOA) format has established itself as the definitive standard for encoding $\omega$-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 $\Pi_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.