Lower Bounds on the Complexity of MSO_1 Model-Checking

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

GANIAN Robert HLINĚNÝ Petr OBDRŽÁLEK Jan LANGER Alexander ROSSMANITH Peter SIKDAR Somnath

Year of publication 2014
Type Article in Periodical
Magazine / Source Journal of Computer and System Sciences
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1016/j.jcss.2013.07.005
Field Informatics
Keywords Monadic Second-Order Logic; Treewidth; Lower Bounds; Exponential Time Hypothesis; Parameterized Complexity
Description Kreutzer and Tazari proved in 2010 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 MSO1 model-checking with a fixed set of vertex labels---i.e., without edge-set quantification---is not solvable even in quasi-polynomial time for fixed MSO-formulas in such graph classes. 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. 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 greatly simplifies important lengthy parts of the former proof. Our result also has an interesting consequence in the realm of digraph width measures.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.