Visibly Tree Automata with Memory and Constraints

Hubert Comon-Lundh 1 Florent Jacquemard 1, 2 Nicolas Perrin 3, 4
2 DAHU - Verification in databases
CNRS - Centre National de la Recherche Scientifique : UMR8643, Inria Saclay - Ile de France, ENS Cachan - École normale supérieure - Cachan, LSV - Laboratoire Spécification et Vérification [Cachan]
Abstract : Tree automata with one memory have been introduced in 2001. They generalize both pushdown (word) automata and the tree automata with constraints of equality between brothers of Bogaert and Tison. Though it has a decidable emptiness problem, the main weakness of this model is its lack of good closure properties. We propose a generalization of the visibly pushdown automata of Alur and Madhusudan to a family of tree recognizers which carry along their (bottom-up) computation an auxiliary unbounded memory with a tree structure (instead of a symbol stack). In other words, these recognizers, called Visibly Tree Automata with Memory (VTAM) define a subclass of tree automata with one memory enjoying Boolean closure properties. We show in particular that they can be determinized and the problems like emptiness, membership, inclusion and universality are decidable for VTAM. Moreover, we propose several extensions of VTAM whose transitions may be constrained by different kinds of tests between memories and also constraints a la Bogaert and Tison. We show that some of these classes of constrained VTAM keep the good closure and decidability properties, and we demonstrate their expressiveness with relevant examples of tree languages.
Document type :
Journal articles
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/inria-00578844
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 2:38:17 PM
Last modification on : Thursday, July 4, 2019 - 3:56:24 PM
Long-term archiving on : Thursday, June 23, 2011 - 2:45:08 AM

File

VTAM-LMCS.pdf
Files produced by the author(s)

Identifiers

Citation

Hubert Comon-Lundh, Florent Jacquemard, Nicolas Perrin. Visibly Tree Automata with Memory and Constraints. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2008, 4 (2), ⟨http://arxiv.org/pdf/0804.3065⟩. ⟨10.2168/LMCS-4(2:8)2008⟩. ⟨inria-00578844⟩

Share

Metrics

Record views

387

Files downloads

283