Title :
Relating word and tree automata
Author :
Kupferman, Orna ; Safra, Shmuel ; Vardi, Moshe Y.
Author_Institution :
AT&T Bell Labs., Murray Hill, NJ, USA
Abstract :
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 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 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
Keywords :
computational complexity; deterministic automata; formal specification; formal verification; temporal logic; tree data structures; Buchi tree automata; Rabin tree automaton; automata-theoretic approach; computational Complexity; derived languages; deterministic Buchi word automata; formal specification; formal verification; nondeterministic Buchi word automata; tree automata; word automata; Automata; Computer science; Logic; Mathematics; Specification languages; Uniform resource locators;
Conference_Titel :
Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on
Conference_Location :
New Brunswick, NJ
Print_ISBN :
0-8186-7463-6
DOI :
10.1109/LICS.1996.561360