pith. sign in

arxiv: 1906.11624 · v2 · pith:6Z6XXXYFnew · submitted 2019-06-27 · 💻 cs.FL

Good for Games Automata: From Nondeterminism to Alternation

Udi Boker , Karoliina Lehtinen This is my paper

Pith reviewed 2026-05-25 13:51 UTC · model grok-4.3

classification 💻 cs.FL
keywords good-for-games automataalternating automatahistory-deterministic automataBüchi automataco-Büchi automataautomata expressivenessword automatagame automata
0
0 comments X

The pith

Alternating good-for-games automata recognize exactly the same languages as deterministic automata with the same acceptance conditions and indices.

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

A word automaton is good for games if composing it with any game whose winning condition is the automaton's language does not change the winner. Several properties have been used to identify nondeterministic automata that are good for games, but their equivalence had not been proved. The paper extends each of those properties to alternating automata and proves the extensions remain equivalent to one another. It further proves that any language recognized by an alternating good-for-games automaton is also recognized by some deterministic automaton using the same acceptance condition and index.

Core claim

We generalize all of these definitions to alternating automata and show their equivalence. We further show that alternating GFG automata are as expressive as deterministic automata with the same acceptance conditions and indices.

What carries the argument

The generalized GFG properties (history-deterministic, letter-game compliant, good for trees, good for composition) for alternating automata and the proofs that they coincide.

If this is right

  • Alternating GFG automata over finite words are not more succinct than deterministic automata.
  • Weak alternating GFG automata over infinite words are not more succinct than deterministic automata.
  • Converting an alternating GFG Büchi or co-Büchi automaton to a deterministic one requires a 2^Θ(n) state blow-up.
  • The question remains open whether alternating GFG automata with stronger acceptance conditions can be doubly-exponentially more succinct than deterministic ones.

Where Pith is reading between the lines

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

  • The equivalence implies that, once restricted to the GFG subclass, alternation adds no extra expressive power over determinism.
  • Game-solving algorithms that rely on deterministic automata could safely substitute alternating GFG automata without changing correctness, provided the acceptance condition is preserved.
  • The single-exponential determinization bound for Büchi and co-Büchi cases suggests that the GFG restriction removes the usual extra exponential cost of alternation.

Load-bearing premise

Extending each GFG property from the nondeterministic setting to alternating automata preserves the original meaning and does not create unintended distinctions among the properties.

What would settle it

An alternating automaton that meets one generalized GFG definition but fails another, or an alternating GFG automaton whose language cannot be recognized by any deterministic automaton with matching acceptance condition and index.

read the original abstract

A word automaton recognizing a language $L$ is good for games (GFG) if its composition with any game with winning condition $L$ preserves the game's winner. While all deterministic automata are GFG, some nondeterministic automata are not. There are various other properties that are used in the literature for defining that a nondeterministic automaton is GFG, including "history-deterministic", "compliant with some letter game", "good for trees", and "good for composition with other automata". The equivalence of these properties has not been formally shown. We generalize all of these definitions to alternating automata and show their equivalence. We further show that alternating GFG automata are as expressive as deterministic automata with the same acceptance conditions and indices. We then show that alternating GFG automata over finite words, and weak automata over infinite words, are not more succinct than deterministic automata, and that determinizing B\"uchi and co-B\"uchi alternating GFG automata involves a $2^{\Theta(n)}$ state blow-up. We leave open the question of whether alternating GFG automata of stronger acceptance conditions allow for doubly-exponential succinctness compared to deterministic automata.

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 / 2 minor

Summary. The paper generalizes several GFG properties (history-deterministic, letter-game compliant, good for trees, good for composition) from nondeterministic to alternating automata, proves their equivalence, and shows that alternating GFG automata recognize exactly the languages recognized by deterministic automata with the same acceptance conditions and indices. It further proves that alternating GFG automata over finite words and weak automata over infinite words are not more succinct than deterministic automata, establishes a 2^Θ(n) state blow-up for determinizing alternating Büchi and co-Büchi GFG automata, and leaves open whether stronger acceptance conditions permit doubly-exponential succinctness.

Significance. If the equivalences and expressiveness results hold, the work unifies disparate GFG characterizations in the alternating setting and clarifies that GFG alternation does not increase expressive power beyond determinism. The succinctness and determinization bounds supply concrete complexity information for finite-word, weak, Büchi, and co-Büchi cases. These contributions strengthen the automata-theoretic toolkit for games and verification.

minor comments (2)
  1. The abstract uses the term 'indices' in the expressiveness claim; a brief parenthetical reminder of the standard definition (e.g., parity index) in §2 would aid readers unfamiliar with the nondeterministic case.
  2. The open question on doubly-exponential succinctness for stronger conditions is stated clearly but would benefit from a short paragraph in the conclusion sketching why the current techniques do not extend.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment and recommendation to accept the paper. The summary accurately captures the main results on generalizing GFG properties to alternating automata, proving equivalences, and establishing expressiveness and succinctness bounds.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper generalizes existing GFG definitions (history-deterministic, letter-game compliant, good for trees, good for composition) from nondeterministic to alternating automata, proves their equivalence via direct arguments, and establishes expressiveness equivalence to deterministic automata under matching acceptance conditions. These steps consist of standard automata-theoretic definitions and equivalence proofs with no reduction of results to fitted parameters, self-definitional constructions, or load-bearing self-citations. The abstract explicitly notes that prior equivalence was unproven, indicating the work supplies independent content rather than renaming or smuggling prior results by the same authors. No equations or claims in the provided text exhibit the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The results rest on the standard mathematical definitions of word automata, acceptance conditions, and game composition; no new free parameters, invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)
  • standard math Standard definitions of deterministic, nondeterministic, and alternating word automata together with acceptance conditions (Buchi, co-Buchi, weak).
    The generalization and equivalence statements are built directly on these background definitions.

