The Community for Technology Leaders
Logic in Computer Science, Symposium on (2006)
Seattle, Washington
Aug. 12, 2006 to Aug. 15, 2006
ISSN: 1043-6871
ISBN: 0-7695-2631-4
pp: 7-16
Mikolaj Bojanczyk , Warsaw University
Thomas Schwentick , Dortmund University
Anca Muscholl , LIAFA, Paris VII
Claire David , LIAFA, Paris VII
Luc Segoufin , INRIA, Paris XI
ABSTRACT
In a data word each position carries a label from a finite alphabet and a data value from some infinite domain. These models have been already considered in the realm of semistructured data, timed automata and extended temporal logics. <p>It is shown that satisfiability for the two-variable first-order logic FO^2(~,\le,+1) is decidable over finite and over infinite data words, where ?? is a binary predicate testing the data value equality and +1,\le are the usual successor and order predicates. The complexity of the problem is at least as hard as Petri net reachability. Several extensions of the logic are considered, some remain decidable while some are undecidable.</p>
INDEX TERMS
null
CITATION
Mikolaj Bojanczyk, Thomas Schwentick, Anca Muscholl, Claire David, Luc Segoufin, "Two-Variable Logic on Words with Data", Logic in Computer Science, Symposium on, vol. 00, no. , pp. 7-16, 2006, doi:10.1109/LICS.2006.51
103 ms
(Ver )