Working Seminar on Formal Models, Discrete Structures, and Algorithms

Model Checking Lower Bounds for Simple Graphs

Michail Lampis (KTH, Sweden)

When: March 11, 2pm

Where: room G2.91b/G215


Courcelle's theorem states that MSO properties can be decided in linear time on bounded treewidth graphs, but the hidden constant is a tower of exponentials. Unfortunately, a well-known result by Frick and Grohe shows that deciding even FO logic on trees (a much more restricted problem) requires such a non-elementary parameter dependence.

In this talk we will extend the results of Frick and Grohe to even simpler classes of graphs. In particular, we will show that the non-elementary parameter dependence is still necessary even for uncolored paths, and then discuss some implications of this result. Furthermore, we will show a (d+1)-fold exponential lower bound for the parameter dependence of MSO model checking on colored trees of height d. This matches the recent (d+1)-fold exponential algorithm for this problem recently given by Gajarsky and Hlineny.