The Emptiness Problem for Tree Automata with Global Constraints

Luis Barguñó 1 Carlos Creus 1 Guillem Godoy 1 Florent Jacquemard 2 Camille Vacher 3, 4
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
4 MOSTRARE - Modeling Tree Structures, Machine Learning, and Information Extraction
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
Abstract : We define tree automata with global constraints (TAGC), generalizing the class of tree automata with global equality and disequality constraints of Filiot, Talbot and Tison 2008 (TAGED). TAGC can test for equality and disequality between subterms whose positions are defined by the states reached during a computation. In particular, TAGC can check that all the subterms reaching a given state are distinct. This constraint is related to monadic key constraints for XML documents, meaning that every two distinct positions of a given type have different values. We prove decidability of the emptiness problem for TAGC. This solves, in particular, the open question of decidability of emptiness for TAGED. We further extend our result by allowing global arithmetic constraints for counting the number of occurrences of some state or the number of different subterms reaching some state during a computation. We also allow local equality and disequality tests between sibling positions and the extension to unranked ordered trees. As a consequence of our results for TAGC, we prove the decidability of a fragment of the monadic second order logic on trees extended with predicates for equality and disequality between subtrees, and cardinality.
Type de document :
Communication dans un congrès
Jouannaud, Jean-Pierre. 25th Annual IEEE Symposium on Logic in Computer Science (LICS), Jul 2010, Edinburgh, Scotland, United Kingdom. IEEE Computer Society Press, pp.263-272, 2010, 〈http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5571714〉. 〈10.1109/LICS.2010.28〉
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00578901
Contributeur : Florent Jacquemard <>
Soumis le : mardi 22 mars 2011 - 16:11:01
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : jeudi 23 juin 2011 - 02:49:13

Fichier

globalconstraints-IEEE.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Luis Barguñó, Carlos Creus, Guillem Godoy, Florent Jacquemard, Camille Vacher. The Emptiness Problem for Tree Automata with Global Constraints. Jouannaud, Jean-Pierre. 25th Annual IEEE Symposium on Logic in Computer Science (LICS), Jul 2010, Edinburgh, Scotland, United Kingdom. IEEE Computer Society Press, pp.263-272, 2010, 〈http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5571714〉. 〈10.1109/LICS.2010.28〉. 〈inria-00578901〉

Partager

Métriques

Consultations de la notice

375

Téléchargements de fichiers

254