Sciweavers

Share
LICS
2006
IEEE

Two-Variable Logic on Words with Data

9 years 8 days ago
Two-Variable Logic on Words with Data
— 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. It is shown that satisfiability for the two-variable first-order logic FO2 (∼,<,+1) is decidable over finite and over infinite data words, where ∼ is a binary predicate testing the data value equality and +1,< 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.
Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentic
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where LICS
Authors Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin, Claire David
Comments (0)
books