Skip to main content

Lower Bounds for Monadic Second-Order Model-Checking

Stephan Kreutzer ( University of Oxford )
In 1990, Courcelle proved a fundamental theorem stating that every property of graphs definable in monadic second-order logic can be decided in linear time on any class of graphs of bounded tree-width. This theorem is the first of what is today known as algorithmic meta-theorems, that is, results of the form: every property definable in a logic L can be decided efficiently on any class of structures or graphs with property P.

Such theorems are of interest both from a logical point of view, as results explaining the complexity of model-checking for various logics such as first-order or monadic second-order logic, and from an algorithmic point of view, where, e.g., Courcelle's theorem allows to verify very quickly that a problem can be solved efficiently on graphs of small tree-width.

Following Courcelle's theorem, much work has gone into establishing meta-theorems for first- and monadic second-order logic on a range of graph classes. Somewhat surprisingly, the question whether Courcelle's theorem is actually tight or can be extended to classes of unbounded tree-width has so far not received much attention.

In this talk I will give a brief, general introduction to algorithmic meta-theorems and recall Courcelle's theorem and the relevant concepts such as tree-width and monadic second-order logic. I will then present first results obtained in proving tightness of the result.

Share this: