@InCollection{Figueira2014,
  editor =       "N. Schweikardt and V. Christophides and V. Leroy",
  booktitle =    "Proc. 17th International Conference on Database Theory
                 (ICDT), Athens, Greece, March 24-28, 2014",
  pages =        "50--60",
  publisher =    "OpenProceedings.org",
  author =       "D. Figueira and S. Figueira and C. Areces",
  booktitle =    "Proceedings of the 17th International Conference on
                 Database Theory",
  title =        "Basic Model Theory of {XP}ath on Data Trees",
  year =         "2014",
  address =      "Athens, Greece",
  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,
                 descendant, parent and ancestor axes to navigate the
                 tree. We show that these notions precisely 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. The results in
                 this article 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.",
  owner =        "areces",
  timestamp =    "2013.11.28",
  ISBN =         "978-3-89318066-1", 
}