Abstracts for the LGTDS workshop

ICGT Conference , Barcelona, October 2002

The complexity of first-order and monadic second-order logic

Markus Frick

Laboratory for Foundations of Computer Science,
Edinburgh, UK


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 following:
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 MSO-model-checking.