Abstract
One of the most important algorithmic metatheorems is a famous result
by Courcelle, which states that any graph problem definable in monadic secondorder logic with edgeset quantifications (MSO2) is decidable in linear time on any class of graphs of bounded treewidth. In the parlance of parameterized complexity, this means that MSO2 modelchecking is fixedparameter tractable with respect to the treewidth as parameter. Recently, Kreutzer and Tazari proved a corresponding complexity lowerboundthat MSO2 modelchecking is not even in XP wrt the formula size as parameter for graph classes that are subgraphclosed and whose treewidth is polylogarithmically unbounded. Of course, this is not an unconditional result but holds modulo a certain complexitytheoretic assumption, namely, the Exponential Time Hypothesis (ETH).
In this paper we present a closely related result. We show that
even MSO1 modelchecking with a fixed set of vertex labels,
but without edgeset quantifications, is not in XP wrt the formula
size as parameter for graph classes which are subgraphclosed and
whose treewidth is polylogarithmically unbounded unless the nonuniform ETH fails. In comparison to Kreutzer and Tazari, (1) we use a stronger prerequisite, namely nonuniform instead of uniform ETH, to avoid the effectiveness assumption and the construction of certain obstructions used in their proofs; and (2) we assume a different set of problems to be efficiently decidable, namely MSO1definable properties on vertex labeled graphs instead of MSO2definable properties on unlabeled graphs.
Our result has an interesting consequence in the realm of digraph width measures: Strengthening a recent result, we show that no
subdigraphmonotone measure can be algorithmically useful, unless it is within a polylogarithmic factor of (undirected) treewidth.
BibTeX  Entry
@InProceedings{ganian_et_al:LIPIcs:2012:3418,
author = {Robert Ganian and Petr Hlineny and Alexander Langer and Jan Obdrž{\'a}lek and Peter Rossmanith and Somnath Sikdar},
title = {{Lower Bounds on the Complexity of MSO_1 ModelChecking}},
booktitle = {29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
pages = {326337},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897354},
ISSN = {18688969},
year = {2012},
volume = {14},
editor = {Christoph D{\"u}rr and Thomas Wilke},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2012/3418},
URN = {urn:nbn:de:0030drops34185},
doi = {http://dx.doi.org/10.4230/LIPIcs.STACS.2012.326},
annote = {Keywords: Monadic SecondOrder Logic, Treewidth, Lower Bounds, Exponential Time Hypothesis, Parameterized Complexity}
}
Keywords: 

Monadic SecondOrder Logic, Treewidth, Lower Bounds, Exponential Time Hypothesis, Parameterized Complexity 
Seminar: 

29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012) 
Issue Date: 

2012 
Date of publication: 

24.02.2012 