|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| 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
| ASCII Text | x | ||
| Diego Figueira, "A Decidable Two-Way Logic on Data Words," Logic in Computer Science, Symposium on, pp. 365-374, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, 2011. | |||
| BibTex | x | ||
| @article{ 10.1109/LICS.2011.18, author = {Diego Figueira}, title = {A Decidable Two-Way Logic on Data Words}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2011}, issn = {1043-6871}, pages = {365-374}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2011.18}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Logic in Computer Science, Symposium on TI - A Decidable Two-Way Logic on Data Words SN - 1043-6871 SP365 EP374 A1 - Diego Figueira, PY - 2011 KW - data word KW - XPath KW - satisfiability KW - two-way KW - reflexive-transitive VL - 0 JA - Logic in Computer Science, Symposium on ER - | |||
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2011.18
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.
