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 LTL↓1(F), that extends LTL(F) with one register for storing data values for later comparisons. We show that satisfiability over data words of LTL↓1(F) is already not primitive recur-sive. We also show that the extension of LTL↓1(F) with either the reverse modality F−1 or with one extra register is undecidable. All those lower bounds were already known for LTL↓1(X,F) 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.