License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2013.484
URN: urn:nbn:de:0030-drops-42159
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4215/
Go to the corresponding LIPIcs Volume Portal

Manuel, Amaldev ; Zeume, Thomas

Two-Variable Logic on 2-Dimensional Structures

pdf-format:
35.pdf (0.6 MB)

Abstract

This paper continues the study of the two-variable fragment of first-order 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 <=_p-equivalence 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 two-dimensional structures.

BibTeX - Entry

@InProceedings{manuel_et_al:LIPIcs:2013:4215,
  author =	{Amaldev Manuel and Thomas Zeume},
  title =	{{Two-Variable Logic on 2-Dimensional Structures}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{484--499},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Simona Ronchi Della Rocca},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4215},
  URN =		{urn:nbn:de:0030-drops-42159},
  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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI