Future-looking logics on data words and trees

Abstract

In a data word or a data tree each position carries a label from a finite alphabet and a data value from an infinite domain. Over data words we consider the logic , that extends LTL ↓1 ( F) with one register for storing data values for later comparisons. We show that satisfiability over data words of LTF ↓1 (F)is already non primitive recursive. We also show that the extension of LTF ↓1 (F) with either the backward modality F -1 or with one extra register is undecidable. All these lower bounds were already known LTF ↓1 (X,F)for and our results essentially show that the X modality was not necessary. Moreover we show that over data trees similar lower bounds hold for certain fragments of Xpath. © 2009 Springer Berlin Heidelberg.