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.

翻译：给定图$G$和顶点集$X$，$X$在$G$中的标注树宽tw$(G,X)$是指$G$的$X$-根子图（即每个$H$的顶点模型都包含$X$中某个顶点的子图$H$）的最大树宽。通过这种方式，tw$(G,X)$可视为$X$对$G$的树可分解性贡献的度量。我们引入CMSO/tw逻辑作为图上的单子二阶逻辑片段，其通过将集合量化限制在有限标注树宽的集合上获得。我们证明以下算法元定理（AMT）：对于每个非平凡闭子图类，CMSO/tw公式的模型检测可在平方时间内完成。我们的证明适用于更一般的CMSO/tw+dp逻辑，即通过不相交通路谓词增强的CMSO/tw。我们的AMT可视为库尔切勒定理在闭子图类上的扩展，其中输入图中的有限树宽条件被替换为公式中的有限树宽量化。我们的结果作为特例，涵盖了所有已知组合限制为非平凡闭子图性的算法元定理。