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

Ignasi Sau, Giannos Stamoulis, Dimitrios M. Thilikos

► To cite this version:

Ignasi Sau, Giannos Stamoulis, Dimitrios M. Thilikos. Parameterizing the quantification of CMSO: model checking on minor-closed graph classes. SODA 2025 - 36th Annual ACM-SIAM Symposium on Discrete Algorithms, Jan 2025, New Orleans, United States. pp.403-445, 10.1137/1.9781611978322.12 . lirmm-04918933

HAL Id: lirmm-04918933

https://hal-lirmm.ccsd.cnrs.fr/lirmm-04918933v1

Submitted on 29 Jan 2025

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Parameterizing the quantification of CMSO: model checking on minor-closed
graph classes*

Ignasi Sau†

Giannos Stamoulis‡

Dimitrios M. Thilikos†

Abstract

Given a graph $G$ and a vertex set $X$, the *annotated treewidth* $\text{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, $\text{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.

# 1 Introduction

A very active line of research lying in the territory between Logic and Algorithms deals with the derivation of *Algorithmic Meta-Theorems*, or AMTs for short. According to Grohe and Kreutzer [41], AMTs state that certain families of algorithmic problems, typically defined by some *logical condition*, are “tractable” when the input graphs satisfy some specific property, typically defined by some *combinatorial condition*. When the logical condition is expressibility in a logic $L$ and the structural condition is membership in some graph class $C$, the notion of “tractability” is most commonly considered as the following: if $\varphi$ is a formula in $L$ and $G$ is a graph in $C$, then deciding whether $G \models \varphi$ (this is known as the *MODEL CHECKING* problem for $L$) can be done in time $f(|\varphi|, C) \cdot |G|^c$, for some function $f$ and some constant $c \in \mathbb{N}$ which does not depend neither on $C$ nor on $\varphi$.

Clearly, there are two natural orthogonal directions to boost the power of an AMT: consider logics $L$ that are as general as possible or/and consider graph classes $C$ that are as general as possible. There is an abundance of such results concerning different compromises between the logical and combinatorial conditions [40, 41, 48]. Among them, a considerable amount of research deals with the definition of logics where AMTs can be derived under the combinatorial condition that $C$ is some non-trivial *minor-closed*<fnref n="1" /> graph class [5, 28, 30, 74, 75]. The pursuit of such AMTs aimed at the definition of several logics able to express, in the most general manner, the rich algorithmic potential of the Graph Minors series of Robertson and Seymour.

In this paper we introduce a fragment of counting monadic second-order logic that is able to subsume all<fnref n="2" /> known AMTs on minor-closed graph classes to a single meta-algorithmic statement. The key idea in our logic is to introduce parameterization in the quantification of CMSO formulas, as discussed in Subsection 1.1.

<footnote>*The full version of the paper can be accessed at https://arxiv.org/abs/2406.18465. All authors were supported by the French-German Collaboration ANR/DFG Project UTMA (ANR-20-CE92-0027). The first author was also supported by ANR project ELIT (ANR-20-CE48-0008). The second author was also supported by the project BOBR that is funded from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme with grant agreement No. 948057. The third author was also supported by the Franco-Norwegian project PHC AURORA 2024 (Projet n° 51260WL).</footnote>

<footnote>†LIRMM, Univ Montpellier, CNRS, Montpellier, France.</footnote>

<footnote>‡University of Warsaw, Poland. Part of the research work for this paper was conducted when G.S. was affiliated with LIRMM, Univ Montpellier, CNRS, Montpellier, France.</footnote>

<footnote n="1">¹A graph class $C$ is *minor-closed* if it contains all minors of its graphs (for the definition of the minor relation, see Subsection 2.2). $C$ is *non-trivial* if it does not contain all graphs. According to Robertson and Seymour's theorem [68], if $C$ is non-trivial and minor-closed then it excludes some big enough clique as a minor.</footnote>

<footnote n="2">²This assertion excludes variants based on cardinality constraints (see e.g. [46]).</footnote>
**Courcelle's theorem: limitations and extensions.** The archetypical example of an AMT is Courcelle's theorem [13–15] (see also [2,9]), asserting that graph properties definable in CMSO (counting monadic second-order logic) are decidable in linear time on graphs of bounded treewidth (for the formal definition of CMSO, see Subsection 2.1). Due to the *grid-exclusion theorem* [66] (and its algorithmic version – see e.g. [11]), this AMT can be rewritten, using minor-exclusion, as follows.

**PROPOSITION 1.1.** *There exist a function $f: \mathbb{N}^2 \to \mathbb{N}$ and an algorithm that, given a planar graph $H$, a formula $\varphi \in \text{CMSO}$, and an $H$-minor-free graph $G$, decides whether $G \models \varphi$ in time $f(|\varphi|, |H|) \cdot |G|$.*

Interestingly, the planarity condition for the excluded minor $H$ in Proposition 1.1 is unavoidable if one wishes to stick to the full expressibility potential of CMSO (see [49]). Therefore, the emerging challenge is the following:

(1.1) *Identify fragments of CMSO that permit the proof of AMTs that are similar to Proposition 1.1 without the planarity condition for the excluded minor $H$.*

The first result in this direction dates back to [28], where Flum and Grohe showed that a “planarity-free” version of Proposition 1.1 holds if we consider first-order logic (FO) instead of the more expressive CMSO. Here we should stress that the meta-algorithmics of FO offers a rich line of research that nowadays has achieved to prove AMTs under combinatorial conditions that are much more general than minor-closedness (see [8, 18, 21–24, 42, 59–62, 76]). While the meta-algorithmics of FO are pretty well studied (see [7, 19, 24]), the challenge in (1.1) has established an independent line of research that resulted in the introduction of intermediate logics that enjoy some of the expressibility characteristics of CMSO and permit tractable model checking on the more general realm of minor-closed graph classes.

The first result in this direction consisted in enhancing FO with extra predicates expressing the existence of a path avoiding some fixed number of vertices. This extension was introduced independently by Schirrmacher, Siebertz, and Vigny in [75] (under the name FO+conn) and by Bojańczyk in [5] (under the name separator logic). The second and more expressive extension of FO, also introduced by Schirrmacher, Siebertz, and Vigny in [75], is FO+dp, which enhances FO with predicates expressing the existence of disjoint paths between certain pairs of vertices. Note that using such predicates one can express properties that are not expressible in FO, like connectivity or planarity [75]. For FO+conn, a tractable model checking algorithm in graphs excluding a (topological) minor has been given by Pilipczuk, Schirrmacher, Siebertz, Toruńczyk, and Vigny [65]. For the more expressive FO+dp, a tractable model checking algorithm in graphs excluding a minor has been given by Golovach, Stamoulis, and Thilikos in [38] (this result has recently been extended for graphs excluding a topological minor in [74]). Note that, in both aforementioned logics, expressibility of FO is boosted by allowing some particular and restricted set quantification “hidden” in the introduced predicates. However, these logics do not allow further queries on the “hidden” quantified sets, and therefore they can be viewed more as enhancements of FO rather than restrictions of CMSO. As an attempt to go further than this, another enhancement of FO was recently introduced by Fomin, Golovach, Sau, Stamoulis, and Thilikos [29], the so-called *compound logic* $\tilde{\Theta}$, which combines FO and CMSO and is essentially a language that was tailored so as to express general families of graph modification problems. In [29], the authors provide an AMT on minor-excluding graph classes for the enhancement of the compound logic with disjoint-paths predicates, denoted by $\tilde{\Theta}^{dp}$.

**1.1 Our contribution** In this paper we deviate from the above approaches that deal with enhancements of FO. In the logic that we introduce, rather than allowing only particular combinations of quantified sets, we now allow arbitrary quantification on sets by restricting the *structure* of each quantified set. Namely, we demand them to have bounded *annotated treewidth*, a parameter introduced in [78], which is defined as follows: given a graph $G$ and a set $X \subseteq V(G)$, the *annotated treewidth* of $X$ in $G$, denoted by $\text{tw}(G, X)$, 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, $\text{tw}(G, X)$ can be seen as a measure of the contribution of $X$ to the tree-decomposability of $G$, in the sense that it corresponds to the largest treewidth of all minors of $G$ in which the set $X$ is “spread” across the vertex models. For instance, if $\Gamma_n$ is a the $(n \times n)$-grid and $X$ are the vertices of its “perimeter”, then $\text{tw}(\Gamma_n, X) = 2$, while if $X$ contains all the vertices of some “diagonal” of $\Gamma_n$ or of the “middle vertical” path of $\Gamma_n$, then $\text{tw}(\Gamma_n, X) = \Omega(n^{1/2})$. For edge sets, annotated treewidth is defined as follows: given a graph $G$ and a set $E \subseteq E(G)$, the *annotated treewidth* of $E$ in $G$, denoted by $\text{tw}(G, E)$, is equal to $\text{tw}(G', X_E)$, where $G'$ is the graph obtained from $G$ after subdividing each edge of $G$ once and $X_E$ is the set of subdivision vertices in $G'$ corresponding to the edges in $E$. For more on annotated treewidth and its related concepts, see Subsection 2.2.
More formally, we denote by CMSO/tw the restriction of CMSO where instead of using the quantifier $∃X$ (resp. $∀X$) for a set variable $X$, we introduce the quantifier $∃_k X$ (resp. $∀_k X$) for some $k \in \mathbb{N}$, where $∃_k X$ and $∀_k X$ mean that the quantification is applied on sets $X \in 2^{V(G)} \cup 2^{E(G)}$ where $\mathrm{tw}(G, X) \le k$. In particular, we define

$$ (1.2) \qquad \exists_k X \varphi := \exists X (\mathrm{tw}(G, X) \le k \wedge \varphi) \quad \text{and} \quad \forall_k X \varphi := \neg (\exists_k X \neg \varphi). $$

(Note that $\forall_k X \varphi = \forall X (\mathrm{tw}(G, X) \le k \rightarrow \varphi)$.)

The main conceptual novelty of our approach is to parameterize the quantification allowed in the considered CMSO formulas and consider the parameter of annotated treewidth as the measure of this parametrization. To the best of our knowledge, this is the first time that such a “parameterized fragment” of CMSO is considered. Let us mention here existing work on extensions of MSO by generalized quantifiers for MSO [1, 10, 47] originating in the corresponding work for FO [52, 58] (see [79] and [25, Chapter 12] for surveys – for second order Category and Measure quantifiers, see [3, 4, 54, 55]).

Concerning the choice of the parameter tw in the above definition, we should stress that among all possible minor-monotone<fnref n="3" /> parameters, treewidth is the best possible choice. Indeed, as we argue in Section 3, by considering the annotated variant of any minor-monotone parameter p that is not functionally larger<fnref n="4" /> than treewidth, we get that on planar graphs the logic CMSO/p has the same expressive power as the general CMSO.

It is important to agree that, when evaluating the length $|\varphi|$ of a formula $\varphi \in \mathrm{CMSO/tw}$, the length of the numerical representation of $k$ is also taken into account. Note also that, for every fixed $k$, the property that $\mathrm{tw}(G, X) \le k$ is MSO-expressible, and therefore CMSO/tw can indeed be seen as a fragment of CMSO. Our results indicate that the quantification defined in (1.2) is the key ingredient for a general answer to question (1.1).

We denote by CMSO/tw+dp the logic obtained from CMSO/tw by allowing also disjoint-paths predicates, as it was already done in [38, 75] for the case of FO. Note that the application of this enhancement on CMSO does not add any expressibility power, as disjoint-paths predicates are already expressible in CMSO. However, when enhancing CMSO/tw by allowing the use of the disjoint-paths predicate, we permit quantification on vertex sets of unbounded annotated treewidth, in the form of the demanded disjoint paths in the predicate. Our result, in its most general form, is the following.

**THEOREM 1.1.** There exist a computable function $f: \mathbb{N}^2 \rightarrow \mathbb{N}$ and an algorithm that, given a graph $H$, a formula $\varphi \in \mathrm{CMSO/tw+dp}$, and an $H$-minor-free graph $G$, decides whether $G \models \varphi$ in time $f(|\varphi|, |H|) \cdot |G|^2$.

Note that Theorem 1.1 can be rephrased as the property that model checking for CMSO/tw+dp is tractable on non-trivial minor-closed graph classes, and subsumes all known meta-algorithmic results on the tractability of logics on non-trivial minor-closed graph classes, such as those in [28–30, 38]. This is schematized in the Hasse diagram of Figure 1. On the other hand, recall that Courcelle’s theorem, stated in Proposition 1.1, asserts that CMSO model checking is tractable on graphs of bounded treewidth, and note that, when restricted to this class of graphs, the logics CMSO and CMSO/tw (as well as CMSO/tw+dp) have the same expressive power, since on bounded-treewidth graphs every set of vertices/edges trivially has bounded annotated treewidth. Therefore, Theorem 1.1 can be interpreted as a far-reaching generalization of Courcelle’s theorem (by using it as a black-box) under a new paradigm in which the bounded-treewidth restriction is not anymore applied to the input graph, but is instead applied, in its annotated form, to the quantification of the considered fragment of CMSO. Our logic allows to lift the tractability from bounded-treewidth graphs to non-trivial minor-closed graph classes, and with the additional “bonus” of the dp-extension of the CMSO/tw logic. See Section 3 for the discussion about extending Theorem 1.1 to more general graph classes.

We should stress that the proof of Theorem 1.1 is arguably simpler, both from the conceptual and the technical point of view, than those of the AMTs in [29, 30, 38].

**1.2 Our techniques** Theorem 1.1 capitalizes on the main algorithmic potential of the Graph Minors series of Robertson and Seymour. Namely, it exploits the “locality” of sets of bounded annotated treewidth and follows the scheme of the irrelevant-vertex technique of [67]. This approach is part of a greater framework that we introduce, concerning reductions between meta-theorems, where the task of finding irrelevant vertices for a problem

<footnote n="3">³A graph parameter is minor-monotone if its value on a graph is never smaller than its value on its minors.</footnote>

<footnote n="4">⁴We say that a parameter p is functionally larger than a parameter p' if there is a function $f: \mathbb{N} \rightarrow \mathbb{N}$ such that for every graph G, $p'(G) \le f(p(G))$.</footnote>
<figure><img src="image_2.png" /><figcaption>Figure 1: The Hasse diagram of the poset of some logics between FO and 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.</figcaption></figure>

is “localized” in a way that makes it (meta-)algorithmically tractable. In what follows, we provide a brief exposition of the principal ideas of our proofs.

**Simplifying instances.** Our approach to model checking is based on the irrelevant-vertex technique, which was introduced by Robertson and Seymour for the design of an algorithm solving the DISJOINT PATHS problem [67]. The core idea of this technique, from its original setting [67] to a striking majority of its subsequent applications in algorithm design for minor-free graphs, is that a candidate solution for the problem can be “rerouted away” from some sufficiently internal part of a grid, typically emerging from a structure called *flat wall*. This allows the characterization of the “avoidable” vertices as *irrelevant*, in the sense that their removal does not change the yes/no status of the instance. The repeated removal of such vertices results in an instance of bounded treewidth that is equivalent to the original instance. In the reduced instance, bounded treewidth can be used algorithmically, typically via explicit dynamic programming or using the meta-result of Proposition 1.1, in order to solve the problem. Let us here mention that the flat-wall structure, where the irrelevant-vertex arguments are applied, is given by the *Flat Wall Theorem* [12, 35, 44, 45, 67, 72] which has also been used in a meta-algorithmic setting in [29, 38].

However, the above approach does not readily work for model checking. The reason is the following and is based on the (un)decidability of the satisfiability problem (i.e., whether, for a given formula $\varphi$, there is some graph satisfying $\varphi$) for FO: Consider a formula $\varphi$ of FO and suppose that for every given graph of unbounded treewidth we can remove irrelevant vertices for the satisfaction of $\varphi$. This way, we would get a bounded-treewidth graph that is equivalent, in terms of satisfaction of $\varphi$, to the original graph. Then, the fact that the satisfiability problem for FO is decidable on graphs of bounded treewidth (see e.g. [16, Theorem 1.26]), would imply that it is also decidable on general (unbounded treewidth) graphs. However, satisfiability for FO on general graphs is undecidable; see e.g. [51, Section 9.1]. Such an obstacle can be avoided by “shifting” from the initial problem with input $(G, \varphi)$ to an alternative problem in which the input graph $G$ comes together with an annotation $R_1, \dots, R_h \subseteq V(G)$ of its vertex set, for some $h \in \mathbb{N}$ depending on $\varphi$, and structures of the form $(G, R_1, \dots, R_h)$, called *annotated graphs*. Such annotated graphs are asked to satisfy some new formula $\hat{\varphi}$, obtained from $\varphi$ by restricting the quantified variables to be picked from the corresponding $R_i$. Initially, each $R_i$ is set to be equal to $V(G)$ and $(G, R_1, \dots, R_h)$ satisfies $\hat{\varphi}$ if and only if $G$ satisfies $\varphi$, and our goal is to obtain some “simplified” instance $(G', R'_1, \dots, R'_h)$ that is equivalent to $(G, R_1, \dots, R_h)$ with respect to the satisfaction of $\hat{\varphi}$. This idea, originating in [36], plays a key role in the proof of the AMTs in [29, 30, 38, 74] and is also used in this work.
**Annotated types of annotated graphs.** In this paper, the formulas for which we find irrelevant vertices are the ones expressing the *annotated type* of an annotated graph. Given an $h \in \mathbb{N}$, the annotated *h*-type of an annotated graph ($G, R_1, \dots, R_h$) can be seen as a “tree-like” encoding of all sentences of $h$ (first-order and monadic second-order) variables in prenex normal form<fnref n="5" /> that $G$ satisfies, where the *i*-th quantified variable is asked to be interpreted in $R_i$. This corresponds to the annotated variant of *h*-rank FO/MSO-types given, for instance, by Shelah [77], Ebbinghaus and Flum [25, Definition 2.2.5], and Libkin [51, Section 3.4]; see also [8, 31, 32, 38, 39, 74]. Our notation builds on the one used in [37, 38, 74], since this facilitates the exposition of our proofs.

Since annotated *h*-types fully determine which formulas of *h* quantified variables are satisfied by an annotated graph ($G, R_1, \dots, R_h$), the MODEL CHECKING problem for any formula $\varphi$ on a input graph $G$ is translated to the computation of the (annotated) *h*-type of the graph $G$ annotated with *h* copies of its vertex set. To compute the annotated *h*-type, rather than computing the atomic type of every *h*-tuple of sets/vertices, we opt for the design of a procedure that *detects and removes* sets $S_0, \dots, S_h$ of vertices that are “irrelevant”, in the sense that they can be safely discarded from the sets $V(G), R_1, \dots, R_h$, respectively, so as to obtain an annotated (sub)graph ($G', R'_1, \dots, R'_h$) that has the *same annotated type* as ($G, R_1, \dots, R_h$). By repeating this process, we obtain an equivalent annotated instance (of the same annotated type as the original instance) which has small treewidth and, using Courcelle’s theorem, we can finally compute its annotated type (which indeed is MSO-expressible). For the irrelevant-vertex arguments, it is important to note that the number of different possible annotated types, over all annotated graphs ($G, R_1, \dots, R_h$), depends only on *h* and the number of different (up to logical equivalence) atomic types on *h* variables. A preliminary version of the above scheme (restricted to FO+dp formulas) appears in [37, 38].

**Reductions between AMTs.** In our setting, irrelevant vertices for the annotated type are obtained via a “local-global” argument. We detect an area of the graph where “*locally*” irrelevant vertices for the $R_i$’s, for some appropriate “local variant” of the annotated type, are also “*globally*” irrelevant for the (global) annotated type. In other words, we describe a way to localize the task of finding irrelevant vertices in a two-fold manner: “*locally*” irrelevant vertices are also “*globally*” irrelevant, and such vertices can be found *locally* using black-box application of some meta-algorithmic result.

We make the above idea more abstract by introducing a notion of *reductions between meta-theorems*. In the viewpoint we adopt, graph classes can be expressed as families of graphs where some (structural) parameter is bounded. Therefore, AMTs are stated for *Logic/Parameter pairs*, also called *LP-pairs*, of the form ($L, p$), where $L$ is a logic and $p$ is a graph parameter, mapping graphs to non-negative integers. In its simplest form, reductions between AMTs are defined as follows. We say that ($L_1, p_1$) is *reduced to* ($L_2, p_2$) if the following conditions hold:

(Definability Condition) For every $h \in \mathbb{N}$, annotated $h$-types for $L_1$ can be defined in $L_2$,

(Local-Global-Irrelevancy Condition) There is an effectively computable set $\Psi_h$ of $L_2$-sentences, for every $h \in \mathbb{N}$, and an algorithm $\mathcal{A}$ that given an $h \in \mathbb{N}$, a graph $G$, and an $h$-tuple $(R_1, \dots, R_h)$ of subsets of $V(G)$, if $p_2(G)$ is “large” as a function of $h$ and $p_1(G)$, then $\mathcal{A}$ outputs, in time $f(h, p_1(G)) \cdot |G|^c$ for some constant $c \in \mathbb{N}$ that does *not* depend on $h$ and $p_1(G)$, a set $Y \subseteq V(G)$ such that

(a) $p_2(G[Y])$ is “small”, i.e., upper-bounded by a function of $h$ and $p_1(G)$,

(b) irrelevant sets for $\Psi_h$ in $(G[Y], R_1 \cap Y, \dots, R_h \cap Y)$, are also irrelevant for the annotated $h$-type of $(G, R_1, \dots, R_h)$,

(c) there exist non-empty irrelevant sets for $\Psi_h$ in $(G[Y], R_1 \cap Y, \dots, R_h \cap Y)$.

If in the running time of $\mathcal{A}$, the dependency on $|G|$ is linear, then we say that ($L_1, p_1$) is *linear-time reduced to* ($L_2, p_2$). Reductions are defined formally and in a more general setting in Subsection 2.3 (see Definition 2.1). We prove that if ($L_1, p_1$) can be reduced to ($L_2, p_2$) and the *evaluation* of $L_2$-expressible formulas is tractable on graphs of bounded $p_2$, then $L_1$ model checking is tractable on graphs of bounded $p_1$; see Theorem 2.1. In this case, the model checking algorithm for $L_1$ has two stages. First, it consists of an iterative application of algorithm $\mathcal{A}$ of

<footnote n="5">⁵For the current section, we assume that all considered formulas are in prenex normal form, i.e., they are “split” into a prefix part that contains only quantifiers and a suffix part that is quantifier-free. The quantifier-free part can be seen as a boolean combination of atomic formulas, for some appropriate definition of atomic formulas depending on the logic we consider. For the corresponding definitions for CMSO/tw+dp, see Subsection 2.2.</footnote>
the Local-Global-Irrelevancy Condition, in order to detect and remove locally irrelevant vertices which we know that are also globally irrelevant. This is done “locally” using the evaluation meta-algorithm for (L₂, p₂). The final outcome, after repeated applications of that procedure, is an annotated graph (G', R'₁, ..., R'ₕ) with the same annotated h-type as G (annotated with h copies of V(G)) where p₂(G') is “small”, i.e, upper-bounded by some function of p₁(G) and h. Therefore, using again the evaluation meta-algorithm for (L₂, p₂), we can compute the annotated h-type of (G', R'₁, ..., R'ₕ) and therefore conclude whether the initial graph G satisfies a given formula φ of h quantifiers.

Let us mention here that reductions between AMTs already exist in the literature in the form of transductions; see e.g. [2, Theorem 4.3] and [41, Section 5]. In our case, reductions focus on iteratively translating “local parts” of the input (and the “candidate” annotated type) in order to gradually simplify the original instance, rather than using syntactic interpretations to completely shift the MODEL CHECKING problem into another class of inputs (which is typically the case in the setting of syntactic interpretations; see e.g. the recent powerful results of [6, 22, 33, 34, 41]).

To prove that an LP-pair (L₁, p₁) is reduced to an LP-pair (L₂, p₂), one has to come up with some appropriate set of formulas Φh and provide a suitable algorithm A that, when combined, yield the Local-Global-Irrelevancy Condition. In such an enterprise, the most demanding task is to prove that “locally” irrelevant vertices are also “globally” irrelevant. For this, one has to develop a “composition” argument on how the global annotated type can be split into two partial parts, one of them corresponding to some part of the graph with “small p₂” (which can be detected by A) and explain how computing this partial part of the annotated type can give us information about the global annotated type. These ideas date back to the work of Feferman and Vaugh [26]. For the setting where annotated types are “glued” in a common set of unbounded size, previous work was done in [29, 30, 37, 38].

After defining the above reduction framework between AMTs, our goal is to prove that

$$ (1.3) \qquad (\text{CMSO/tw} + \text{dp}, \text{hw}) \text{ is linear-time reduced to } (\text{CMSO}, \text{tw}), $$

where hw(G) is the Hadwiger number of G, i.e., the minimum k such that G does not contain Kₖ as a minor, while tw(G) is the treewidth of G. This, combined with Theorem 2.1 and the evaluation variant of Courcelle's theorem [17, Theorem 2.10] (see also, [2] and [27, Corollary 4.15]) implies tractable model checking for CMSO/tw+dp on classes of bounded Hadwiger number (Theorem 1.1). Using the framework of reductions, one can also prove that if L ∈ {FO, FO+dp, CMSO/tw, CMSO/tw+dp} and p ∈ {eg, hw} (here eg corresponds to Euler genus), then (L, p) is linear-time reduced to (CMSO, tw) (for (L, p) = (FO+dp, hw), the proof is in [37, 38]). However, the statement of (1.3) subsumes all these statements. Note that, using the same framework, one can show that if L ∈ {FO+sdp, CMSO/tw+sdp}, then (L, eg) is linear-time reduced to (CMSO, tw)<fnref n="6" />.

**Novelties of our approach.** As discussed earlier, the notion of reduction between AMTs that we introduce is a new concept that stems from the approach of [29, 38] and evolves it in a more abstract and general way, aiming to establish it as a base for the study and the proof of other AMTs. To the best of our knowledge, it is the first time that the irrelevant-vertex technique is abstracted as a *method* for the derivation of AMTs in such a general setting.

The crucial property of having bounded annotated treewidth is not only allowing us to obtain a fragment of CMSO for which model checking can be tractable on unbounded-treewidth inputs (without contradicting general complexity assumptions; see [41, Section 9]), but also permits to see sets of bounded annotated treewidth as “local” sets inside a grid-like structure. In fact, sets of bounded annotated treewidth are *local* inside *flat railed annuli*: systems of concentric cycles in a graph together with a collection of disjoint paths orthogonally traversing them, in such a way that there are no long “jumps” in the graph that can connect distant cycles or paths (see Figure 2).

The locality of sets of bounded annotated treewidth allow us to lift locality arguments for FO and, in particular, argue that for every tuple of sets of bounded annotated treewidth inside a flat railed annulus, we can find a “strip” of the railed annulus that is disjoint of these sets and crops out some part of them. This property lies in the very base of our arguments toward showing the Local-Global-Irrelevancy Condition in our reduction.

In fact, this property is essential to prove both items (b) and (c) of the Local-Global-Irrelevancy Condition. Let us particularly stress that, in order to prove (c), one has to show that there is a way to “locally” reduce the Rᵢ's while not changing the (partial) annotated type of the (partial) annotated graph. For Rᵢ's that correspond to first-order quantification, one may simply locally restrict Rᵢ only to “representative” vertices that represent the

<footnote n="6">⁶FO+dsp and CMSO/tw+sdp are the extensions of FO and CMSO/tw with *scattered disjoint-paths predicates*, as defined in [37, 38].</footnote>
<figure><img src="image_3.png" /><figcaption>Figure 2: A graph *G* and a flat railed annulus of *G*.</figcaption></figure>

satisfaction of all different annotated types of one level less and discard duplicates, eventually leading to a “small”
number of representative vertices for each R<sub>i</sub>. This was the approach of [37,38]. In the case of MSO-quantification,
this approach fails because the (union of) these representative sets have unbounded size and therefore we should
not hope to bound the total number of sets in a locally representative R'<sub>i</sub>. To deal with this, we use the fact that
the union of representative sets has bounded annotated treewidth. In a large flat railed annulus, we can find a
strip disjoint from these sets. We use this observation to iteratively “zoom” inside such a strip to prove that we
can restrict each R<sub>i</sub> after in an area that is disjoint from the already restricted R<sub>1</sub>,..., R<sub>i-1</sub>.

Another cornerstone of our approach is that the quantifier ∃<sub>k</sub> X (as well as ∀<sub>k</sub> X) can be expressed in FO+dp,
via the excluded-minor characterization of bounded annotated treewidth. Such a translation of the bounded
annotated treewidth demand for a set X into a query on the satisfiability of certain disjoint-paths queries between
terminals in X, allows to focus our study on “just” (more complicated) queries on disjoint paths between terminals
that are picked in certain (quantified) sets. Shifting to disjoint paths, we can use existing tools to achieve the
*Local-Global-Irrelevancy Condition* in the presence of disjoint-paths predicates, as the ones developed in [37, 38].
In our work, when it comes to dealing with the disjoint-paths predicates, we further develop the technical lemmas
of [37, 38]. The framework of flat railed annuli that we use, which serves as the main combinatorial base of the
*Local-Global-Irrelevancy Condition*, evolves the one of [29, 37, 38] and originates from the combinatorial tools
studied in [72].

**2 Main definitions and formal statement of the results**

This section is dedicated to the presentation of the main definitions of this paper, including the formal definition
of the logic CMSO/tw+dp and of the reductions between AMTs, as well as the formal statement of our results.
In this paper, we consider only *finite relational vocabularies* consisting of relation and constant symbols (we do not use function symbols). Every relation symbol *R* is associated with a positive integer, its *arity*. A *structure* $\mathfrak{A}$ of vocabulary $\sigma$, in short a $\sigma$-structure, consists of a non-empty finite set $V(\mathfrak{A})$, called the *universe* of $\mathfrak{A}$, an *r-ary* relation $R^\mathfrak{A} \subseteq V(\mathfrak{A})^r$ for each relation symbol $R \in \sigma$ of arity $r \ge 1$, and an element $c^\mathfrak{A} \in V(\mathfrak{A})$ for each constant symbol $c \in \sigma$. We refer to $R^\mathfrak{A}$ (resp. $c^\mathfrak{A}$) as the *interpretation of the symbol* $R$ (resp. $c$) *in the structure* $\mathfrak{A}$. When there is no ambiguity, we will not distinguish between relation symbols and their interpretations. We use $|\mathfrak{A}|$ to denote $|V(\mathfrak{A})|$. An undirected graph without loops can be seen as an $\{E\}$-structure $\mathfrak{G} = (V(\mathfrak{G}), E^\mathfrak{G})$, where $E^\mathfrak{G}$ is a binary relation that is symmetric and anti-reflexive. A *colored-graph vocabulary* contains a binary relation symbol *E* that is always interpreted as a symmetric and anti-reflexive binary relation (corresponding to edges) and a collection of unary relation symbols $Y_1, \dots, Y_h$ (corresponding to colors on the vertices). For a structure $\mathfrak{G}$ of vocabulary $\sigma$, its *Gaifman graph*, denoted by $\text{Gaifman}(\mathfrak{G})$, is the graph whose vertex set is $V(\mathfrak{G})$ and two vertices are adjacent if they both appear in a tuple of the same relation. For colored-graph vocabularies, this is $(V(\mathfrak{G}), E^\mathfrak{G})$.

**Some conventions on notation.** Given two integers $p, q$ such that $p \le q$, we set $[p, q] := \{p, \dots, q\}$ and, if $p \ge 1$, $[p] := [1, p]$. Given a set $A$, we use $2^A$ to denote the set of all of its subsets and $A^c$ to denote the product $A \times \dots \times A$ of $c$ copies of $A$.

**2.1 Basic definitions from logic** We now define the syntax and the semantics of first-order logic and monadic second-order logic of a vocabulary $\sigma$. We refer the reader to [16, 25, 51] for a broader discussion on logical structures, first-order logic, and monadic second-order logic, from the viewpoint of graphs. We assume the existence of a countable infinite set of *first-order variables*, usually denoted by lowercase symbols $x_1, x_2, \dots$, and of a countable infinite set of *set variables*, usually denoted by uppercase symbols $X_1, X_2, \dots$. A *first-order term* is either a first-order variable or a constant symbol.

A *first-order logic formula*, in short *FO-formula*, of vocabulary $\sigma$ is built from atomic formulas of the form $x = y$ and $(x_1, \dots, x_r) \in R$, where $R \in \sigma$ and has arity $r \ge 1$, on first-order terms $x, y, x_1, \dots, x_r$, by using the logical connectives $\vee$, $\neg$ and the quantifier $\exists$ on first-order variables.

A *monadic second-order logic formula*, in short *MSO-formula*, of vocabulary $\sigma$ is obtained by enhancing the syntax of FO-formulas by allowing atomic formulas of the form $x \in X$, for some first-order term $x$ and some set variable $X$, and allowing quantification both on first-order and set variables$^7$.

We use $\forall x\varphi$ and $\forall X\varphi$ as an abbreviation for $\neg(\exists x (\neg\varphi))$ and $\neg(\exists X (\neg\varphi))$, respectively. A *counting monadic second-order logic formula*, in short *CMSO-formula*, of vocabulary $\sigma$ is obtained by enhancing the syntax of MSO-formulas by allowing predicates of the form $\text{card}_p(X)$, expressing that $|X|$ is a multiple of an integer $p > 1$, for a fixed integer $p > 1$.

Given a logic$^8$ $\mathfrak{L}$, we denote by $\mathfrak{L}[\sigma]$ the set of all $\mathfrak{L}$-formulas of vocabulary $\sigma$. Given a formula $\varphi$ of some logic $\mathfrak{L}$, the *free variables* of $\varphi$ are its variables that are not in the scope of any quantifier. We write $\varphi(x_1, \dots, x_k, X_1, \dots, X_\ell)$ to indicate that the free variables of the formula $\varphi$ are among $x_1, \dots, x_k, X_1, \dots, X_\ell$. A *sentence* is a formula without free variables. Let $\mathfrak{L}$ be a logic and $\sigma$ be a vocabulary. Given a $\sigma$-structure $\mathfrak{A}$, a formula $\varphi(x_1, \dots, x_k, X_1, \dots, X_\ell) \in \mathfrak{L}[\sigma]$, $a_1, \dots, a_k \in V(\mathfrak{A})$, and $A_1, \dots, A_\ell \subseteq V(\mathfrak{A})$, we write $\mathfrak{A} \models \varphi (a_1, \dots, a_k, A_1, \dots, A_\ell)$ to denote that $\varphi(x_1, \dots, x_k, X_1, \dots, X_\ell)$ holds in $\mathfrak{A}$ if, for every $i \in [k]$, the variable $x_i$ is interpreted as $a_i$ and, for every $j \in [\ell]$, the variable $X_j$ is interpreted as $A_j$. If $\varphi$ is a sentence, then we write $\mathfrak{A} \models \varphi$ to denote that $\mathfrak{A}$ satisfies $\varphi$. For every considered set of formulas $\Phi$, we assume that we have fixed an encoding $\gamma : \Phi \to \{0, 1\}^*$, and we set the *length of $\varphi$*, denoted by $|\varphi|$, to be the length of $\gamma(\varphi)$. Note that this encoding takes into account the maximum value of $p$ and $k$, where $\text{card}_p(X)$ and $\exists_k X$ are used in $\varphi$.

**2.2 Definition of CMSO/tw** Let us first formally define the notion of treewidth and of a tree decomposition. A *tree decomposition* of a graph *G* is a pair $(T, \chi)$ where *T* is a tree and $\chi: V(T) \to 2^{V(G)}$ such that

<footnote>$^7$We clarify that MSO is commonly referred in the literature as MSO$_1$. For the vocabulary of graphs, MSO$_2$ is defined by also allowing quantification over edges and edge sets. Every MSO$_2$-formula on $G$ can be turned into an MSO$_1$-formula on the incidence graph $I(G)$ of $G$, defined as $(V(G) \cup E(G), \{\{v, e\} | v \in e\})$. In this paper, for the vocabulary of graphs, we use MSO to denote MSO$_2$. Note that $\text{hw}(G) = \text{hw}(I(G))$ and for a vertex/edge set $X$ in $G$, $\text{tw}(G, X) = \text{tw}(I(G), X)$.</footnote>

<footnote>$^8$We use the term *logic* to refer to a syntactic language closed under boolean combinations and element quantification.</footnote>
1. $\bigcup_{t \in V(T)} \chi(t) = V(G),$

2. for every edge $e$ of $G$ there is a $t \in V(T)$ such that $\chi(t)$ contains both endpoints of $e$, and

3. for every $v \in V(G)$, the subgraph of $T$ induced by $\{t \in V(T) | v \in \chi(t)\}$ is connected.

The width of $(T, \chi)$ is defined as $\max \{|\chi(t)| - 1 | t \in V(T)\}$. The treewidth of $G$, denoted by $\mathrm{tw}(G)$, is defined as the minimum width among all tree decompositions of $G$.

**Annotated treewidth.** We refer the reader to [78], where annotated treewidth was first defined. Let $G$ be a graph and $X \subseteq V(G)$. We say that a graph $H$ is an $X$-rooted minor of $G$ (or, simply, an $X$-minor of $G$) if there is a collection $S = \{S_v | v \in V(H)\}$ of pairwise disjoint subsets of $V(G)$, each inducing a connected subgraph of $G$ and containing at least one vertex of $X$, and such that, for every edge $xy \in E(H)$, the set $S_x \cup S_y$ is connected in $G$. A graph $H$ is a minor of $G$ if it is a $V(G)$-rooted minor of $G$. Given a graph $G$ and a set $X \subseteq V(G)$, we define $\mathrm{tw}(G, X)$ as the maximum treewidth of an $X$-minor of $G$. Note that $\mathrm{tw}(G, V(G)) = \mathrm{tw}(G)$ and that $\mathrm{tw}(G, X) \le \mathrm{tw}(G)$, for every $X \subseteq V(G)$. See [78, Subsection 1.5] for a comparison with other types of annotated extensions of treewidth.

The origins of annotated treewidth can be found in [20], where a similar notion was used for the proof of the main result (see [20, Lemma 3.1]). A similar measure of the portion of a flat wall that a set of vertices may intersect has been used in [69–71] for an extension of the results of [20] (see [71, Lemma 13]). This notion was also used in [29, 56, 57] where this measure is referred to as the bidimensionality of a set $X$ relatively to a flat wall.

As suggested in [78], it is possible to define the annotated extension of every minor-monotone parameter $p$, where $p(G, X)$ is equal to the maximum value of $p$ among all $X$-rooted minors of $G$. This notion was introduced as a measure of the essential contribution of the set $X$ in the value of the parameter $p$ and is commented in more detail in Section 3. For recent results on the structural properties of annotated treewidth, see [63, 64].

**Syntax and semantics of CMSO/tw.** The terms, (atomic) formulas, and free variables of CMSO/tw are defined as the ones of CMSO with the only exception that instead of using the quantifier $\exists X$, where $X$ is a set variable, we use the quantifier $\exists_k X$ (semantically defined below) for some $k \in \mathbb{N}$. Also, we use $\forall_k X \varphi$ as an abbreviation of $\neg(\exists_k X \neg\varphi)$. The semantics of CMSO/tw are as the ones of CMSO, where for a given vocabulary $\sigma$, and $\varphi \in \mathrm{CMSO/tw}[\sigma]$, a $\sigma$-structure $\mathfrak{G}$ satisfies $\exists_k X \varphi$, denoted by $\mathfrak{G} \models \exists_k X \varphi$, if and only if there is a vertex/edge subset $S$ of $\mathfrak{G}$ such that $\mathrm{tw}(\mathrm{Gaifman}(\mathfrak{G}), S) \le k$ and $\mathfrak{G}$ satisfies $\varphi$ when $X$ is interpreted as $S$.

**The logic CMSO/tw + dp.** For every positive integer $k$, we define the $2k$-ary disjoint-paths predicate $\mathrm{dp}_k(x_1, y_1, \dots, x_k, y_k)$, where $x_1, y_1, \dots, x_k, y_k$ are first-order terms. We use $\mathrm{dp}$ instead of $\mathrm{dp}_k$ when $k$ is clear from the context. A formula of CMSO/tw+dp is obtained by enhancing the syntax of CMSO/tw by allowing atomic formulas of the form $\mathrm{dp}_k(x_1, y_1, \dots, x_k, y_k)$ on first-order terms $x_1, y_1, \dots, x_k, y_k$, for $k \ge 1$. The satisfaction relation between a $\sigma$-structure $\mathfrak{G}$ and formulas $\varphi$ of CMSO/tw+dp[$\sigma$] is as for CMSO/tw, where $\mathrm{dp}_k(x_1, y_1, \dots, x_k, y_k)$ evaluates true in $\mathfrak{G}$ if and only if there are paths $P_1, \dots, P_k$ of $\mathrm{Gaifman}(\mathfrak{G})$ between (the interpretations of) $x_i$ and $y_i$ for all $i \in [k]$ such that for every distinct $i, j \in [k]$, $V(P_i) \cap V(P_j) = \emptyset$. It is easy to see that $\mathrm{dp}_k$ is $\mathrm{MSO}_1$-expressible. Also, note that $\mathrm{tw}(G, X)$ is $\mathrm{MSO}_1$-expressible via the obstruction characterization of treewidth and hence CMSO/tw+dp is “contained” in CMSO. Let us also stress that the problem of deciding whether a given formula in CMSO has an equivalent formula in CMSO/tw+dp is undecidable.

**2.3 A framework for the derivation of AMTs** Given a vocabulary $\sigma$ and a set $\Phi$ of formulas of vocabulary $\sigma$, we say that two $\sigma$-structures $\mathfrak{G}_1$ and $\mathfrak{G}_2$ are $\Phi$-equivalent, and we denote it by $\mathfrak{G}_1 \equiv_{\Phi} \mathfrak{G}_2$, if for every $\varphi \in \Phi$, $\mathfrak{G}_1 \models \varphi \iff \mathfrak{G}_2 \models \varphi$.

Let $\sigma$ be a vocabulary, let $R_1, \dots, R_h$ be a collection of $h$ unary relation symbols not contained in $\sigma$, for some $h \in \mathbb{N}$. Also, let $\Phi$ be a set of formulas of vocabulary $\sigma \cup \{R_1, \dots, R_h\}$. Given a $\sigma$-structure $\mathfrak{G}$ and sets $R_1, \dots, R_h \subseteq V(\mathfrak{G})$, we say that a tuple $(S_0, \dots, S_h)$ where $S_0, \dots, S_h \subseteq V(\mathfrak{G})$ is $\Phi$-irrelevant in $(\mathfrak{G}, R_1, \dots, R_h)$ if for every $i \in [h]$, $S_0 \subseteq S_i$ and

$$ (\mathfrak{G} \setminus S_0, R_1 \setminus S_1, \dots, R_h \setminus S_h) \equiv_{\Phi} (\mathfrak{G}, R_1, \dots, R_h). $$

Note that, given a $\Phi \subseteq L[\sigma]$ such that $\mathrm{FO} \subseteq L$, $\Phi$-irrelevancy is $L[\sigma]$-expressible.
**Reductions between meta-theorems.** A logic-parameter pair, in short an LP-pair, is a pair $M = (L, p)$, where $L$ is a logic and $p$ is a graph parameter, mapping graphs to non-negative integers.

**DEFINITION 2.1.** Given a positive integer $c$, and two LP-pairs $M_1 = (L_1, p_1)$ and $M_2 = (L_2, p_2)$, where for every graph $G$, $p_2(G) = O(|G|)$, we say that $M_1$ is $n^c$-reducible to $M_2$, denoted by $M_1 \leq_n^c M_2$, if the following conditions are satisfied:

(Definability Condition) For every $d \in \mathbb{N}$ and every formula $\varphi \in L_1[\{E\}]$ of length $d$, there is an $h_d \in \mathbb{N}$, a set $\Phi_d \subseteq L_2[\{E\}]$, and a formula $\delta_\varphi \in L_2[\{E, R_1, \dots, R_{h_d}\}]$ such that for every two graphs $G, G'$ and every $h_d$-tuple $\bar{R}$ of subsets of $V(G')$,

$$ \text{if } (G, V(G)^{h_d}) \equiv_{\Phi_d} (G', \bar{R}), \text{ then } G \models \varphi \iff (G', \bar{R}) \models \delta_\varphi. $$

Moreover, $h_d, \Psi_d$, and $\delta_\varphi$ are effectively computable from $d$ and $\varphi$.

(Local-Global-Irrelevancy Condition) There exist a vocabulary $\sigma_{d,l}$ and a finite set $\Psi_{d,l} \subseteq L_2[\sigma_{d,l} \cup \{R_1, \dots, R_{h_d}\}]$, both effectively computable for given $d,l \in \mathbb{N}$, and there is a function $f: \mathbb{N}^2 \to \mathbb{N}$ and an algorithm $A$ that, given a $d \in \mathbb{N}$, a graph $G$, where $l := p_1(G)$, and an $h_d$-tuple $\bar{R}$ of subsets of $V(G)$, either reports that $p_2(G) \leq f(d,l)$, or outputs a set $Y \subseteq V(G)$, a $\sigma_{d,l}$-structure $\mathfrak{B}$, where $Y \subseteq V(\mathfrak{B})$, an $h_d$-tuple $\bar{R}^{\mathfrak{B}}$ of subsets of $V(\mathfrak{B})$, and a set $Z \subseteq Y$ such that

(a) $|\mathfrak{B}| = O(|Y|)$ and $p_2(\text{Gaifman}(\mathfrak{B})) \leq f(d,l)$,

(b) for every vertex subsets $S_0, \dots, S_{h_d} \subseteq Z$ it holds that

if $(S_0, \dots, S_{h_d})$ is $\Psi_{d,l}$-irrelevant in $(\mathfrak{B}, \bar{R}^{\mathfrak{B}})$,
then $(S_0, \dots, S_{h_d})$ is $\Phi_d$-irrelevant in $(G, \bar{R})$.

(c) there exist vertex subsets $S_0, \dots, S_{h_d} \subseteq Z$, with $S_0 \neq \emptyset$, such that $(S_0, \dots, S_{h_d})$ is $\Psi_{d,l}$-irrelevant in $(\mathfrak{B}, \bar{R}^{\mathfrak{B}})$.

Moreover, algorithm $A$ runs in time $O_{d,l}(|G|^c)$.

**Decision and evaluation AMTs.** Let $L$ be a logic and $\sigma$ be a vocabulary. The MODEL CHECKING problem for $L$ asks, given as input a $\sigma$-structure $\mathfrak{G}$ and a $\varphi \in L[\sigma]$, whether $\mathfrak{G} \models \varphi$. The EVALUATION problem for $L$ asks, given as input a $\sigma$-structure $\mathfrak{G}$ and a $\varphi(\bar{X}) \in L[\sigma]$, for a tuple $\bar{S}$ such that $\mathfrak{G} \models \varphi(\bar{S})$, or a report that no such a tuple exists. Given an integer $c \geq 1$, we say that an LP-pair $(L, p)$ is an $n^c$-FPT-decision (resp. evaluation) Algorithmic Meta-Theorem, in short, an $n^c$-FPT-decision AMT (resp. an $n^c$-FPT-evaluation AMT), if there is a computable function $f: \mathbb{N}^2 \to \mathbb{N}$ and an algorithm solving the MODEL CHECKING (resp. EVALUATION) problem for $L$ in time $f(|\varphi|, p(\text{Gaifman}(\mathfrak{G}))) \cdot |\mathfrak{G}|^c$, where $(\varphi, \mathfrak{G})$ is the input instance.

**Our results.** We prove the following two results. Given $p \in \mathbb{N}$, we set $\mathbb{N}_{\geq p} := \mathbb{N} \setminus [0, p-1]$.

**THEOREM 2.1.** If $c, c' \in \mathbb{N}_{\geq 1}$ and $(L_1, p_1)$ and $(L_2, p_2)$ are LP-pairs, where $(L_1, p_1) \leq_{n^{c'}} (L_2, p_2)$ and $(L_2, p_2)$ is an $n^c$-FPT-evaluation AMT, then $(L_1, p_1)$ is an $n^{\max\{c, c'\}+1}$-FPT-decision AMT.

**THEOREM 2.2.** $(\text{CMSO}/\text{tw}+\text{dp}, \text{hw}) \leq_{n^1} (\text{CMSO}, \text{tw})$.

Since $(\text{CMSO}, \text{tw})$ is an $n$-FPT-evaluation AMT [17, Theorem 2.10] (see also [2] and [27]), Theorems 2.1 and 2.2, imply that $(\text{CMSO}/\text{tw}+\text{dp}, \text{hw})$ is an $n^2$-FPT-decision AMT (Theorem 1.1).

The next subsection contains the proof of Theorem 2.1. For the proof of Theorem 2.2, we refer the reader to the full version of the paper [73].

**2.4 Proof of Theorem 2.1** In this subsection, we prove Theorem 2.1. The proof of Theorem 2.1 is split into two parts. First, assuming that we are given an annotated graph $(G, \bar{R})$, where $p_2(G)$ is “large”, we show how to use the Local-Global-Irrelevancy Condition in order to obtain an annotated graph $(G', \bar{R}')$ such that $p_2(G')$ is “small” and $(G, \bar{R}) \equiv_{\Phi_d} (G', \bar{R}')$.
**LEMMA 2.1.** Let $c, c' \in \mathbb{N}_{\ge 1}$ and let $(\mathbf{L}_1, \mathbf{p}_1)$ and $(\mathbf{L}_2, \mathbf{p}_2)$ be two LP-pairs, where $(\mathbf{L}_1, \mathbf{p}_1) \le_{n^{c'}} (\mathbf{L}_2, \mathbf{p}_2)$ and $(\mathbf{L}_2, \mathbf{p}_2)$ is an $n^c$-FPT-evaluation AMT. There is an algorithm that given a $d \in \mathbb{N}$, a graph $G$, where $l := \mathbf{p}_1(G)$, and an $h_d$-tuple $\bar{R}$ of subsets of $V(G)$, outputs a subgraph $G'$ of $G$ and an $h_d$-tuple $\bar{R}'$ of subsets of $V(G')$, such that $\mathbf{p}_2(G') \le f(d, l)$ and $(G, \bar{R}) \equiv_{\Psi_d} (G', \bar{R}')$. Moreover, this algorithm runs in time $O_{d, \mathbf{p}_1(G)}(|G|^{\max\{c, c'\}+1})$.

*Proof.* Let $\mathbb{A}$ be the algorithm that certifies that $(\mathbf{L}_1, \mathbf{p}_1) \le_{n^{c'}} (\mathbf{L}_2, \mathbf{p}_2)$. Also, let $\mathbb{B}$ be an algorithm certifying that $(\mathbf{L}_2, \mathbf{p}_2)$ is an $n^c$-FPT-evaluation AMT. We start by setting $(G', \bar{R}') := (G, \bar{R})$. We also set $(R'_1, \dots, R'_{h_d}) := \bar{R}'$. The algorithm proceeds in two steps:

**Step 1.** Apply algorithm $\mathbb{A}$ with input $d$ and $(G', \bar{R}')$. If $\mathbb{A}$ reports that $\mathbf{p}_2(G') \le f(d, l)$, then stop. If it outputs a set $Y \subseteq V(G)$, a $\sigma_{d,l}$-structure $\mathfrak{B}$, where $Y \subseteq V(\mathfrak{B})$, an $h_d$-tuple $\bar{R}^{\mathfrak{B}}$ of subsets of $V(\mathfrak{B})$, and a set $Z \subseteq Y$ as in Definition 2.1, then proceed to Step 2.

**Step 2.** Let $\gamma_{\Psi_{-irr}}$ be the $\mathbb{L}_2$-formula defining $\Phi$-irrelevancy for $\Psi = \Psi_{d,l}$. Apply algorithm $\mathbb{B}$ with input $(\mathfrak{B}, \bar{R}^{\mathfrak{B}})$ to find some $S_0, \dots, S_{h_d} \subseteq Z$ where $S_0 \neq \emptyset$ and $(S_0, \dots, S_{h_d})$ is $\Psi_{d,l}$-irrelevant in $(\mathfrak{B}, \bar{R}^{\mathfrak{B}})$. Set $(G', \bar{R}') := (G' \setminus S_0, R'_1 \setminus S_1, \dots, R'_{h_d} \setminus S_{h_d})$ and repeat Step 1.

The correctness of the algorithm follows from the definition of $(S_0, \dots, S_{h_d})$ being $\Psi_{d,l}$-irrelevant in $(G', \bar{R}')$. The algorithm terminates because $\mathbf{p}_2(G) = O(|G|)$. For the running time, note that Step 1 is performed in time $O_{d, \mathbf{p}_1(G)}(|G|^c)$. Also, $|\gamma_{\Psi_{-irr}}|$ depends only on $|\Psi_{d,l}|$, which, in turn, depends only on $d$ and $l$ (which is equal to $\mathbf{p}_1(G)$). Moreover, $\mathbf{p}_2(G') \le f(d, l)$ and $|\mathfrak{B}| = O(|G'|)$. Thus, Step 2 is performed in time $O_{d, \mathbf{p}_1(G)}(|G|^{c'})$ and the overall running time is $O_{d, \mathbf{p}_1(G)}(|G|^{\max\{c, c'\}+1})$. $\square$

*Proof.* [Proof of Theorem 2.1] Let $c, c' \in \mathbb{N}_{\ge 1}$ and let $(\mathbf{L}_1, \mathbf{p}_1)$ and $(\mathbf{L}_2, \mathbf{p}_2)$ be two LP-pairs, where $(\mathbf{L}_1, \mathbf{p}_1) \le_{n^{c'}} (\mathbf{L}_2, \mathbf{p}_2)$. Also, let $\mathbb{B}$ be an algorithm certifying that $(\mathbf{L}_2, \mathbf{p}_2)$ is an $n^c$-FPT-evaluation AMT. We present an algorithm that certifies that $(\mathbf{L}_1, \mathbf{p}_1)$ is an $n^{\max\{c, c'\}+1}$-FPT-decision AMT. First, given a sentence $\varphi \in \mathbf{L}_1(\{E\})$, we compute the integer $h_{|\varphi|}$, the set $\Phi_{|\varphi|} \subseteq \mathbf{L}_2(\{E\})$ and the formula $\delta_{\varphi} \in \mathbf{L}_2(\{E, R_1, \dots, R_{h_{|\varphi|}}\})$. Note that $|\delta_{\varphi}|$ depends only on $|\varphi|$. To decide whether a given graph $G$ satisfies a given sentence $\varphi \in \mathbf{L}_1(\{E\})$, we perform the following two steps.

**Step 1.** Apply the algorithm of Lemma 2.1 with input $|\varphi|, G, (V(G))^{h_{|\varphi|}}$. This algorithm outputs a subgraph $G'$ of $G$ and an $h_d$-tuple $\bar{R}'$ of subsets of $V(G')$, such that $\mathbf{p}_2(G') \le f(|\varphi|, \mathbf{p}_1(G))$ and $(G, V(G)^{h_{|\varphi|}}) \equiv_{\Phi_{|\varphi|}} (G', \bar{R}')$.

**Step 2.** Apply algorithm $\mathbb{B}$ with input $(G', \bar{R}')$, which decides whether $(G', \bar{R}') \models \delta_{\varphi}$ and therefore whether $G \models \varphi$.

Note that $G \models \varphi \iff (G', \bar{R}') \models \delta_{\varphi}$, because $(G, V(G)^{h_{|\varphi|}}) \equiv_{\Phi_{|\varphi|}} (G', \bar{R}')$; see the *Definability Condition* of Definition 2.1. Step 1 is performed in time $O_{|\varphi|, \mathbf{p}_1(G)}(|G|^{\max\{c, c'\}+1})$, while Step 2 in time $O_{|\varphi|, \mathbf{p}_1(G)}(|G|^{c'})$, and thus the overall running time is $O_{|\varphi|, \mathbf{p}_1(G)}(|G|^{\max\{c, c'\}+1})$. $\square$

### 3 Conclusions and directions for further research

In this paper we proved that model checking on non-trivial minor-closed graph classes is tractable for problems expressible in the newly introduced logic CMSO/tw + dp (Theorem 1.1). We wish to stress that our proof is constructive, in the sense that one can construct a (meta-)algorithm that receives as an input a formula $\varphi \in \text{CMSO/tw} + \text{dp}$ and an integer $h$, and outputs an algorithm $\mathbb{A}_{\varphi, h}$ that, given an $K_h$-minor-free graph $G$, outputs whether $G \models \varphi$ or not.

**On the choice of tw in the parametrization of the quantifiers.** Note that, in the definition of CMSO/tw, based on the parameterized quantification introduced in (1.2), annotated treewidth plays a pivotal role. The annotated version of every minor-monotone graph parameter $p$ (such as treewidth, as it is our case) was defined in [78] by setting $p(G, X) := \max\{p(H) \mid H \text{ is an } X\text{-minor of } G\}$. Likewise, one may parameterize the quantification in CMSO formulas by setting

$$ \exists_{p \le k} X \varphi := \exists X (p(G, X) \le k \wedge \varphi), $$

hence defining the fragment CMSO/p of CMSO. Certainly, if $p$ is any parameter that is functionally larger than tw, then CMSO/tw is more expressive than CMSO/p (recall that a parameter $p$ is *functionally larger* than a parameter
$p'$ if there is a function $f: \mathbb{N} \to \mathbb{N}$ such that for every graph $G$, $p'(G) \le f(p(G))$. But what if we consider CMSO/$p$ for some parameter $p$ that is *not* functionally larger than $tw$? Such a parameter might be, for instance, the Euler genus, the apex$^9$ number, or the Hadwiger number. In such a case, the parameter $p$ would be bounded for all planar graphs, which, in turn, would imply that, on planar graphs, CMSO/$p$ would be as expressive as CMSO. This, combined with the impossibility results of [49, 50, 53] (see also [41, Section 9]) implies that no AMT as the one of Theorem 1.1 can be expected for CMSO/$p$ when $p$ is not functionally larger than treewidth. In this sense, the choice of treewidth in the definition of CMSO/tw is the best possible for an AMT as the one in Theorem 1.1. This justifies the use of $\exists_k X \varphi$ as a simplified way to write $\exists_{tw \le k} X \varphi$ in (1.2), and indicates that Theorem 1.1 is "optimal" in what concerns the choice of the fragment CMSO/tw.

The introduction of CMSO/$p$ for every minor-monotone parameter introduces a “fine-grained” viewpoint of CMSO whose algorithmic properties, in our opinion, deserve independent research. Is it possible to generate analogous hierarchies for other partial ordering relations and other fragments of CMSO, such as $\text{CMSO}_1$ where quantification is allowed only on vertex sets?

**Further than minors.** The next question is whether and when we may go further than the combinatorial threshold of minor-closedness. The next horizon for this might be topological minor-closedness, where we know that FO+conn and the more general FO+dp admit tractable model checking because of the results in [65] and [74], respectively. We are not in position to conjecture whether it is possible to replace, in Theorem 1.1, H-minor-freeness by H-topological-minor-freeness. However, we cannot exclude that this might be possible for CMSO/$p$ for some suitable choice of $p$ such as vc (vertex cover) or td (treedepth). Note that for all logics that subsume FO+conn, such as FO+dp, $\tilde{\mathbb{O}}^{\text{dp}}$, or CMSO/tw+dp (cf. Figure 1), H-topological-minor-freeness is the most general combinatorial condition we may hope for if we restrict to monotone graph classes (assuming a mild condition on the efficiency of the encoding), as proved in [65].

**Extending the predicates.** Another direction is to consider variants or extensions of CMSO/tw that use more expressive predicates than the disjoint paths. In this direction our proofs can be easily extended if, instead of $dp_k(s_1, t_1, \dots, s_k, t_k)$, we consider more powerful predicates as follows: $dp_k^1(A, s_1, t_1, \dots, s_k, t_k)$ where $A$ is a set containing vertices and edges (of small annotated treewidth) and we demand that the disjoint paths between the pairs of terminals $(s_1, t_1), \dots, (s_k, t_k)$ avoid all elements of $A$. The second is $dp_k^2(Z, S, s_1, t_1, \dots, s_k, t_k)$ where $Z$ and $S$ are vertex sets (of small annotated treewidth) and we demand that the disjoint paths between the pairs of terminals $(s_1, t_1), \dots, (s_k, t_k)$ avoid every edge incident to a vertex of a connected component of $G-Z$ that contains some vertex in $S$.

Another direction is to consider parity conditions in the paths of $dp_k(s_1, t_1, \dots, s_k, t_k)$. We believe that our technique can be applied in this direction as well.

**Irrelevant vertices in sub-quadratic time.** An insisting open question is whether (or when) it is possible to improve the quadratic running time of the algorithms implied by Theorem 1.1. Notice that this running time is quite linked to the idea of the irrelevant vertex technique, given that the irrelevant parts are removed one by one and the cost their detection is already linear. An improvement of the running time in Theorem 1.1 would require either the detection of “many” irrelevant vertices at once (this is been achieved so far for particular modification problems such as in [43]) or would be based on new ideas beyond the irrelevant vertex technique.

**Reductions between AMTs.** In Subsection 2.3 we defined a concept of reduction between AMTs based on the notion of *vertex irrelevancy* and the fact that “local irrelevancy”, certified by some AMT, may imply “global irrelevancy”, yielding AMTs on more general combinatorial structures. We defined this reducibility notion in a most abstract way as we believe that it might be a good base for the study, the understanding, and the proof of other AMTs in the future.

## References

[1] Anders Andersson. On second-order generalized quantifiers and finite structures. *Annals of Pure and Applied Logic*, 115(1):1–32, 2002.

<footnote n="9">⁹The *apex number* of a graph *G* is the minimum number of vertices whose removal yields a planar graph.</footnote>
[2] Stefan Arnborg, Jens Lagergren, and Detlef Seese. Easy Problems for Tree-Decomposable Graphs. *Journal of Algorithms*, 12(2):308–340, 1991.

[3] Mikołaj Bojańczyk. Thin MSO with a Probabilistic Path Quantifier. In *Proc. of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP)*, volume 55 of *LIPIcs*, pages 96:1–96:13, 2016.

[4] Mikołaj Bojańczyk, Edon Kelmendi, and Michał Skrzypczak. MSO+∇ is Undecidable. In *Proc. of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*. IEEE Press, 2021.

[5] Mikołaj Bojańczyk. Separator logic and star-free expressions for graphs. *arXiv preprint arXiv:2107.13953*, 2021.

[6] Édouard Bonnet, Jan Dreier, Jakub Gajarský, Stephan Kreutzer, Nikolas Mählmann, Pierre Simon, and Szymon Toruńczyk. Model checking on interpretations of classes of bounded local cliquewidth. In *Proc. of the 37th Annual ACM/IEEE Symposium on Logic in Computer (LICS)*, pages 54:1–54:13, 2022.

[7] Édouard Bonnet, Ugo Giocanti, Patrice Ossona de Mendez, Pierre Simon, Stéphan Thomassé, and Szymon Toruńczyk. Twin-width IV: ordered graphs and matrices. In *Proc. of the 54th Annual ACM Symposium on Theory of Computing (STOC)*, 2022.

[8] Édouard Bonnet, Eun Jung Kim, Stéphan Thomassé, and Rémi Watrigant. Twin-width I: tractable FO model checking. *Journal of the ACM*, 69(1):3:1–3:46, 2022.

[9] Richard B. Borie, R. Gary Parker, and Craig A. Tovey. Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graph families. *Algorithmica*, 7(5-6):555–581, 1992.

[10] Hans-Jörg Burtschick and Heribert Vollmer. Lindström quantifiers and leaf language definability. *International Journal of Foundations of Computer Science*, 09(03):277–294, 1998.

[11] Chandra Chekuri and Julia Chuzhoy. Polynomial bounds for the grid-minor theorem. *Journal of the ACM*, 63(5), 2016.

[12] Julia Chuzhoy. Improved Bounds for the Flat Wall Theorem. In *Proc. of the 26th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)*, pages 256–275, 2015.

[13] Bruno Courcelle. The monadic second-order logic of graphs. I. recognizable sets of finite graphs. *Information and Computation*, 85(1):12–75, 1990.

[14] Bruno Courcelle. The monadic second-order logic of graphs III: tree-decompositions, minor and complexity issues. *RAIRO - Theoretical Informatics and Applications*, 26:257–286, 1992.

[15] Bruno Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. In *Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations*, pages 313–400. World Scientific, 1997.

[16] Bruno Courcelle and Joost Engelfriet. *Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach*, volume 138 of *Encyclopedia of mathematics and its applications*. Cambridge University Press, 2012.

[17] Bruno Courcelle and Mohamed Mosbah. Monadic second-order evaluations on tree-decomposable graphs. *Theoretical Computer Science*, 109(1&2):49–82, 1993.

[18] Anuj Dawar, Martin Grohe, and Stephan Kreutzer. Locally excluding a minor. In *Proc. of the 21st IEEE Symposium on Logic in Computer Science (LICS)*, pages 270–279, 2007.

[19] Anuj Dawar and Stephan Kreutzer. Parameterized complexity of first-order logic. *Electronic Colloquium on Computational Complexity (ECCC)*, TR09-131, 2009.

[20] Erik D. Demaine, Fedor V. Fomin, Mohammad Taghi Hajiaghayi, and Dimitrios M Thilikos. Bidimensional parameters and local treewidth. *SIAM Journal on Discrete Mathematics*, 18(3):501–511, 2004.

[21] Jan Dreier, Ioannis Eleftheriadis, Nikolas Mählmann, Rose McCarty, Michał Pilipczuk, and Szymon Toruńczyk. First-order model checking on monadically stable graph classes. *arXiv preprint arXiv:2311.18740*, 2023.

[22] Jan Dreier, Nikolas Mählmann, and Sebastian Siebertz. First-order model checking on structurally sparse graph classes. In *Proc. of the 55th Annual ACM Symposium on Theory of Computing (STOC)*, pages 567–580, 2023.

[23] Jan Dreier, Nikolas Mählmann, and Szymon Toruńczyk. Flip-breakability: A combinatorial dichotomy for monadically dependent graph classes. In *Proc. of the 56th Annual ACM Symposium on Theory of Computing (STOC)*, page 1550–1560, New York, NY, USA, 2024. ACM.

[24] Zdeněk Dvořák, Daniel Král, and Robin Thomas. Testing first-order properties for subclasses of sparse graphs. *Journal of the ACM*, 60(5):36:1–36:24, 2013.

[25] Heinz-Dieter Ebbinghaus and Jörg Flum. *Finite model theory*. Perspectives in Mathematical Logic. Springer, 1999.

[26] Solomon Feferman and Robert L. Vaught. The first order properties of products of algebraic systems. *Fundamenta Mathematicae*, 47(1):57–103, 1959.

[27] Jörg Flum, Markus Frick, and Martin Grohe. Query evaluation via tree-decompositions. *Journal of the ACM*, 49(6):716–752, 2002.

[28] Jörg Flum and Martin Grohe. Fixed-parameter tractability, definability, and model-checking. *SIAM Journal on Computing*, 31(1):113–145, 2001.

[29] Fedor V. Fomin, Petr A. Golovach, Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. Compound logics for modification problems. In *Proc. of the 50th International Colloquium on Automata, Languages, and Programming*
(ICALP), volume 261 of LIPIcs, pages 61:1–61:21, 2023.

[30] Fedor V. Fomin, Petr A. Golovach, Giannos Stamoulis, and Dimitrios M. Thilikos. An algorithmic meta-theorem for graph modification to planarity and FOL. *ACM Transactions on Computation Theory*, 14(3-4):1–29, 2022.

[31] Jakub Gajarský. *Algorithmic Metatheorems for Restricted Classes of Graphs*. PhD thesis, Masaryk University, Brno, 2016.

[32] Jakub Gajarský, Maximilian Gorsky, and Stephan Kreutzer. Differential games, locality, and model checking for FO logic of graphs. In *Proc. of the 30th EACSL Annual Conference on Computer Science Logic (CSL)*, volume 216 of *LIPIcs*, pages 22:1–22:18, 2022.

[33] Jakub Gajarský, Petr Hliněný, Jan Obdržálek, Daniel Lokshtanov, and M. S. Ramanujan. A new perspective on FO model checking of dense graph classes. *ACM Transactions on Computational Logic*, 21(4), 2020.

[34] Jakub Gajarský, Stephan Kreutzer, Jaroslav Nešetřil, Patrice Ossona De Mendez, Michał Pilipczuk, Sebastian Siebertz, and Szymon Toruńczyk. First-order interpretations of bounded expansion classes. *ACM Transactions on Computational Logic*, 21(4), 2020.

[35] Archontia C. Giannopoulou and Dimitrios M. Thilikos. Optimizing the graph minors weak structure theorem. *SIAM Journal on Discrete Mathematics*, 27(3):1209–1227, 2013.

[36] Petr A. Golovach, Marcin Kaminski, Spyridon Maniatis, and Dimitrios M. Thilikos. The parameterized complexity of graph cyclability. *SIAM Journal on Discrete Mathematics*, 31(1):511–541, 2017.

[37] Petr A. Golovach, Giannos Stamoulis, and Dimitrios M. Thilikos. Model-checking for first-order logic with disjoint paths predicates in proper minor-closed graph classes. *arXiv preprint arXiv:2211.01723*, 2022.

[38] Petr A. Golovach, Giannos Stamoulis, and Dimitrios M. Thilikos. Model-checking for first-order logic with disjoint paths predicates in proper minor-closed graph classes. In *Proc. of the 34th ACM-SIAM Symposium on Discrete Algorithms (SODA)*, pages 3684–3699, 2023.

[39] Erich Grädel, Wolfgang Thomas, and Thomas Wilke. *Automata, logics, and infinite games: a guide to current research*, volume 2500. Springer, 2003.

[40] Martin Grohe. Algorithmic meta theorems. In *Proc. of the 34th International Workshop on Graph-Theoretic Concepts in Computer Science (WG)*, volume 5344 of *Lecture Notes in Computer Science*, page 30, 2008.

[41] Martin Grohe and Stephan Kreutzer. Methods for algorithmic meta theorems. In *Model Theoretic Methods in Finite Combinatorics - AMS-ASL Joint Special Session*, volume 558, pages 181–206. AMS, 2009.

[42] Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding first-order properties of nowhere dense graphs. *Journal of the ACM*, 64(3):17:1–17:32, 2017.

[43] Ken-ichi Kawarabayashi. Planarity allowing few error vertices in linear time. In *Proc. of the 50th Annual IEEE Symposium on Foundations of Computer Science (FOCS)*, pages 639–648, 2009.

[44] Ken-ichi Kawarabayashi, Yusuke Kobayashi, and Bruce A. Reed. The disjoint paths problem in quadratic time. *Journal of Combinatorial Theory, Series B*, 102(2):424–435, 2012.

[45] Ken-ichi Kawarabayashi, Robin Thomas, and Paul Wollan. A new proof of the flat wall theorem. *Journal of Combinatorial Theory, Series B*, 129:204–238, 2018.

[46] Dusan Knop, Martin Koutecký, Tomáš Masarík, and Tomáš Toufar. Simplified algorithmic metatheorems beyond MSO: treewidth and neighborhood diversity. *Logical Methods in Computer Science*, 15(4), 2019.

[47] Juha Kontinen. Definability of second order generalized quantifiers. *Archive for Mathematical Logic*, 49(3):379–398, 2010.

[48] Stephan Kreutzer. Algorithmic meta-theorems. In *Finite and Algorithmic Model Theory*, volume 379 of *London Mathematical Society Lecture Note Series*, pages 177–270. Cambridge University Press, 2011.

[49] Stephan Kreutzer. On the parameterized intractability of monadic second-order logic. *Logical Methods in Computer Science*, 8(1), 2012.

[50] Stephan Kreutzer and Siamak Tazari. Lower bounds for the complexity of monadic second-order logic. In *Proc. of the 25th Annual IEEE Symposium on Logic in Computer Science (LICS)*, page 189–198, 2010.

[51] Leonid Libkin. *Elements of Finite Model Theory*. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.

[52] Per Lindström. First order predicate logic with generalized quantifiers. *Theoria*, 32(3):186–195, 1966.

[53] Johann A. Makowsky and Julian P. Mariño. Tree-width and the monadic quantifier hierarchy. *Theoretical Computer Science*, 303(1):157–170, 2003. Logic and Complexity in Computer Science.

[54] Henryk Michalewski and Matteo Mio. Measure quantifier in monadic second order logic. In *Proc. of the International Symposium on Logical Foundations of Computer Science (LFCS)*, pages 267–282, 2016.

[55] Matteo Mio, Michał Skrzypczak, and Henryk Michalewski. Monadic Second Order Logic with Measure and Category Quantifiers. *Logical Methods in Computer Science*, Volume 14, Issue 2, 2018.

[56] Laure Morelle, Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. Faster parameterized algorithms for modification problems to minor-closed classes. In *Proc. of the 50th International Colloquium on Automata, Languages, and Programming (ICALP)*, volume 261 of *LIPIcs*, pages 93:1–93:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2023.

[57] Laure Morelle, Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. Faster parameterized algorithms for modification problems to minor-closed classes. *TheoretiCS*, 3, 2024.

[58] Andrzej Mostowski. On a generalization of quantifiers. *Fundamenta Mathematicae*, 44(1):12–36, 1957.

[59] Jaroslav Nešetřil and Patrice Ossona de Mendez. *Sparsity - Graphs, Structures, and Algorithms*, volume 28 of *Algorithms and combinatorics*. Springer, 2012.

[60] Jaroslav Nešetřil and Patrice Ossona de Mendez. Grad and classes with bounded expansion. I. Decompositions. *European Journal of Combinatorics*, 29(3):760–776, 2008.

[61] Jaroslav Nešetřil and Patrice Ossona de Mendez. Grad and classes with bounded expansion. II. Algorithmic aspects. *European Journal of Combinatorics*, 29(3):777–791, 2008.

[62] Jaroslav Nešetřil and Patrice Ossona de Mendez. Grad and classes with bounded expansion. III. Restricted graph homomorphism dualities. *European Journal of Combinatorics*, 29(4):1012–1024, 2008.

[63] Christophe Paul, Evangelos Protopapas, Dimitrios M. Thilikos, and Sebastian Wiederrecht. Obstructions to Erdös-Pósa Dualities for Minors. arXiv preprint arXiv:2407.09671, 2024.

[64] Christophe Paul, Evangelos Protopapas, Dimitrios M. Thilikos, and Sebastian Wiederrecht. Obstructions to erdős-pósa dualities for minors. In *Proc. of the 65rd IEEE Annual Symposium on Foundations of Computer Science (FOCS)*. IEEE, 2024.

[65] Michał Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Toruńczyk, and Alexandre Vigny. Algorithms and data structures for first-order logic with connectivity under vertex failures. In *Proc. of the 49th International Colloquium on Automata, Languages, and Programming, (ICALP)*, volume 229 of LIPIcs, pages 102:1–102:18, 2022.

[66] Neil Robertson and Paul D. Seymour. Graph Minors. V. Excluding a planar graph. *Journal of Combinatorial Theory, Series B*, 41(2):92–114, 1986.

[67] Neil Robertson and Paul D. Seymour. Graph Minors. XIII. The Disjoint Paths Problem. *Journal of Combinatorial Theory, Series B*, 63(1):65–110, 1995.

[68] Neil Robertson and Paul D. Seymour. Graph Minors. XX. Wagner's conjecture. *Journal of Combinatorial Theory, Series B*, 92(2):325–357, 2004.

[69] Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. An fpt-algorithm for recognizing k-apices of minor-closed graph classes. In *Proc. of the 47th International Colloquium on Automata, Languages, and Programming (ICALP)*, volume 168 of LIPIcs, pages 95:1–95:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.

[70] Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. *k*-apices of Minor-closed Graph Classes. II. Parameterized Algorithms. *ACM Transactions on Algorithms*, 18(3):21:1–21:30, 2022.

[71] Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. *k*-apices of minor-closed graph classes. I. Bounding the obstructions. *Journal of Combinatorial Theory, Series B*, 161:180–227, 2023.

[72] Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. A more accurate view of the Flat Wall Theorem. *Journal of Graph Theory*, 2024.

[73] Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. Parameterizing the quantification of CMSO: model checking on minor-closed graph classes. arXiv preprint arXiv:2406.18465, 2024.

[74] Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M. Thilikos, and Alexandre Vigny. Model checking disjoint-paths logic on topological-minor-free graph classes. In *Proc. of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*. ACM, 2024.

[75] Nicole Schirrmacher, Sebastian Siebertz, and Alexandre Vigny. First-order logic with connectivity operators. *ACM Transactions on Computational Logic*, 24(4), 2023.

[76] Detlef Seese. Linear time computable problems and first-order descriptions. *Mathematical Structures in Computer Science*, 6(6):505–526, 1996.

[77] Saharon Shelah. The monadic theory of order. *Annals of Mathematics*, 102(3):379–419, 1975.

[78] Dimitrios M. Thilikos and Sebastian Wiederrecht. Excluding surfaces as minors in graphs. *CoRR*, abs/2306.01724, 2023.

[79] Jouko Väänänen. Generalized quantifiers, an introduction. In *Generalized Quantifiers and Computation*, pages 1–17. Springer Berlin Heidelberg, 1999.