[Zurück]

R. Ganian, P. Hlinený, A. Langer, J. Obdrzalek, P. Rossmanith, S. Sikdar:
"Lower Bounds on the Complexity of MSO1 Model-Checking";
Journal of Computer and System Sciences, 80 (2014), 1; S. 180 - 194.

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.

http://dx.doi.org/10.1016/j.jcss.2013.07.005

Projektleitung Stefan Szeider:
Exploiting New Types of Structure for Fixed Parameter Tractability

Projektleitung Stefan Szeider:
The Parameterized Complexity of Reasoning Problems