A Decidable Two-Way Logic on Data Words

摘要

We study the satisfiability problem for a logic on data words. A data word is a finite word where every position carries a label from a finite alphabet and a data value from an infinite domain. The logic we consider is two-way, contains future and past modalities, which are considered as reflexive and transitive relations, and data equality and inequality tests. This logic corresponds to the fragment of XPath with the 'following-sibling-or-self' and 'preceding-sibling-or-self' axes over data words. We show that this problem is decidable, EXPSPACE-complete. This is surprising considering that with the strict (non-reflexive) navigation relations the satisfiability problem is undecidable. To prove this, we first reduce the problem to a derivation problem for an infinite transition system, and then we show how to abstract this problem into a reachability problem of a finite transition system.