Model theory of XPath on data trees. Part II: Binary bisimulation and definability

Abstract

We study the expressive power of the downward and vertical fragments of XPath equipped with (in)equality tests over possibly infinite data trees. We introduce a suitable notion of saturation with respect to node expressions, and show that over saturated data trees, the already studied notion of (unary) bisimulation coincides with the idea of ‘indistinguishability by means of node expressions’. We also prove definability and separation theorems for classes of pointed data trees. 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 prove a characterization theorem, which describes when a first-order formula with two free variables is expressible in the downward fragment. We show definability and separation theorems, for classes of two-pointed data trees and in the context of path expressions.