S.Kreutzer's lectures at the
Evaluating logical formulas in finite structures is one of the central problems in computational model theory, with many applications in computer science. For logics such as first-order or monadic second-order logic, if both the formula and the structure are part of the input, this problem is well known to be PSPACE complete and hence, presumably, not solvable in polynomial time.
Fall school (Sept.'11)
The Complexity of Evaluating Formulas in Relational Structures
On the other hand, going back to work by Buchi and others, it is known that any fixed formula of monadic second-order logic can be evaluated in linear time on finite trees. This has later been extended by Courcelle to the case of structures of bounded tree-width. Following these results a range of "algorithmic meta-theorems", i.e. results relating the complexity of evaluating a fixed formula to structural parameters of the input instances, have been obtained for logics such as monadic second-order logic and first-order logic.
The general aim of this research area is to find for each of the common logics structural parameters such that formulas of this logic can be evaluated efficiently precisely on input instances of this form.
Most results in this area establish upper bounds, i.e. are of the form that verifying whether a formula is true in an input structure is tractable whenever the input is of a certain form, e.g. is tree-like or a planar graph. Results establishing tighter corresponding lower bounds have only very recently been established.
In this talk we will give an overview of algorithmic meta-theorems established so far and introduce some of the techniques used in this area. We will focus in particular on the lower bounds proved only very recently.
Slides.