Good-for-Games (GFG) automata are nondeterministic automata on infinite words, for which there is a strategy to resolve the non-determinism depending only on the prefix of the word read so far.
They offer an intermediate model between determinism and nondeterminism, retaining advantages from both sides. This makes them well suited tools for verification, for instance towards solving the Church Synthesis problem. After describing basic properties and examples, I will present recent results on this model. We focus on two particular problems: are GFG automata more succinct than deterministic ones, and what is the complexity of deciding whether an automaton is GFG ?
This is joint work with Michał Skrzypczak.