Solving games without determinization

Abstract

The synthesis of reactive systems requires the solution of two-player games on graphs with ω-regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Büchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, doterminization for automata on infinite words is osxtremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given non-deterministic Büchi automaton, an equivalent nondeterministic parity automaton P that is good for solving games with objective P. The main insight is that a nondeterministic automaton is good for solving games if it fairly simulates the equivalent deterministic automaton. In this way, we omit the determinization step in game solving and reactive synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation. and allows an incremental search for winning strategies. © Springer-Verlag Berlin Heidelberg 2006.