A data word (resp. a data tree) is a fi-nite word (resp. tree) whose every position carries a letter from a fi-nite alphabet and a datum form an infi-nite domain. In this thesis we investigate automata and logics for data words and data trees with decidable reasoning problems: we focus on the emptiness problem in the case of automata, and the satisfi-ability problem in the case of logics. On data words, we present a decidable extension of the model of alternating register automata studied by Demri and Lazi'c. Further, we show the decidability of the satisfi-ability problem for the linear-time temporal logic on data words LTL_\downarrow (X, F, U) (studied by Demri and Lazi'c) with quantifi-cation over data values. We also prove that the lower bounds of non-primitive recursiveness shown by Demri and Lazi'c for LTL↓- (X, F) carry over to LTL↓- (F). On data trees, we consider three decidable automata models with diff-erent characteristics. We fi-rst introduce the Downward Data automaton (DD automata). Its execution consists in a transduction of the fi-nite labeling of the tree, and a verifi-cation of data properties for every subtree of the transduced tree. This model is closed under boolean operations, but the tests it can make on the order of the siblings is very limited. Its emptiness problem is 2ExpTime. On the contrary, the other two automata models we introduce have an emptiness problem with a non-primitive recursive complexity, and are closed under intersection and union, but not complementation. They are both alternating automata with one register to store and compare data values. The automata class ATRA(guess, spread) extends the top-down automata ATRA of Jurdzinski and Lazic. We exhibit similar decidable extensions as the one showed in the case of data words. This class can test for any tree regular language--in contrast to DD automata. Finally, we consider a bottom-up alternating tree automaton with one register (called BUDA). Although the BUDA class is one-way, it has features that allow to test data properties by navigating the tree in both directions: upward and downward. In opposition to ATRA(guess, spread), this automaton cannot test for properties on the the sequence of siblings (like, for example, the order in which labels appear). All these three models have connections with the logic XPath--a logic conceived for xml documents, which can be seen as data trees. Through the aforementioned automata we show that the satisfi-ability of three natural fragments of XPath are decidable. These fragments are: downward XPath, where navigation can only be done by child and descendant axes- forward XPath, where navigation also contains the next sibling axis and its transitive closure- and vertical XPath, whose navigation consists in the child, descendant, parent and ancestor axes. Whereas downward XPath is ExpTime-complete, forward and vertical XPath have non-primitive recursive lower bounds.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00718605 |
| Date | 06 December 2010 |
| Creators | Figueira, Diego |
| Publisher | École normale supérieure de Cachan - ENS Cachan |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | English |
| Type | PhD thesis |
Page generated in 0.0022 seconds