Skip to Main content Skip to Navigation
New interface
Journal articles

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], Inria Saclay - Ile de France
5 VALDA - Value from Data
DI-ENS - Département d'informatique - ENS Paris, 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.
Document type :
Journal articles
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download
Contributor : Luc Segoufin Connect in order to contact the contributor
Submitted on : Tuesday, February 20, 2018 - 2:15:37 PM
Last modification on : Friday, July 8, 2022 - 10:08:01 AM
Long-term archiving on: : Monday, May 21, 2018 - 12:53:15 PM


Files produced by the author(s)



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



Record views


Files downloads