@article{Geneves06d,
  author = {Pierre Genevès and Nabil Layaïda},
  title = {Deciding {XPath} Containment with {MSO}},
  journal = {Data and Knowledge Engineering (DKE)},
  volume = 63,
  number = 1,
  month = oct,
  year = 2007,
  pages = {108-136},
  url = {http://hal.archives-ouvertes.fr/hal-00189134},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  abstract = {XPath is the standard language for addressing parts of an XML
    document. We present a sound and complete decision procedure for
    containment of XPath queries. The considered XPath fragment covers most
    of the language features used in practice. Specifically, we show how XPath
    queries can be translated into equivalent formulas in monadic second-order
    logic. Using this translation, we construct an optimized logical
    formulation of the containment problem, which is decided using tree
    automata. When the containment relation does not hold between two XPath
    expressions, a counter-example XML tree is generated. We provide practical
    experiments that illustrate the efficiency of the decision procedure for
    realistic scenarios.}
}