Abstract
This paper continues the study of the twovariable fragment of firstorder logic (FO^2) over two dimensional structures, more precisely structures with two orders, their induced successor relations and arbitrarily many unary relations. Our main focus is on ordered data words which are finite sequences from the set \Sigma x D where \Sigma is a finite alphabet and D is an ordered domain. These are naturally represented as labelled finite sets with a linear order <=_l and a total preorder <=_p.
We introduce ordered data automata, an automaton model for ordered data words. An ordered data automaton is a composition of a finite state transducer and a finite state automaton over the product Boolean algebra of finite and cofinite subsets of N. We show that ordered data automata are equivalent to the closure of FO^2(+1_l,<=_p,+1_p) under existential quantification of unary relations. Using this automaton model we prove that the finite satisfiability problem for this logic is decidable on structures where the <=_pequivalence classes are of bounded size. As a corollary, we obtain that finite satisfiability of FO^2 is decidable (and it is equivalent to the reachability problem of vector addition systems) on structures with two linear order successors and a linear order corresponding to one of the successors. Further we prove undecidability of FO^2 on several other twodimensional structures.
BibTeX  Entry
@InProceedings{manuel_et_al:LIPIcs:2013:4215,
author = {Amaldev Manuel and Thomas Zeume},
title = {{TwoVariable Logic on 2Dimensional Structures}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {484499},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897606},
ISSN = {18688969},
year = {2013},
volume = {23},
editor = {Simona Ronchi Della Rocca},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4215},
URN = {urn:nbn:de:0030drops42159},
doi = {10.4230/LIPIcs.CSL.2013.484},
annote = {Keywords: FO2, Data words, Satisfiability, Decidability, Automata}
}
Keywords: 

FO2, Data words, Satisfiability, Decidability, Automata 
Collection: 

Computer Science Logic 2013 (CSL 2013) 
Issue Date: 

2013 
Date of publication: 

02.09.2013 