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

TL;DR

This paper introduces a new logical framework, CMSO/tw, that extends model checking capabilities to minor-closed graph classes by parameterizing quantification with annotated treewidth, leading to a quadratic-time algorithm.

Contribution

It develops an Algorithmic Meta-Theorem extending Courcelle's theorem to minor-closed classes with bounded annotated treewidth quantification.

Findings

Model checking for CMSO/tw formulas is quadratic-time for all non-trivial minor-closed classes.

The framework generalizes existing meta-theorems to broader graph classes.

It incorporates disjoint-path predicates in the logic, enhancing expressiveness.

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.