Title:Deciding Graph MSO Properties: Has it all been told already?

Abstract:A famous result of Courcelle claims that on graphs of bounded tree-width <=t, all MSO2 properties \phi are decidable in FPT time O(f(\phi, t)\cdot|G|). The result, being in a wide sense "optimal", brings a question; what new can be said about this problem nowadays? However, see that the function f in time complexity of Courcelle's algorithm involves a tower of exponents of height growing with \phi (which is generally unavoidable by [Frick-Grohe]). Perhaps the first "MSO2 algorithmic metatheorem" with elementary dependence on the parameter \phi has been given only recently by [Lampis, ESA2010] for the graphs of bounded vertex cover. Some extensions for the MSO1 case are presented also in [Ganian, IPEC2011]. We take a general approach, proving that the MSO model-checking problem admits an FPT algorithm with an elementary dependence on the formula on all classes of trees of bounded height. This result, via standard logic interpretation, implies that all MSO2 properties \phi are decidable in FPT with an elementary dependence on \phi for the graphs of bounded tree-depth (a subclass of bounded tree-width). Analogously, all MSO1 properties admit a similar algorithm on certain subclasses of bounded clique-width graphs.