On the Succinctness of Nondeterminism

Much is known about the differences in expressiveness and succinctness be- tween 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 B ¨ uchi automaton to a nondeter- ministic 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 non- determinism, nor to show that it is powerless, is shared by more problems, with direct ap- plications 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 ! that are recognizable by deterministic B ¨ uchi automata as those for which there is a regular language R such that L is the limit of R; that is, w 2 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 co-limit, where w 2 L iff w has only finitely many prefixes in R, and persistent-limit, where w 2 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-B ¨ uchi 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, or to 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 nondeterminism to the succinctness of an automaton does depend upon its semantics.