Titre: On reflexive-transitive navigation in the presence of data values
Abstract: When working on data words or data trees, it is often important to be able to compare data values from positions far apart. In modal or navigational languages, such as LTL or XPath, this is done using transitive closure modalities (such as Future, or Descendant). As it turns out, this type of modalities very easily makes the satisfiability problem either undecidable or with non-primitive recursive complexity. However, in many of these cases, replacing modalities with their reflexive-transitive counterpart (as opposed to only transitive) entails a series of monotonicity properties useful to gain decidability, even elementarity. The purpose of this talk is to give an idea of why adding reflexivity improves things.