Model Theory of XPath on Data Trees. Part I: Bisimulation and Characterization
D. Figueira, S. Figueira, and C. Areces. Model Theory of XPath on Data Trees. Part I: Bisimulation and Characterization. Journal of Artificial Intelligence Research, 53:271–314, 2015.
Download
Abstract
We investigate model theoretic properties of XPath with data (in)equality tests over the class of data trees, i.e., the class of trees where each node contains a label from a finite alphabet and a data value from an infinite domain. We provide notions of (bi)simulations for XPath logics containing the child, parent, ancestor and descendant axes to navigate the tree. We show that these notions pre- cisely characterize the equivalence relation associated with each logic. We study formula complexity measures consisting of the number of nested axes and nested subformulas in a formula; these notions are akin to the notion of quantifier rank in first-order logic. We show characterization results for fine grained notions of equivalence and (bi)simulation that take into account these complexity measures. We also prove that positive fragments of these logics correspond to the formulas preserved under (non-symmetric) simulations. We show that the logic including the child axis is equivalent to the fragment of first-order logic invariant under the corresponding notion of bisimulation. If upward navigation is allowed the characterization fails but a weaker result can still be established. These results hold both over the class of possibly infinite data trees and over the class of finite data trees. Besides their intrinsic theoretical value, we argue that bisimulations are useful tools to prove (non)expressivity results for the logics studied here, and we substantiate this claim with examples.
BibTeX
@Article{Figueira2015,
author = "D. Figueira and S. Figueira and C. Areces",
journal = "Journal of Artificial Intelligence Research",
title = "Model Theory of {XPath} on Data Trees. Part {I:}
Bisimulation and Characterization",
year = "2015",
pages = "271--314",
volume = "53",
abstract = "We investigate model theoretic properties of XPath
with data (in)equality tests over the class of data
trees, i.e., the class of trees where each node
contains a label from a finite alphabet and a data
value from an infinite domain. We provide notions of
(bi)simulations for XPath logics containing the child,
parent, ancestor and descendant axes to navigate the
tree. We show that these notions pre- cisely
characterize the equivalence relation associated with
each logic. We study formula complexity measures
consisting of the number of nested axes and nested
subformulas in a formula; these notions are akin to the
notion of quantifier rank in first-order logic. We show
characterization results for fine grained notions of
equivalence and (bi)simulation that take into account
these complexity measures. We also prove that positive
fragments of these logics correspond to the formulas
preserved under (non-symmetric) simulations. We show
that the logic including the child axis is equivalent
to the fragment of first-order logic invariant under
the corresponding notion of bisimulation. If upward
navigation is allowed the characterization fails but a
weaker result can still be established. These results
hold both over the class of possibly infinite data
trees and over the class of finite data trees. Besides
their intrinsic theoretical value, we argue that
bisimulations are useful tools to prove
(non)expressivity results for the logics studied here,
and we substantiate this claim with examples.",
doi = "10.1613/jair.4658",
owner = "areces",
URL = "http://dx.doi.org/10.1613/jair.4658",
}