Parameterizing the quantification of CMSO: model checking on minor-closed graph classes

TL;DR

The work develops CMSO/tw, a parameterized fragment of counting MSO that restricts quantified vertex-sets to those with bounded annotated treewidth, and proves an algorithmic meta-theorem: model checking CMSO/tw+dp is tractable in quadratic time on any non-trivial minor-closed graph class, with a precise reduction to CMSO on bounded Hadwiger-number graphs. The core methodology combines annotated types, flat railed annuli, and a Local-Global-Irrelevancy framework to localize bounded-tw sets and lift locality to global graph structure, enabling a reduction from complex inputs to bounded-treewidth cores. The results unify and extend known AMTs for minor-exclusion, via a flexible reduction framework between LP-pairs, and provide constructive algorithms that can, given a formula and a graph class, output an efficient decision procedure. The significance lies in generalizing Courcelle-type tractability from input-treewidth constraints to formula-structure constraints, thereby broadening practical tractability for logical properties on a wide range of minor-closed graph classes.

Abstract

Given a graph $G$ and a vertex set $X$, the annotated treewidth tw$(G,X)$ of $X$ in $G$ is the maximum treewidth of an $X$-rooted minor of $G$, i.e., a minor $H$ where the model of each vertex of $H$ contains some vertex of $X$. That way, tw$(G,X)$ can be seen as a measure of the contribution of $X$ to the tree-decomposability of $G$. We introduce the logic CMSO/tw as the fragment of monadic second-order logic on graphs obtained by restricting set quantification to sets of bounded annotated treewidth. We prove the following Algorithmic Meta-Theorem (AMT): for every non-trivial minor-closed graph class, model checking for CMSO/tw formulas can be done in quadratic time. Our proof works for the more general CMSO/tw+dp logic, that is CMSO/tw enhanced by disjoint-path predicates. Our AMT can be seen as an extension of Courcelle's theorem to minor-closed graph classes where the bounded-treewidth condition in the input graph is replaced by the bounded-treewidth quantification in the formulas. Our results yield, as special cases, all known AMTs whose combinatorial restriction is non-trivial minor-closedness.

Figures (2)

• Figure 1: The Hasse diagram of the poset of some logics between $\mathsf{FO}$ and $\mathsf{CMSO}$ along with the corresponding known and recent results on AMTs whose combinatorial condition is minor-exclusion. An edge between two logics means that the formulas of the lower one are expressible by the formulas of the higher one.
• Figure 2: A graph $G$ and a $(6,5)$-railed annulus flatness pair $(\mathcal{A},\mathfrak{R})$ of $G$. The $(6,5)$-railed annulus $\mathcal{A}$ is depicted in deep blue, where we assume that the "outer" cycle in the figure is $C_1$ and the "inner" cycle is $C_6$. The vertices in $X_1\cap Y_1$ and $X_2\cap Y_2$ are the "outer" and the "inner" red squared vertices, respectively. The green vertices are the vertices in $X_1\setminus Y_1$ and the red vertices are the vertices in $Y_2\setminus X_2$. The grey and green disks are the cells of $\mathfrak{R}$ and $\mathsf{Influence}_\mathfrak{R}([C_2,C_3])$ is the set of all graphs drawn in the green cells.

Theorems & Definitions (37)

• Proposition 1
• Theorem 1
• Definition 1
• Theorem 2
• Theorem 3
• Lemma 1
• proof
• proof : Proof of \ref{['thm_reduce']}
• Lemma 2
• Lemma 3