License: 
Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2012.326
URN: urn:nbn:de:0030-drops-34185
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3418/
Ganian, Robert ;
Hlineny, Petr ;
Langer, Alexander ;
Obdržálek, Jan ;
Rossmanith, Peter ;
Sikdar, Somnath
Lower Bounds on the Complexity of MSO_1 Model-Checking
Abstract
One of the most important algorithmic meta-theorems is a famous result
by Courcelle, which states that any graph problem definable in monadic second-order logic with edge-set quantifications (MSO2) is decidable in linear time on any class of graphs of bounded tree-width. In the parlance of parameterized complexity, this means that MSO2 model-checking is fixed-parameter tractable with respect to the tree-width as parameter. Recently, Kreutzer and Tazari proved a corresponding complexity lower-bound---that MSO2 model-checking is not even in XP wrt the formula size as parameter for graph classes that are subgraph-closed and whose tree-width is poly-logarithmically unbounded. Of course, this is not an unconditional result but holds modulo a certain complexity-theoretic assumption, namely, the Exponential Time Hypothesis (ETH).
In this paper we present a closely related result. We show that
even MSO1 model-checking with a fixed set of vertex labels,
but without edge-set quantifications, is not in XP wrt the formula
size as parameter for graph classes which are subgraph-closed and
whose tree-width is poly-logarithmically unbounded unless the non-uniform ETH fails. In comparison to Kreutzer and Tazari, (1) we use a stronger prerequisite, namely non-uniform 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 MSO1-definable properties on vertex labeled graphs instead of MSO2-definable 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
subdigraph-monotone measure can be algorithmically useful, unless it is within a poly-logarithmic factor of (undirected) tree-width.
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 Model-Checking}},
booktitle = {29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
pages = {326--337},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-35-4},
ISSN = {1868-8969},
year = {2012},
volume = {14},
editor = {Christoph D{\"u}rr and Thomas Wilke},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2012/3418},
URN = {urn:nbn:de:0030-drops-34185},
doi = {10.4230/LIPIcs.STACS.2012.326},
annote = {Keywords: Monadic Second-Order Logic, Treewidth, Lower Bounds, Exponential Time Hypothesis, Parameterized Complexity}
}
|
Keywords: |
|
Monadic Second-Order Logic, Treewidth, Lower Bounds, Exponential Time Hypothesis, Parameterized Complexity |
|
Collection: |
|
29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012) |
|
Issue Date: |
|
2012 |
|
Date of publication: |
|
24.02.2012 |
