The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
We develop the basic model theory of XPath with data (in)equality tests over the class of data trees, i.e., the class of trees where each node contains a label from a finite alphabet and a data value from an infinite domain. We provide notions of bisimulations (both general and bounded) for XPath logics containing only 'child', or both 'child' and 'parent' navigational axes. We show that these notions precisely capture the logical equivalence relation associated with each fragment, and show two results where the tool of bisimulation plays a central role: characterization and definability. The former says that certain logic is the bisimulation-invariant fragment of first order; the latter gives necessary and sufficient conditions for a class of pointed data trees to be definable by a set of formulas or by a single formula.