Model Theory of XPath on Data Trees. Part II: Binary Bisimulation and Definability

SERGIO ABRIOLA; MARÍA EMILIA DESCOTTE; SANTIAGO FIGUEIRA

Information and Computation

ACADEMIC PRESS INC ELSEVIER SCIENCE

Lugar: Amsterdam; Año: 2017 p. 195 - 233

0890-5401

We study the expressive power of the downward and vertical fragments of XPath equipped with (in)equality tests over data trees. We show definability theorems (which provide conditions under which a class of pointed data trees can be defined by a node expression or by a set of node expressions) and separation theorems (which provide conditions under which two disjoint classes of pointed data trees can be separated by a class definable by a node expression or a set of node expressions). To do so, we introduce a notion of saturation, and show that over saturated data trees, the already known notion of (unary) bisimulation coincides with logical equivalence. Both for the downward and vertical fragments, we introduce new notions of binary bisimulations, which relate two ´pairs´ of nodes of data trees. We show that over finitely branching data trees, these notions correspond to the idea of `indistinguishability by means of path expressions´. We show a characterization theorem, which states that a first-order formula with two free variables is expressible in the downward fragment of XPath with (in)equality tests if and only if it is binary-bisimulation-invariant and represents a `forward property´. Using the new tool of binary bisimulations, together with suitable modifications of saturation, we show definability and separation theorems, this time with respect to classes of two-pointed data trees (with some restrictions) and in the context of path expressions as the language of description.