## 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.