Two-Variable Logic on 2-Dimensional Structures

Authors Amaldev Manuel, Thomas Zeume



PDF
Thumbnail PDF

File

LIPIcs.CSL.2013.484.pdf
  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Amaldev Manuel
Thomas Zeume

Cite As Get BibTex

Amaldev Manuel and Thomas Zeume. Two-Variable Logic on 2-Dimensional Structures. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 484-499, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013) https://doi.org/10.4230/LIPIcs.CSL.2013.484

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.

Subject Classification

Keywords
  • FO2
  • Data words
  • Satisfiability
  • Decidability
  • Automata

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail