Other formats:
BibTeX
LaTeX
RIS
@inproceedings{992001,
author = {Ganian, Robert and Hliněný, Petr and Obdržálek, Jan and Langer, Alexander and Rossmanith, Peter and Sikdar, Somnath},
address = {Dagstuhl, Germany},
booktitle = {29th International Symposium on Theoretical Aspects of Computer Science STACS2012},
doi = {http://dx.doi.org/10.4230/LIPIcs.STACS.2012.326},
edition = {2012},
keywords = {Monadic Second-Order Logic; Treewidth; Lower Bounds; Exponential Time Hypothesis; Parameterized Complexity},
howpublished = {elektronická verze "online"},
language = {eng},
location = {Dagstuhl, Germany},
isbn = {978-3-939897-35-4},
pages = {326-337},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, LIPICS},
title = {Lower Bounds on the Complexity of MSO_1 Model-Checking},
url = {http://stacs2012.lip6.fr/},
year = {2012}
}
TY - JOUR
ID - 992001
AU - Ganian, Robert - Hliněný, Petr - Obdržálek, Jan - Langer, Alexander - Rossmanith, Peter - Sikdar, Somnath
PY - 2012
TI - Lower Bounds on the Complexity of MSO_1 Model-Checking
PB - Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, LIPICS
CY - Dagstuhl, Germany
SN - 9783939897354
KW - Monadic Second-Order Logic
KW - Treewidth
KW - Lower Bounds
KW - Exponential Time Hypothesis
KW - Parameterized Complexity
UR - http://stacs2012.lip6.fr/
L2 - http://stacs2012.lip6.fr/
N2 - 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.
ER -
GANIAN, Robert, Petr HLINĚNÝ, Jan OBDRŽÁLEK, Alexander LANGER, Peter ROSSMANITH and Somnath SIKDAR. Lower Bounds on the Complexity of MSO\_{}1 Model-Checking. Online. In \textit{29th International Symposium on Theoretical Aspects of Computer Science STACS2012}. 2012th ed. Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, LIPICS, 2012, p.~326-337. ISBN~978-3-939897-35-4. Available from: https://dx.doi.org/10.4230/LIPIcs.STACS.2012.326.
|
