On determinisation of good-for-games automata

Abstract

In this work we study Good-For-Games (GFG) automata over ω-words: non-deterministic automata where the non-determinism can be resolved by a strategy depending only on the prefix of the ω-word read so far. These automata retain some advantages of determinism: they can be composed with games and trees in a sound way, and inclusion L(A) ⊇ L(B) can be reduced to a parity game over A × B if A is GFG. Therefore, they could be used to some advantage in verification, for instance as solutions to the synthesis problem. The main results of this work answer the question whether parity GFG automata actually present an improvement in terms of state complexity (the number of states) compared to the deterministic ones. We show that a frontier lies between the Büchi condition, where GFG automata can be determinised with only quadratic blow-up in state complexity; and the co-Büchi condition, where GFG automata can be exponentially smaller than any deterministic automaton for the same language. We also study the complexity of deciding whether a given automaton is GFG.