Bottom-up automata on data trees and vertical XPath

Diego Figueira 1, 2, 3 Luc Segoufin 4, 5
4 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
5 VALDA - Value from Data
DI-ENS - Département d'informatique de l'École normale supérieure, Inria de Paris
Abstract : A data tree is a finite tree whose every node carries a label from a finite alphabet and a datum from some infinite domain. We introduce a new model of automata over unranked data trees with a decidable emptiness problem. It is essentially a bottom-up alternating automaton with one register that can store one data value and can be used to perform equality tests with the data values occurring within the subtree of the current node. We show that it captures the expressive power of the vertical fragment of XPath - containing the child, descendant, parent and ancestor axes - obtaining thus a decision procedure for its satisfiability problem.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, 13 (4), 〈10.23638/LMCS-13(4:5)2017〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01631219
Contributeur : Luc Segoufin <>
Soumis le : mardi 20 février 2018 - 14:15:37
Dernière modification le : mardi 19 juin 2018 - 10:44:02
Document(s) archivé(s) le : lundi 21 mai 2018 - 12:53:15

Fichier

1710.08748.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Diego Figueira, Luc Segoufin. Bottom-up automata on data trees and vertical XPath. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, 13 (4), 〈10.23638/LMCS-13(4:5)2017〉. 〈hal-01631219〉

Partager

Métriques

Consultations de la notice

226

Téléchargements de fichiers

25