Solving Games without Determinization

Thomas A. Henzinger and Nir Piterman

The synthesis of reactive systems requires the solution of two-player games on graphs with omega-regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Buchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, determinization for automata on infinite words is extremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given nondeterministic Buchi automaton, an equivalent nondeterministic parity automaton N that is good for solving games with objective N. 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.

Proceedings of the International Conference for Computer Science Logic (CSL), Lecture Notes in Computer Science 4207, Springer, 2006, pp. 395-410.

Download inofficial, sometimes updated PostScript / PDF document. © 2006 Springer.