Characterizations for XPath_R(\downarrow)

SERGIO ABRIOLA; NICOLÁS GONZÁLEZ

Congreso; Workshop on Logic, Language, Information and Computation; 2021

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