pith. sign in

arxiv: 2604.24231 · v1 · submitted 2026-04-27 · 💻 cs.LO · cs.FL

A Theory of Hanoi Omega-Automata and Games

Emmanuel Filiot , Allen Joseph , Guillermo A. P\'erez , Saina Sunny This is my paper

Pith reviewed 2026-05-07 17:52 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords Hanoi Omega-Automataomega-automatanon-emptinesslanguage inclusionautomata gamescomputational complexityEmerson-Lei acceptancesymbolic automata
0
0 comments X

The pith

Boolean transition guards make non-emptiness NP-complete for Hanoi Omega-Automata under every acceptance condition.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper shows that the Boolean formulas used as transition guards in the Hanoi Omega-Automata format push the non-emptiness problem to NP-complete for every standard acceptance condition. A reader would care because HOA is the common format in synthesis tools, so these bounds directly limit what verification and controller synthesis procedures can do in practice. The authors give matching upper and lower bounds for language inclusion, which stays in PSPACE for most conditions but reaches EXPSPACE for Emerson-Lei, and for two-player games on deterministic HOA arenas. They also show the same methods apply when transition guards come from any decidable first-order theory.

Core claim

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 where the arena is a deterministic HOA with inputs and outputs partitioned. We provide tight complexity bounds for solving these games, ranging from Pi-2-completeness for parity and safety to PSPACE-completeness for Muller and Emerson-Lei objectives. The techniques extend to symbolic games guarded by formulas from arbitrary decidable first-oder

What carries the argument

The Boolean formulas that serve as transition guards in the HOA encoding, which compactly describe transitions over large alphabets.

If this is right

  • Emptiness checks in synthesis tools that use HOA must handle NP-hard instances in the worst case.
  • Language inclusion checks require at most PSPACE resources except when Emerson-Lei acceptance is used.
  • Solving deterministic HOA games stays inside Pi-2 or PSPACE depending on the winning condition.
  • The same complexity pattern holds when guards are taken from any decidable first-order theory.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Restricting the Boolean guards to a simpler syntactic class might restore polynomial-time emptiness while keeping some succinctness.
  • The results suggest that other succinct automata formats that rely on formula guards will inherit similar hardness.
  • Tool builders could add guard-simplification passes to avoid the worst-case complexity in common cases.

Load-bearing premise

The hardness of non-emptiness and related problems is produced by the Boolean transition guards themselves rather than by other features of the encoding or the acceptance conditions.

What would settle it

A polynomial-time algorithm that decides non-emptiness for arbitrary Boolean guards in HOA would falsify the NP-completeness result.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript provides the first systematic complexity analysis of decision problems for ω-automata and games encoded in the Hanoi Omega-Automata (HOA) format. It proves that non-emptiness is NP-complete for all standard acceptance conditions (Büchi, co-Büchi, parity, Muller, Emerson-Lei), with hardness arising directly from the Boolean transition guards rather than other HOA features. Language inclusion is PSPACE-complete under most conditions but EXPSPACE-complete for Emerson-Lei acceptance. For Hanoi Omega-Games (HOG) on deterministic HOA arenas with partitioned input/output propositions, solving complexity ranges from Π₂-complete (parity, safety) to PSPACE-complete (Muller, Emerson-Lei). The results are generalized to symbolic games whose transitions are guarded by formulas in arbitrary decidable first-order theories.

Significance. If the results hold, this work is significant because it quantifies the computational overhead introduced by HOA's succinct symbolic representation, which is now the standard encoding in synthesis tools. The explicit separation of hardness sources (Boolean guards vs. acceptance conditions or state structure) and the tight bounds for games provide actionable guidance for algorithm designers. The generalization to first-order theories extends the applicability beyond propositional logic and supplies reproducible proof techniques via reductions from known hard problems.

minor comments (3)
  1. [Abstract] Abstract: the statement that HOA 'has established itself as the definitive standard' would be strengthened by a brief citation to its adoption in tools such as Spot or Strix.
  2. [§4] §4 (HOG definition): the determinism requirement on the underlying HOA should explicitly state whether it holds with respect to the full alphabet or only after the input/output partition; the current wording leaves this ambiguous for the game semantics.
  3. [§5] §5 (generalization): an illustrative example of a concrete first-order theory (e.g., linear integer arithmetic) together with its decision procedure would help readers assess the practical scope of the EXPSPACE result.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their detailed summary of our paper and for recommending a minor revision. The summary accurately captures the key contributions regarding the complexity results for HOA non-emptiness, inclusion, and HOG games. Since the report does not list any specific major comments, we have no individual points to address at this time. We will proceed with preparing a revised version incorporating any minor suggestions.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper establishes complexity results for non-emptiness, inclusion, and games on HOA via standard techniques: NP membership follows from guessing a polynomial-size accepting run together with satisfying assignments to Boolean guards (each checkable in NP), while hardness is shown by direct polynomial reduction from SAT that places a single hard formula on a trivial underlying graph admitting the required acceptance condition. These arguments are self-contained, rely on external known problems (SAT, standard automata theory), and do not reduce to any self-definition, fitted parameter renamed as prediction, or load-bearing self-citation. The abstract and skeptic analysis confirm that hardness arises independently from the Boolean guards rather than from HOA-specific features being presupposed. No step in the derivation chain collapses to an input by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The results rest entirely on standard automata theory and complexity theory; no free parameters, invented entities, or ad-hoc axioms are introduced.

axioms (1)
  • standard math Standard definitions of omega-automata, acceptance conditions (parity, safety, Muller, Emerson-Lei), and complexity classes (NP, PSPACE, EXPSPACE, Pi2).
    Invoked to classify decision problems throughout the abstract.

