Characterizations for $$\text {XPath}^{}_{{\mathcal R}}(\downarrow ){}$$

Over the semantic universe of trees augmented with arbitrary sets of relations between nodes, we study model-theoretic properties of the extension \(\text {XPath}^{}_{{\mathcal R}}(\downarrow ){}\) of the downward fragment of XPath, equipped with a finite set \({\mathcal R}\) of relation symbols. We introduce an adequate notion of bisimulation, dependant on the set of relations \({\mathcal R}\) in consideration, and show a characterization result in the style of Hennessy-Milner’s, relating bisimulation and logical equivalence and showing that both coincide over finitely branching \({\mathcal R}\text {-trees}\). Furthermore, we also give a van Benthem-like theorem characterizing each \(\text {XPath}^{}_{{\mathcal R}}(\downarrow ){}\) as the fragment of first-order logic (over an adequate signature) with one free variable that is \({\mathcal R}\)-bisimulation-invariant. Finally, we show that our results are also valid when applied to universes of trees with some fixed semantics for the symbols of \({\mathcal R}\). This contains in particular the case of \(\text {XPath} _{=} (\downarrow )\) over data trees.