Future-Looking Logics on Data Words and Trees

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 non primitive recursive. We also show that the extension of LTL↓ 1(F) with either the backward modality F−1 or with one extra register is undecidable. All these 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.

• Type: Conference
• Year: 2009
• Where: MFCS
• Authors: Diego Figueira, Luc Segoufin
• Keywords: Data Trees, Data Values, Data Words, MFCS 2009, Theoretical Computer Science