Logic in Computer Science (LICS 2002)

Paper: The complexity of first-order and monadic second-order logic revisited (at LICS 2002)

Authors: Markus Frick Martin Grohe

Abstract

The model-checking problem for a logic L on a class C of structures asks whether a given L-sentence holds in a given structure in C. In this paper, we give super-exponential lower bounds for fixed-parameter tractable model-checking problems. We show that unless PTIME=NP, the model-checking problem for monadic second-order logic on finite words is not solvable in time f(k)p(n), for any elementary function f and any polynomial p. Here k denotes the size of the input sentence and n the size of the input word. We prove the same result for first-order logic under a stronger complexity theoretic assumption from parameterized complexity theory. Furthermore, we prove that the model-checking problem for first-order logic on structures of degree 2 is not solvable in time 2^{2^{o(k)}} p(n), for any polynomial p, again under an assumption from parameterized complexity theory. We match this lower bound by a corresponding upper bound.

BibTeX

  @InProceedings{FrickGrohe-Thecomplexityoffirs,
    author = 	 {Markus Frick and Martin Grohe},
    title = 	 {The complexity of first-order and monadic second-order logic
    revisited},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }