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.
