Relating word and tree automata

Annals of Pure and Applied Logic 138 (1):126-146 (2006)
  Copy   BIBTEX

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 60s, it was known that deterministic Büchi word automata are less expressive than nondeterministic Büchi word automata. The proof is easy and can be stated in a few lines. In the late 60s, Rabin proved that Büchi 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 Büchi word automata and the expressiveness gap between Büchi 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 Büchi word automaton but not by a deterministic Büchi word automaton iff L is recognizable by a Rabin tree automaton and not by a Büchi tree automaton. Our result provides a simple explanation for the expressiveness gap between Büchi and Rabin tree automata. Since the gap between deterministic and nondeterministic Büchi word automata is well understood, our result also provides a characterization of derived languages that can be recognized by Büchi tree automata. Finally, it also provides an exponential determinization of Büchi tree automata that recognize derived languages

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

A hierarchy of tree-automatic structures.Olivier Finkel & Stevo Todorčević - 2012 - Journal of Symbolic Logic 77 (1):350-368.
Church's problem revisited.Orna Kupferman & Moshe Y. Vardi - 1999 - Bulletin of Symbolic Logic 5 (2):245-263.
Branching-time logics repeatedly referring to states.Volker Weber - 2009 - Journal of Logic, Language and Information 18 (4):593-624.
Iterating semantic automata.Shane Steinert-Threlkeld & I. I. I. Thomas F. Icard - 2013 - Linguistics and Philosophy 36 (2):151-173.
Review: Ferenc Gecseg, Magnus Steinby, Tree Automata. [REVIEW]Dirk Siefkes - 1987 - Journal of Symbolic Logic 52 (1):287-288.
Verification of concurrent programs: the automata-theoretic framework.Moshe Y. Vardi - 1991 - Annals of Pure and Applied Logic 51 (1-2):79-98.
Modifiable automata self-modifying automata.J.-P. Moulin - 1992 - Acta Biotheoretica 40 (2-3):195-204.
Basic Properties of Quantum Automata.Stanley Gudder - 2000 - Foundations of Physics 30 (2):301-319.
Fragility and indestructibility of the tree property.Spencer Unger - 2012 - Archive for Mathematical Logic 51 (5-6):635-645.
Cellularity of Pseudo-Tree Algebras.Jennifer Brown - 2006 - Notre Dame Journal of Formal Logic 47 (3):353-359.

Analytics

Added to PP
2013-12-31

Downloads
28 (#490,139)

6 months
1 (#1,040,386)

Historical graph of downloads
How can I increase my downloads?