On the Succinctness of Nondeterminizm

Much is known about the differences in expressiveness and succinctness
between nondeterministic and deterministic automata on infinite
words. Much less is known about the relative succinctness of the
different classes of nondeterministic automata. For example, while the
best translation from a nondeterministic Buchi automaton to a
nondeterministic co-Buchi automaton is exponential, and involves
determinization, no super-linear lower bound is known. This annoying
situation, of not being able to use the power of nondeterminizm, nor
to show its powerless, is shared by more problems, with direct
applications in formal verification.

In this paper we study a family of problems of this class.  The
problems originate from the study of the expressive power of
deterministic Buchi automata: Landweber characterizes languages L
\subseteq \Sigma^\omega that are recognizable by deterministic Buchi
automata as those for which there is a regular language R \subseteq
\Sigma^* such that L is the {\em limit\/} of R; that is, w \in L iff w
has infinitely many prefixes in R.  Two other operators that induce a
language of infinite words from a language of finite words are {\em
co-limit\/}, where w \in L iff w has only finitely many prefixes in R,
and {\em persistent-limit\/}, where w \in L iff almost all the
prefixes of w are in R.  Both co-limit and persistent-limit define
languages that are recognizable by deterministic co-Buchi
automata. They define them, however, by means of nondeterministic
automata. While co-limit is associated with complementation,
persistent-limit is associated with universality. For the three limit
operators, the deterministic automata for R and L share the same
structure. It is not clear, however, whether and how it is possible to
relate nondeterministic automata for R and L, and relate
nondeterministic automata to which different limit operators are
applied. In the paper, we show that the situation is involved: in some
cases, we are able to describe a polynomial translation, whereas in
some we present an exponential lower bound. For example, going from a
nondeterministic automaton for R to a nondeterministic automaton for
its limit is polynomial, whereas going to a nondeterministic automaton
for its persistent limit is exponential. Our results show that the
contribution of nondeterminizm to the succinctness of an automaton
does depend on its semantics.