Future-Looking Logics on Data Words and Trees

9 years 1 months ago
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.
Diego Figueira, Luc Segoufin
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where MFCS
Authors Diego Figueira, Luc Segoufin
Comments (0)