Abstract:

One of the most ambitious goals in the field of verification is
to automatically produce designs from their specifications, a
process called {\em synthesis}. We are interested in {\em
reactive systems}, systems that continuously interact with other
programs, users, or their environment (like operating systems or
CPUs). The complexity of reactive system does not necessarily
arise from computing complicated functions but rather from the
fact that they have to be able to react to all possible inputs
and maintain their behavior forever. The most appropriate way to
consider synthesis is by considering two-sided games between the
system and the environment. The environment tries to falsify the
specification and the system tries to satisfy it. Every system
move (the way the system handles its internal variables) has to
match all possible future moves of the environment. The system
wins the game if it has a strategy such that all infinite traces
satisfy the specification.

When the specification is a {\em linear temporal logic} formula
or a {\em nondeterministic B\"uchi automaton}, the problem is
reduced to solving simpler games by constructing deterministic
automata. However, determinization for automata on infinite
words is extremely complicated. Here we show how to construct
nondeterministic automata that can replace deterministic
automata in the context of games and synthesis. The fact that
our automata are nondeterministic makes them surprisingly
simple, amenable to symbolic implementation, and allows a
natural hierarchy of automata of increasing complexity that lead
to the full solution.