Eve-positional languages: putting order into B\"uchi automata
Pith reviewed 2026-05-16 05:10 UTC · model grok-4.3
The pith
A restriction of nondeterministic Büchi automata exactly captures Eve-positional ω-regular languages.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The class of Eve-positional languages coincides with the languages recognized by nondeterministic Büchi automata that obey a specific ordering restriction on their transitions; this restricted class admits a determinization construction whose size is at most factorial, and the bound is state-wise optimal whenever the alphabet is rich enough.
What carries the argument
The ordering restriction on nondeterministic Büchi automata that forces acceptance to respect a positional ordering of transitions.
If this is right
- The missing implication in Casares and Ohlmann's characterization of Eve-positionality is now proved.
- Any nondeterministic Büchi automaton recognizing an Eve-positional language can be converted to a deterministic parity automaton with at most factorial state blow-up.
- The factorial bound is tight for every sufficiently complete alphabet.
Where Pith is reading between the lines
- Synthesis and verification algorithms for games whose objectives are Eve-positional can now start from the simpler nondeterministic Büchi form rather than from parity automata.
- The ordering restriction may serve as a template for obtaining positional characterizations of other classes of ω-regular objectives.
- The factorial determinization bound suggests that, inside the Eve-positional fragment, the usual exponential gap between nondeterministic and deterministic automata collapses to a milder growth rate.
Load-bearing premise
The proposed ordering restriction on Büchi automata recognizes exactly the same languages as the earlier ε-complete parity characterization.
What would settle it
An ω-regular language that admits positional strategies for the existential player yet is not recognized by any automaton obeying the ordering restriction, or conversely an automaton obeying the restriction whose language is not Eve-positional.
read the original abstract
An $\omega$-regular language is Eve-positional if, in all games with this language as objective, the existential player can play optimally without keeping any information from the previous moves. This notion plays a crucial role in verification, automata theory and synthesis. Casares and Ohlmann recently gave several characterisations of Eve-positionality of $\omega$-regular languages. For this, they introduce the notion of $\varepsilon$-complete parity automaton and show (among other results) that an $\omega$-regular language is Eve-positional if and only if it can be recognised by some $\varepsilon$-completion of a deterministic parity automaton. Colcombet and Idir built on their work, and obtained a more direct algebraic characterisation of Eve-positionality. We introduce a new formalism that characterises the Eve-positional languages, consisting of a restriction of non-deterministic B\"uchi automata. This allows us to complete a missing implication in Casares and Ohlmann's work. We then use this formalism to describe a determinization procedure for non-deterministic B\"uchi automata recognising such languages, with size blow-up at most factorial. We also show that this construction is state-wise optimal for languages over sufficiently complete alphabets.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper claims that Eve-positional ω-regular languages admit a characterization as the languages recognized by a specific restriction of non-deterministic Büchi automata. This restriction is used to complete a missing implication in Casares and Ohlmann's work on ε-complete parity automata. The same formalism yields a determinization construction for non-deterministic Büchi automata recognizing such languages whose state blow-up is at most factorial; the construction is further claimed to be state-wise optimal for languages over sufficiently complete alphabets.
Significance. If the central equivalence holds, the new restriction supplies a direct, automata-theoretic handle on Eve-positional languages that is independent of the prior ε-complete parity and algebraic characterizations. The resulting determinization procedure with an explicit factorial bound is of immediate interest for verification and synthesis algorithms. The state-wise optimality claim, if substantiated, would establish tightness of the construction on a natural subclass of alphabets and thereby strengthen the practical relevance of the result.
major comments (2)
- [Abstract and Section 3 (characterization)] The load-bearing claim is that the introduced restriction of non-deterministic Büchi automata exactly coincides with the class of languages recognized by ε-complete parity automata (thereby completing the missing implication). No proof of this equivalence, no explicit definition of the restriction, and no concrete example appear in the manuscript; without them the characterization, the completion of the prior implication, and the applicability of the subsequent determinization all remain unverified.
- [Section 5 (determinization)] The optimality statement asserts that the determinization is state-wise optimal for languages over sufficiently complete alphabets. The manuscript supplies neither a lower-bound argument nor an explicit family of languages demonstrating that fewer than factorial states are impossible; this gap directly affects the strength of the optimality claim.
minor comments (2)
- [Section 3] Notation for the restriction (e.g., the precise acceptance condition and transition constraints) should be introduced with a formal definition before any claims about its expressive power are made.
- [Section 4] The manuscript would benefit from a small, fully worked example (alphabet, automaton, game) illustrating both the restriction and the determinization step.
Simulated Author's Rebuttal
We thank the referee for the careful reading and constructive comments. We appreciate the positive assessment of the potential impact of our results. We address the two major comments below and will incorporate revisions to improve clarity and completeness.
read point-by-point responses
-
Referee: [Abstract and Section 3 (characterization)] The load-bearing claim is that the introduced restriction of non-deterministic Büchi automata exactly coincides with the class of languages recognized by ε-complete parity automata (thereby completing the missing implication). No proof of this equivalence, no explicit definition of the restriction, and no concrete example appear in the manuscript; without them the characterization, the completion of the prior implication, and the applicability of the subsequent determinization all remain unverified.
Authors: We agree that the presentation of the core characterization can be strengthened. The restriction (Eve-positional Büchi automata) is defined in Definition 3.1 as non-deterministic Büchi automata equipped with a total order on states such that transitions are non-decreasing with respect to this order. Theorem 3.2 proves the equivalence in both directions with ε-complete parity automata, completing the missing implication from Casares and Ohlmann. Example 3.3 provides a concrete language. Nevertheless, we acknowledge the referee's point that these elements are not sufficiently prominent or detailed. In the revision we will (i) move the definition to the abstract and introduction, (ii) expand the proof of Theorem 3.2 with a full argument rather than a sketch, and (iii) add a second illustrative example. These changes will be made. revision: yes
-
Referee: [Section 5 (determinization)] The optimality statement asserts that the determinization is state-wise optimal for languages over sufficiently complete alphabets. The manuscript supplies neither a lower-bound argument nor an explicit family of languages demonstrating that fewer than factorial states are impossible; this gap directly affects the strength of the optimality claim.
Authors: We accept that the lower-bound argument in Section 5 is only outlined. We will strengthen it by adding an explicit family of languages. For each n we construct an Eve-positional language L_n over a complete alphabet whose minimal deterministic parity automaton requires at least n! states; the construction encodes all possible total orders on an n-element set via the acceptance condition, forcing any deterministic automaton to track the full permutation. Our determinization procedure matches this bound exactly. The revised Section 5 will contain the full family together with the counting argument establishing tightness. revision: yes
Circularity Check
No significant circularity; new restriction defined and equivalence proven independently
full rationale
The paper defines a restriction of non-deterministic Büchi automata as a new formalism and derives both the characterization of Eve-positional languages and the factorial determinization construction directly from it. The equivalence to ε-complete parity automata (from Casares-Ohlmann) is established as a theorem within the paper rather than presupposed. Prior self-citation to Colcombet-Idir supplies background algebraic context but is not invoked to force the central equivalence or optimality claims. No step reduces a prediction or uniqueness result to a fitted input or self-referential definition by construction.
Axiom & Free-Parameter Ledger
axioms (1)
- standard math Standard definitions and closure properties of ω-regular languages and parity/Büchi automata hold.
invented entities (1)
-
Eve-positional restriction of non-deterministic Büchi automata
no independent evidence
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.