The complexity of first-order and monadic second-order logic
Laboratory for Foundations of Computer Science,
In this talk we take look at the complexity of the model-checking problem.
The model-checking problem for a logic L on a class C of structures is the
Input: a formula F out of L and a structure A from C
Problem: does F hold in A?
We examine the complexity of these decision problems for first-order (FO)
and monadic second-order logic (MSO). We start presenting classical results
concerning their combined and parameterized complexity. Here we call an
instance of the model-checking problem fixed-parameter tractable, if it
can be solved in time f(||F||) p(||A||), for an arbitrary function f and
a polynomial p.
The main part of the presentation will be an examination of parameterized
lower bounds, i.e. we take a fixed-parameter tractable instance of the model-checking
problem and ask how "big" the dependency f on the size of the formula necessarily
is. We give lower bounds on f under standard complexity theoretic assumptions.
For example, model-checking for monadic second-order logic on words cannot
be done with an elementary bound on f, unless P = NP. In this spirit, we
give lower bounds for a different classes C of input structures.
We complement these results by improved upper bounds. Together, this gives
us a rather complete picture of the parameterized complexity of FO- and