Ganian, R., Hliněný, P., Langer, A., Obdržálek, J., Rossmanith, P., & Sikdar, S. (2014). Lower bounds on the complexity of MSO₁ model-checking. Journal of Computer and System Sciences, 80(1), 180–194. https://doi.org/10.1016/j.jcss.2013.07.005
E192-03 - Forschungsbereich Knowledge Based Systems
-
Journal:
Journal of Computer and System Sciences
-
ISSN:
0022-0000
-
Date (published):
Feb-2014
-
Number of Pages:
15
-
Peer reviewed:
Yes
-
Keywords:
Applied Mathematics; Theoretical Computer Science; Computational Theory and Mathematics; Computer Networks and Communications
-
Abstract:
Recently, Kreutzer and Tazari proved a complexity lower-bound to the famous
MSO2 theorem of Courcelle-that MSO2 model-checking is not polynomial
(XP) wrt. the formula size as parameter for graph classes that are
subgraph-closed and whose tree-width is poly-logarithmically unbounded. We
prove that even MSO1 model-checking with a fixed set of vertex labels-i.e.,
without edge-set quantification-is not solvable in polynomial time (and even
not solvable in quasi-polynomial time) for fixed MSO1-formulas in such graph
classes. This also has an interesting consequence in the realm of digraph width
measures, strengthening upon recent results. Both the lower bounds hold modulo
a certain complexity-theoretic assumption, namely, the Exponential Time
Hypothesis (ETH) in the former case and the nonuniform ETH in the latter
case. Altogether, in comparison to Kreutzer and Tazari, we show a different
set of problems to be intractable, and our stronger complexity assumption of
nonuniform ETH slightly weakens assumptions on the graph class and simplifies
important lengthy parts of the former proof.
en
Project title:
The Parameterized Complexity of Reasoning Problems: 239962 (Europäischer Forschungsrat (ERC)) Exploiting New Types of Structure for Fixed Parameter Tractability: P 26696-N30 (Fonds zur Förderung der wissenschaftlichen Forschung (FWF))