pith-pipeline@v0.9.0 · 5733 in / 1260 out tokens · 39565 ms · 2026-05-25T13:51:51.507748+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

23 extracted references · 23 canonical work pages

  1. [1]

    An automata toolbox

    Miko aj Bojanczyk and Wojciech Czerwinski. An automata toolbox. Technical report, University of Warsaw, 2018

    work page 2018

  2. [2]

    Why these automata types? In Proceedings of LPAR , pages 143--163, 2018

    Udi Boker. Why these automata types? In Proceedings of LPAR , pages 143--163, 2018

    work page 2018

  3. [3]

    Nondeterminism in the presence of a diverse or unknown future

    Udi Boker, Denis Kuperberg, Orna Kupferman, and Micha Skrzypczak. Nondeterminism in the presence of a diverse or unknown future. In Proceedings of ICALP , pages 89--100, 2013

    work page 2013

  4. [4]

    How deterministic are good-for-games automata? In Proceedings of FSTTCS , pages 18:1--18:14, 2017

    Udi Boker, Orna Kupferman, and Micha Skrzypczak . How deterministic are good-for-games automata? In Proceedings of FSTTCS , pages 18:1--18:14, 2017

    work page 2017

  5. [5]

    Alternation removal in B\"uchi automata

    Udi Boker, Orna Kupferman, and Adin Rosenberg. Alternation removal in B\"uchi automata. In Proceedings of ICALP , pages 76--87, 2010

    work page 2010

  6. [6]

    Register games

    Udi Boker and Karoliina Lehtinen. Register games. Submitted to Logical Methods in Computer Science

    work page

  7. [7]

    On the way to alternating weak automata

    Udi Boker and Karoliina Lehtinen. On the way to alternating weak automata. In Proceedings of FSTTCS , 2018

    work page 2018

  8. [8]

    Good for games automata: From nondeterminism to alternation

    Udi Boker and Karoliina Lehtinen. Good for games automata: From nondeterminism to alternation. arXiv:..., 2019

    work page 2019

  9. [9]

    Solving sequential conditions by finite-state strategies

    J Richard B \"u chi and Lawrence H Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society , 138:295--311, 1969

    work page 1969

  10. [10]

    Deciding parity games in quasipolynomial time

    Cristian S Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Proceedings of STOC , pages 252--263, 2017

    work page 2017

  11. [11]

    The theory of stabilisation monoids and regular cost functions

    Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In Proceedings of ICALP , pages 139--150, 2009

    work page 2009

  12. [12]

    Forms of determinism for automata

    Thomas Colcombet. Forms of determinism for automata. In Proceedings of STACS , pages 1--23, 2012

    work page 2012

  13. [13]

    Fonctions r \'e guli \`e res de co \^u t

    Thomas Colcombet. Fonctions r \'e guli \`e res de co \^u t. Habilitation \`a diriger les recherches, \'E cole Doctorale de Sciences Math \'e matiques de Paris Centre , 2013

    work page 2013

  14. [14]

    Universal graphs and good for small games automata: New tools for infinite duration games

    Thomas Colcombet and Nathana \"e l Fijalkow. Universal graphs and good for small games automata: New tools for infinite duration games. In FOSSACS , 2019

    work page 2019

  15. [15]

    Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games

    Wojciech Czerwi \'n ski, Laure Daviaud, Nathana \"e l Fijalkow, Marcin Jurdzi \'n skit, Ranko Lazi \'c , and Pawel Parys. Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. In Proceedings of SODA , pages 2333--2349, 2019

    work page 2019

  16. [16]

    Alternating weak automata from universal trees

    Laure Daviaud, Marcin Jurdzinski, and Karoliina Lehtinen. Alternating weak automata from universal trees. In CONCUR , 2019

    work page 2019

  17. [17]

    Solving games without determinization

    Thomas Henzinger and Nir Piterman. Solving games without determinization. In Proceedings of CSL , pages 395--410, 2006

    work page 2006

  18. [18]

    On determinisation of good-for-games automata

    Denis Kuperberg and Micha Skrzypczak. On determinisation of good-for-games automata. In Proceedings of ICALP , pages 299--310, 2015

    work page 2015

  19. [19]

    Relating word and tree automata

    Orna Kupferman, Shmuel Safra, and Moshe Y Vardi. Relating word and tree automata. Ann. Pure Appl. Logic , 138(1-3):126--146, 2006. Conference version in 1996

    work page 2006

  20. [20]

    A modal perspective on solving parity games in quasi-polynomial time

    Karoliina Lehtinen. A modal perspective on solving parity games in quasi-polynomial time. In Proceedings of LICS , pages 639--648, 2018

    work page 2018

  21. [21]

    Efficient minimization of deterministic weak omega-automata

    Cristof L \"o ding. Efficient minimization of deterministic weak omega-automata. Information Processing Letters , 79(3):105--109, 2001

    work page 2001

  22. [22]

    Alternating finite automata on -words

    Satoru Miyano and Takeshi Hayashi. Alternating finite automata on -words. Theoretical Computer Science , 32:321--330, 1984

    work page 1984

  23. [23]

    Expressiveness results at the bottom of the -regular hierarchy

    Gila Morgenstern. Expressiveness results at the bottom of the -regular hierarchy. M.Sc. Thesis, The Hebrew University, 2003

    work page 2003