Two-variable logic and key constraints on data words
Matthias Niewerth, Thomas Schwentick · 2011
The paper introduces key constraints for data words and shows that it is decidable whether, for a given two-variable sentence φ that can refer to the successor relation on positions and a set Κ of key constraints, there is a data string w that satisfies φ and respects Κ. Here, the formula is allowed to refer to the successor relation but not to the linear order on the positions of the word. As a byproduct, a self-contained exposition of an algorithm that decides satisfiability of such formulas (without key constraints) in 2-nexptime is given.