An Isaac Newton Institute Programme

Logic and Algorithms

Avoiding determinization

13th February 2006

Authors: Orna Kupferman (Hebrew University of Jerusalem), Moshe Vardi (Rice)

Abstract

Nondeterministic automata may have several runs on every input, and an input is accepted if one of the runs is accepting. In contrast, deterministic automata have a single run on every input. The existential mode of nondeterministic automata is an obstacle in many applications. For example, complementing a nondeterministic automaton A cannot be done by dualizing its acceptance condition. Likewise, running A on all branches of a tree, which is needed in decision procedures for high-order logics, game solving, and open-system synthesis, results in a tree automaton that accepts a subset of the trees all of whose branches are accepted by A. The standard solution for coping with this obstacle is to determinize A. This gives rise to yet another obstacle: determinization of automata on infinite words is very complicated. Safra's optimal determinization algorithm is highly nontrivial and indeed this approach proved to be not too amenable to implementation.

We offer an alternative to the standard automata-theoretic approach. The crux of our approach is avoiding determinization. Our approach goes instead via universal 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 high-order 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.