Lower Bounds for Monadic Second-Order Model-Checking
Stephan Kreutzer ( University of Oxford )
- 14:00 8th May 2009 ( week 2, Trinity Term 2009 )Lecture Theatre B
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.
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:
