On the complexity of the model checking problem

DOI10.1137/140965715MaRDI QIDQ3176188zbMATH OpenOpenAlexFDO

Authors Florent R. Madelaine, Barnaby Martin

Publication date 19 July 2018

Published in SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1210.6893, http://dro.dur.ac.uk/25546/1/25546.pdf

zbMATH Keywords

computational complexityGalois connectionlogic in computer sciencequantified constraintsuniversal algebra

Mathematics Subject Classification ID

Logic in computer science (03B70) Galois correspondences, closure operators (in relation to ordered sets) (06A15) Applications of universal algebra in computer science (08A70) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: The model checking problem for various fragments of first-order logic has attracted much attention over the last two decades: in particular, for the primitive positive and the positive Horn fragments, which are better known as the constraint satisfaction problem and the quantified constraint satisfaction problem, respectively. These two fragments are in fact the only ones for which there is currently no known complexity classification. All other syntactic fragments can be easily classified, either directly or using Schaefer's dichotomy theorems for SAT and QSAT, with the exception of the positive equality free fragment. This outstanding fragment can also be classified and enjoys a tetrachotomy: according to the model, the corresponding model checking problem is either tractable, NP-complete, co-NP-complete or Pspace-complete. Moreover, the complexity drop is always witnessed by a generic solving algorithm which uses quantifier relativisation. Furthermore, its complexity is characterised by algebraic means: the presence or absence of specific surjective hyper-operations among those that preserve the model characterise the complexity.

Recommendations

• First-Order Model Checking Problems Parameterized by the Model
• On the complexity of existential positive queries
• The complexity of problems for quantified constraints
• Decomposing quantified conjunctive (or disjunctive) formulas
• Decomposing Quantified Conjunctive (or Disjunctive) Formulas

Cites work

• A dichotomy theorem for constraint satisfaction problems on a 3-element set
• Classifying the Complexity of Constraints Using Finite Algebras
• Closure properties of constraints
• Complexity classifications of Boolean constraint satisfaction problems
• Conjunctive-query containment and constraint satisfaction
• Finite model theory and its applications.
• First-Order Model Checking Problems Parameterized by the Model
• scientific article; zbMATH DE number 53151 (Why is no real title available?)
• Log Space Recognition and Translation of Parenthesis Languages
• Logical Approaches to Computational Barriers
• Meditations on quantified constraint satisfaction
• On the complexity of H-coloring
• On the Computational Complexity of Monotone Constraint Satisfaction Problems
• Principles and Practice of Constraint Programming – CP 2004
• QCSP on partially reflexive forests
• The complexity of constraint satisfaction games and QCSP
• The complexity of positive first-order logic without equality
• The complexity of positive first-order logic without equality. II: The four-element case
• The Complexity of Quantified Constraint Satisfaction: Collapsibility, Sink Algebras, and the Three-Element Case
• The complexity of satisfiability problems
• The Computational Structure of Monotone Monadic SNP and Constraint Satisfaction: A Study through Datalog and Group Theory
• The CSP Dichotomy Holds for Digraphs with No Sources and No Sinks (A Positive Answer to a Conjecture of Bang-Jensen and Hell)

Cited in

(21)

• The complexity of model checking multi-stack systems
• Complexity of model checking for cardinality-based belief revision operators
• scientific article; zbMATH DE number 1688350 (Why is no real title available?)
• Intuitionistic implication makes model checking hard
• The complexity of positive first-order logic without equality
• Decomposing quantified conjunctive (or disjunctive) formulas
• First-Order Model Checking Problems Parameterized by the Model
• The complexity of model checking for Boolean formulas
• The complexity of positive first-order logic without equality. II: The four-element case
• Lower bounds on the complexity of \(\mathsf{MSO}_1\) model-checking
• The tractability frontier of graph-like first-order query sets
• The tractability frontier of graph-like first-order query sets
• scientific article; zbMATH DE number 2163033 (Why is no real title available?)
• scientific article; zbMATH DE number 1884382 (Why is no real title available?)
• On the complexity of model expansion
• Model Checking for String Problems
• The lattice and semigroup structure of multipermutations
• The Complexity of Model Checking Multi-stack Systems
• On the complexity of existential positive queries
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Mathematical Foundations of Computer Science 2005

This page was built for publication: On the complexity of the model checking problem

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