Two-variable logic with two order relations

DOI10.2168/LMCS-8(1:15)2012zbMATH Open1238.03031arXiv1110.1439MaRDI QIDQ5891508FDOQ5891508

Authors: Thomas Schwentick, Thomas Zeume 

Publication date: 3 April 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: It is shown that the finite satisfiability problem for two-variable logic over structures with one total preorder relation, its induced successor relation, one linear order relation and some further unary relations is EXPSPACE-complete. Actually, EXPSPACE-completeness already holds for structures that do not include the induced successor relation. As a special case, the EXPSPACE upper bound applies to two-variable logic over structures with two linear orders. A further consequence is that satisfiability of two-variable logic over data words with a linear order on positions and a linear order and successor relation on the data is decidable in EXPSPACE. As a complementing result, it is shown that over structures with two total preorder relations as well as over structures with one total preorder and two linear order relations, the finite satisfiability problem for two-variable logic is undecidable.

Full work available at URL: https://arxiv.org/abs/1110.1439

Recommendations

• Two-variable logic with two order relations (extended abstract)
• Two-variable logic on 2-dimensional structures
• Decidability issues for two-variable logics with several linear orders
• Two-variable logic with counting and a linear order
• Two variable first-order logic over ordered domains

zbMATH Keywords

linear orderstwo-variable logicdata word

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Complexity of computation (including implicit computational complexity) (03D15)

Cited In (16)

• Title not available (Why is that?)
• Synthesis of data word transducers
• Church synthesis on register automata over linearly ordered data domains
• Decidability issues for two-variable logics with several linear orders
• Two-Variable Separation Logic and Its Inner Circle
• Order-invariance of two-variable logic is decidable
• Synthesis of Data Word Transducers
• Reasoning on data words over numeric domains
• Two-variable logic with two order relations (extended abstract)
• Two-variable logic with a between relation
• Two-variable logic on 2-dimensional structures
• Pebble-intervals automata and \(\text{FO}^2\) with two orders
• Finite satisfiability for two‐variable, first‐order logic with one transitive relation is decidable
• Two-Variable Logic over Countable Linear Orderings
• Two-variable logic on data words
• Two variables and two successors

This page was built for publication: Two-variable logic with two order relations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5891508)