Model-checking positive equality free logic on a fixed structure (direttissima)

TL;DR

This paper presents a new, relation-based proof of the tetrachotomy classification for the complexity of model-checking positive equality-free logic on various structures, including infinite ones, simplifying previous algebraic approaches.

Contribution

It introduces a direct, relation-only proof of the tetrachotomy, applicable to infinite structures, and develops algorithms for NP and co-NP cases in these contexts.

Findings

Classification into four complexity classes for various structures.

New algorithms for NP and co-NP membership in infinite structures.

Applicability to equality, temporal, and random graph structures.

Abstract

We give a new, direct proof of the tetrachotomy classification for the model-checking problem of positive equality-free logic parameterised by the model. The four complexity classes are Logspace, NP-complete, co-NP-complete and Pspace-complete. The previous proof of this result relied on notions from universal algebra and core-like structures called U-X-cores. This new proof uses only relations, and works for infinite structures also in the distinction between Logspace and NP-hard under Turing reductions. For finite domains, the membership in NP and co-NP follows from a simple argument, which breaks down already over an infinite set with a binary relation. We develop some interesting new algorithms to solve NP and co-NP membership for a variety of infinite structures. We begin with those first-order definable in (Q;=), the so-called equality languages, then move to those first-order definable in (Q;<), the so-called temporal languages. However, it is first-order expansions of the Random Graph (V,E) that provide the most interesting examples. In all of these cases, the derived classification is a tetrachotomy between Logspace, NP-complete, co-NP-complete and Pspace-complete.