Lower bounds on the complexity of MSO₁ model-checking

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.