Basic Model Theory of XPath on Data Trees

Figueira, D., Figueira, S., and Areces, C.. Basic Model Theory of XPath on Data Trees. In Proceedings of the 17th International Conference on Database Theory, Athens, Greece, March 2014.

Download: [pdf] 

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.

BibTeX: (download)

@INPROCEEDINGS{figu:basi14,
  author = {Figueira, D. and Figueira, S. and Areces, C.},
  title = {Basic Model Theory of XPath on Data Trees},
  booktitle = {Proceedings of the 17th International Conference on Database Theory},
  year = {2014},
  address = {Athens, Greece},
  month = {March},
  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}
}

Generated by bib2html.pl (written by Patrick Riley) on Sun Oct 02, 2016 17:05:49