This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2011 IEEE 26th Annual Symposium on Logic in Computer Science
A Decidable Two-Way Logic on Data Words
Toronto, Ontario Canada
June 21-June 24
ISBN: 978-0-7695-4412-0
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.
Index Terms:
data word, XPath, satisfiability, two-way, reflexive-transitive
Citation:
Diego Figueira, "A Decidable Two-Way Logic on Data Words," lics, pp.365-374, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, 2011
Usage of this product signifies your acceptance of the Terms of Use.