pith-pipeline@v0.9.0 · 5539 in / 1194 out tokens · 62635 ms · 2026-05-07T17:52:39.840675+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

13 extracted references · 13 canonical work pages

  1. [1]

    The hanoi omega-automata format

    2 Tomás Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kretínský, David Müller, David Parker, and Jan Strejcek. The hanoi omega-automata format. In Daniel Kroening and Corina S. Pasareanu, editors,Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, vol...

    work page 2015

  2. [2]

    In: CA V ’15

    doi:10.1007/978-3-319-21690-4\_31. 3 Jon Barwise. An introduction to first-order logic. In Jon Barwise, editor,Handbook of Mathematical Logic, pages 5–46. North-Holland,

    work page doi:10.1007/978-3-319-21690-4

  3. [4]

    URL:https://doi.org/10.4230/LIPIcs.CSL.2017.12, doi: 10.4230/LIPICS.CSL.2017.12. E. Filiot, A. Joseph, G. A. Pérez, and S. Sunny 23 6 Itshak Borosh and Leon Bruce Treybig. Bounds on positive integral solutions of linear Diophantine equations.Proceedings of the American Mathematical Society, 55(2):299–304,

    work page doi:10.4230/lipics.csl.2017.12 2017

  4. [5]

    7 Randal E. Bryant. Binary decision diagrams. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors,Handbook of Model Checking, pages 191–217. Springer, 2018.doi:10.1007/978-3-319-10575-8\_7. 8 Antonio Casares. Transition-based vs stated-based acceptance for automata over infinite words.CoRR, abs/2508.15402,

    work page doi:10.1007/978-3-319-10575-8 2018

  5. [6]

    9 Yaacov Choueka

    URL: https://doi.org/10.48550/arXiv.2508.15402, arXiv:2508.15402,doi:10.48550/ARXIV.2508.15402. 9 Yaacov Choueka. Theories of automata on omega-tapes: A simplified approach.J. Comput. Syst. Sci., 8(2):117–141, 1974.doi:10.1016/S0022-0000(74)80051-6. 10 Loris D’Antoni and Margus Veanes. Automata modulo theories.Commun. ACM, 64(5):86–95, 2021.doi:10.1145/34...

    work page doi:10.48550/arxiv.2508.15402 1974

  6. [7]

    pages 174--187 , doi:10.1007/978-3-031-13188-2\_9

    doi:10.1007/978-3-031-13188-2\_9. 12 Oliver Friedmann and Martin Lange. The pgsolver collection of parity game solvers. Tech- nical report,

    work page doi:10.1007/978-3-031-13188-2

  7. [8]

    14 Christoph Haase

    URL:https://www.sciencedirect.com/ science/article/pii/0304397588901363,doi:10.1016/0304-3975(88)90136-3. 14 Christoph Haase. Subclasses of presburger arithmetic and the weak EXP hierarchy. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Scienc...

    work page doi:10.1016/0304-3975(88)90136-3 2014

  8. [9]

    15 Christoph Haase

    doi:10.1145/2603088.2603092. 15 Christoph Haase. A survival guide to presburger arithmetic.ACM SIGLOG News, 5(3):67–82, 2018.doi:10.1145/3242953.3242964. 16 Philippe Heim and Rayna Dimitrova. Issy: A comprehensive tool for specification and synthesis of infinite-state reactive systems. InCAV (4), Lecture Notes in Computer Science, pages 298–312. Springer,

    work page doi:10.1145/2603088.2603092 2018

  9. [10]

    Complexity bounds for regular games

    18 Paul Hunter and Anuj Dawar. Complexity bounds for regular games. InMathematical Foundations of Computer Science 2005, pages 495–506, Berlin, Heidelberg,

    work page 2005

  10. [11]

    19 Swen Jacobs, Guillermo A

    Springer Berlin Heidelberg. 19 Swen Jacobs, Guillermo A. Pérez, Remco Abraham, Véronique Bruyère, Michaël Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, BerndFinkbeiner, AyratKhalimov, FelixKlein, MichaelLuttenberger, KlaraJ.Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-...

    work page 2018

  11. [12]

    In: Proceedings of the 16th International Symposium on Automated Technology for Verifica- tion and Analysis (ATV A’18)

    20 Jan Kretínský, Tobias Meggendorfer, and Salomon Sickert. Owl: A library for ω-words, automata, and LTL. In Shuvendu K. Lahiri and Chao Wang, editors,Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, 24 A Theory of Hanoi Omega-Automata and Games USA, October 7-10, 2018, Proceedings, volume 111...

    work page doi:10.1007/978-3-030-01090-4 2018

  12. [13]

    Infinite games played on finite graphs.Ann

    URL:https://www.sciencedirect.com/science/article/pii/ 016800729390036D,doi:10.1016/0168-0072(93)90036-D. 25 Nir Piterman. From nondeterministic büchi and streett automata to deterministic parity automata. In21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pages 255–264. IEEE Computer Society, 2006.doi:10.1109/LICS.2006.28. 26 Shmuel S...

    work page doi:10.1016/0168-0072(93)90036-d 2006

  13. [14]

    doi:10.1145/800125.804029

    Association for Computing Machinery. doi:10.1145/800125.804029. 28 Tom van Dijk, Feije van Abbema, and Naum Tomov. Knor: reactive synthesis using oink. In TACAS (1), Lecture Notes in Computer Science, pages 103–122. Springer, 2024

    work page doi:10.1145/800125.804029 2024