Two-Variable Logic with Two Order Relations

TL;DR

This paper investigates the computational complexity of the finite satisfiability problem for two-variable logic over structures with various order relations, establishing EXPSPACE-completeness in some cases and undecidability in others.

Contribution

It precisely characterizes the complexity of two-variable logic satisfiability over structures with different combinations of order relations, including new decidability and undecidability results.

Findings

EXPSPACE-completeness for structures with one total preorder, its successor, and one linear order.

Decidability in EXPSPACE for structures with two linear orders.

Undecidability for structures with two total preorders or mixed 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.