Campus Event Calendar
Event Entry
What and Who
Model Checking Lower Bounds for Simple Graphs
Michael Lampis
KTH Stockholm
AG1 Mittagsseminar (own work)
AG 1, AG 2, AG 3, AG 4, AG 5, RG1, SWS, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 18 June 2013
13:00
30 Minutes
E1 4
024
Saarbrücken
Abstract
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.
Contact
Matthias Mnich
--email hidden
passcode not visible
logged in users only
Matthias Mnich, 05/05/2013 12:38
Matthias Mnich, 05/05/2013 12:37 -- Created document.
Matthias Mnich, 05/05/2013 12:37 -- Created document.