How Deterministic are Good-For-Games Automata?

TL;DR

This paper investigates the properties of Good-For-Games automata, showing they can be exponentially more succinct than deterministic automata and possess typeness similar to deterministic automata, with implications for automata translation and complementation.

Contribution

It proves that GFG automata enjoy typeness properties akin to deterministic automata and analyzes their position between deterministic and nondeterministic automata.

Findings

GFG automata can be exponentially more succinct than deterministic automata.

GFG automata exhibit typeness, allowing simpler equivalent automata with weaker acceptance conditions.

Complementation of GFG automata can incur exponential state blow-up, similar to nondeterministic automata.

Abstract

In GFG automata, it is possible to resolve nondeterminism in a way that only depends on the past and still accepts all the words in the language. The motivation for GFG automata comes from their adequacy for games and synthesis, wherein general nondeterminism is inappropriate. We continue the ongoing effort of studying the power of nondeterminism in GFG automata. Initial indications have hinted that every GFG automaton embodies a deterministic one. Today we know that this is not the case, and in fact GFG automata may be exponentially more succinct than deterministic ones. We focus on the typeness question, namely the question of whether a GFG automaton with a certain acceptance condition has an equivalent GFG automaton with a weaker acceptance condition on the same structure. Beyond the theoretical interest in studying typeness, its existence implies efficient translations among different acceptance conditions. This practical issue is of special interest in the context of games, where the Buchi and co-Buchi conditions admit memoryless strategies for both players. Typeness is known to hold for deterministic automata and not to hold for general nondeterministic automata. We show that GFG automata enjoy the benefits of typeness, similarly to the case of deterministic automata. In particular, when Rabin or Streett GFG automata have equivalent Buchi or co-Buchi GFG automata, respectively, then such equivalent automata can be defined on a substructure of the original automata. Using our typeness results, we further study the place of GFG automata in between deterministic and nondeterministic ones. Specifically, considering automata complementation, we show that GFG automata lean toward nondeterministic ones, admitting an exponential state blow-up in the complementation of a Streett automaton into a Rabin automaton, as opposed to the constant blow-up in the deterministic case.