Avoiding Determinization

Automata on infinite objects are extensively used in system
specification, verification, and synthesis.  While some applications
of the automata-theoretic approach have been well accepted by the
industry, some have not yet been reduced to practice.  Applications
that involve determinization of automata on infinite words have been
doomed to belong to the second category. This has to do with the
intricacy of Safra's optimal determinization construction, the fact
that the state space that results from determinization is awfully
complex and is not amenable to optimizations and a symbolic
implementation, and the fact that determinization requires the
introduction of acceptance conditions that are more complex than the
B\"uchi acceptance condition.  Examples of applications that involve
determinization and belong to the unfortunate second category include
model checking of $\omega$-regular properties, decidability of
branching temporal logics, and synthesis and control of open systems.

We offer an alternative to the standard automata-theoretic
approach. The crux of our approach is avoiding determinization.  Our
approach goes instead via universal co-B\"uchi automata. Like
nondeterministic automata, universal automata may have several runs on
every input. Here, however, an input is accepted if all of the runs
are accepting. We show how the use of universal automata simplifies
significantly known complementation constructions for automata on
infinite words, known decision procedures for branching temporal
logics, known synthesis algorithms, and other applications that are
now based on determinization. Our algorithms are less difficult to
implement and have practical advantages like being amenable to
optimizations and a symbolic implementation.