Skip to main content

Research Repository

Advanced Search

On the Complexity of the Model Checking Problem

Madelaine, Florent R.; Martin, Barnaby D.

On the Complexity of the Model Checking Problem Thumbnail


Authors

Florent R. Madelaine



Abstract

The complexity of the model checking problem for various fragments of first-order logic (FO) has attracted much attention over the last two decades, in particular for the fragment induced by ∃ and ∧ and that induced by ∀, ∃, and ∧, which are better known as the constraint satisfaction problem and the quantified constraint satisfaction problem, respectively. The former was conjectured to follow a dichotomy between P and NP-complete by Feder and Vardi [SIAM J. Comput., 28 (1998), pp. 57–104]. For the latter, there are several partial trichotomy results between P, NP-complete, and Pspace-complete, and Chen [Meditations on quantified constraint satisfaction, in Logic and Program Semantics, Springer, Heidelberg, 2012, pp. 35–49] ventured a conjecture regarding Pspace-completeness vs. membership in NP in the presence of constants. We give a comprehensive account of the whole field of the complexity of model checking similar syntactic fragments of FO. The above two fragments are in fact the only ones for which there is currently no known complexity classification. Indeed, we consider all other similar syntactic fragments of FO, induced by the presence or absence of quantifiers and connectives, and fully classify the complexities of the parameterization of the model-checking problem by a finite model D, that is, the expression complexities for certain finite D. Perhaps surprisingly, we show that for most of these fragments, “tractability” is witnessed by a generic solving algorithm which uses quantifier relativization. Our classification methodology relies on tailoring suitably the algebraic approach pioneered by Jeavons, Cohen, and Gyssens [J. ACM, 44 (1997), pp. 527–548] for the constraint satisfaction problem and by B¨orner et al. [Inform. and Comput., 207 (2009), pp. 923–944] for the quantified constraint satisfaction problem. Most fragments under consideration can be relatively easily classified, either directly or using Schaefer’s dichotomy theorems for SAT and QSAT, with the notable exception of the positive equality-free fragment induced by ∃, ∀, ∧, and ∨. 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.

Citation

Madelaine, F. R., & Martin, B. D. (2018). On the Complexity of the Model Checking Problem. SIAM Journal on Computing, 47(3), 769-797. https://doi.org/10.1137/140965715

Journal Article Type Article
Acceptance Date Oct 27, 2017
Online Publication Date Jun 12, 2018
Publication Date Jun 12, 2018
Deposit Date Jul 13, 2018
Publicly Available Date Jul 13, 2018
Journal SIAM Journal on Computing
Print ISSN 0097-5397
Electronic ISSN 1095-7111
Publisher Society for Industrial and Applied Mathematics
Peer Reviewed Peer Reviewed
Volume 47
Issue 3
Pages 769-797
DOI https://doi.org/10.1137/140965715

Files

Published Journal Article (582 Kb)
PDF

Copyright Statement
© 2018, Society for Industrial and Applied Mathematics







You might also like



Downloadable Citations