Relating Word and Tree Automata
-------------------------------
In the automata-theoretic approach to verification, we translate
specifications to automata. Complexity considerations
motivate the distinction between different types of automata.
Already in the 60's, it was known that deterministic Buchi
word automata are less expressive than nondeterministic Buchi word
automata. The proof is easy and can be stated in a few lines.
In the late 60's, Rabin proved that Buchi tree automata are less
expressive than Rabin tree automata. This proof is much harder.
In this work we relate the expressiveness gap between deterministic
and nondeterministic Buchi word automata and the expressiveness gap
between Buchi and Rabin tree automata.
We consider tree automata that recognize derived languages. For
a word language $L$, the derived language of $L$, denoted $\derT{L}$,
is the set of all trees all of whose paths are in $L$. Since often we
want to specify that all the computations of the program satisfy some
property, the interest in derived languages is clear.
Our main result shows that $L$ is recognizable by a nondeterministic
Buchi word automaton but not by a deterministic Buchi word
automaton iff $\derT{L}$ is recognizable by a Rabin tree automaton and
not by a Buchi tree automaton. Our result provides a simple
explanation to the expressiveness gap between Buchi and Rabin tree
automata. Since the gap between deterministic and nondeterministic
Buchi word automata is well understood, our result also provides a
characterization of derived languages that can be recognized by Buchi
tree automata. Finally, it also provides an exponential
determinization of Buchi tree automata that recognize derived
languages.