Two-Variable Logic with Two Order Relations

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.

Cited by in corpus (8)

• The Finite Satisfiability Problem for Two-Variable, First-Order Logic with one Transitive Relation is Decidable
• Synthesis of Data Word Transducers
• Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants
• Order-Invariance of Two-Variable Logic is Decidable
• A Short Note on Two-Variable Logic with a Linear Order Successor and a Preorder Successor
• Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
• Pebble-Intervals Automata and FO2 with Two Orders (Extended Version)
• Finite Model Reasoning in Expressive Fragments of First-Order Logic