arxiv: 2605.00192 · v1 · submitted 2026-04-30 · 💻 cs.LO · math.CO

Recognition: unknown

Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph Classes

Alexandre Vigny, Dimitrios M. Thilikos, Giannos Stamoulis, Ignasi Sau, Nicole Schirrmacher, Sebastian Siebertz

Pith reviewed 2026-05-09 19:46 UTC · model grok-4.3

classification 💻 cs.LO math.CO

keywords CMSOmodel checkingfixed-parameter tractabilitytopological minorsalgorithmic meta-theoremsdisjoint pathsannotated graphsmonodimensionality

0 comments

The pith

Model checking for the low-monodimensionality fragment of CMSO with the disjoint-paths predicate is fixed-parameter tractable on topological-minor-free graph classes.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops an annotated-graph framework that fragments CMSO by restricting set quantification to vertex sets of low monodimensionality. It establishes that model checking for this fragment, augmented with the disjoint-paths predicate, is fixed-parameter tractable on graphs excluding any fixed topological minor. A reader would care because these graph classes are maximal for subgraph-closed families where such tractability can hold, and the result lifts known meta-theorems from first-order logic to a strictly richer setting. The approach reduces the problem to cases already known to be tractable by prior work on annotated graphs.

Core claim

We identify a fragment of CMSO defined by allowing quantification only over sets having low monodimensionality, which generalizes several previously known logics. We show that model checking for this fragment, enhanced with the disjoint-paths predicate, is fixed-parameter tractable on topological-minor-free graph classes. Such classes essentially delimit the tractability for this logic on subgraph-closed classes. As a consequence, our results lift several known algorithmic meta-theorems beyond first-order logic to the topological-minor-free setting.

What carries the argument

Annotated graph parameters that restrict set quantification in CMSO to vertex sets of low monodimensionality, together with the disjoint-paths predicate.

If this is right

The tractability result applies directly to all logics previously known to be captured by the low-monodimensionality fragment.
Several algorithmic meta-theorems that were previously limited to first-order logic now extend to this richer counting monadic second-order setting.
The boundary of tractability for the logic on subgraph-closed classes is exactly the topological-minor-free graph classes.
Any problem expressible in this fragment admits an FPT algorithm on every topological-minor-free class when the formula is the parameter.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same annotated-parameter technique may apply to other natural restrictions on set quantification beyond monodimensionality.
Concrete problems such as variants of disjoint-paths routing or packing that are expressible in the fragment become FPT on all topological-minor-free classes.
If the reduction step can be made uniform, the same proof strategy could be reused for further extensions of the logic on the same graph classes.

Load-bearing premise

The low-monodimensionality restriction on quantified sets together with the disjoint-paths predicate is enough to reduce every model-checking instance to a form already known to be tractable via the annotated-graph framework.

What would settle it

An explicit topological-minor-free graph class together with a concrete low-monodimensionality CMSO formula containing the disjoint-paths predicate for which model checking is not fixed-parameter tractable in the formula size would falsify the claim.

read the original abstract

Algorithmic meta-theorems explain the tractability of large classes of computational problems by linking logical expressibility with structural graph properties. While extensions of first-order logic such as FO+dp admit efficient model checking on graph classes excluding a fixed topological minor, comparable results for richer fragments of CMSO were previously unknown. We further develop the framework of Sau, Stamoulis, and Thilikos [SODA 2025] for fragmenting CMSO via annotated graph parameters, which restrict set quantification to vertex sets satisfying bounded structural conditions. Following this approach, we identify a fragment of CMSO, namely the one defined by allowing quantification only over sets having what we call low monodimensionality, that generalizes several previously-known logics and we show that model checking for this fragment, enhanced with the disjoint-paths predicate, is fixed-parameter tractable on topological-minor-free graph classes. Such classes essentially delimit the tractability for this logic on subgraph-closed classes. As a consequence, our results lift several known algorithmic meta-theorems beyond first-order logic to the topological-minor-free setting.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper carves out a low-monodimensionality fragment of CMSO and proves FPT model checking with disjoint paths on topological-minor-free graphs by direct reduction to the 2025 annotated-graph framework.

read the letter

The core result is that model checking for this restricted fragment of CMSO, plus the disjoint-paths predicate, is fixed-parameter tractable on graphs excluding a fixed topological minor. The authors achieve it by restricting set quantifiers to vertex sets of low monodimensionality and showing that this bound carries through the existing meta-theorem from Sau, Stamoulis, and Thilikos without extra cost to the parameter or the graph class. That class is already known to be the right boundary for subgraph-closed families, so the lift from FO stays inside the same tractability region. The reduction is presented as explicit, with the new predicate folded in cleanly. This is the main new piece: a concrete, usable fragment that generalizes several earlier logics while inheriting the prior FPT machinery. The paper does a straightforward job of stating the fragment, mapping it onto the annotated parameters, and confirming the boundary claim. No circularity or hidden fitting appears in the argument. One soft spot is that low monodimensionality is defined via a structural parameter on quantified sets, and while the abstract lists generalizations, it is not yet clear how many natural counting problems sit strictly inside this fragment but outside the older ones. That is a question of scope rather than correctness. The technical steps look solid enough that the central claim should hold. This is a paper for people already working on algorithmic meta-theorems and logic on sparse graphs. A reader who follows the SODA 2025 line will find the extension useful and the proof strategy familiar. It has enough formal grounding and a clear new statement to merit a serious referee.

Referee Report

0 major / 3 minor

Summary. The manuscript introduces the low-monodimensionality restriction on set quantifiers in CMSO, augments the logic with the disjoint-paths predicate, and proves that model checking for this fragment is fixed-parameter tractable on topological-minor-free graph classes by an explicit reduction to the annotated-graph meta-theorem of Sau, Stamoulis, and Thilikos. The result generalizes prior FO and FO+dp meta-theorems and asserts that topological-minor-free classes essentially delimit tractability for the logic on subgraph-closed families.

Significance. If the central reduction holds, the work meaningfully extends algorithmic meta-theorems beyond first-order logic to a natural fragment of CMSO on an important structural graph class. The mapping of low monodimensionality onto existing annotated-graph parameters, together with the preservation of the bound when adding the disjoint-paths predicate, supplies a clean lifting of earlier results and strengthens the boundary picture for subgraph-closed classes.

minor comments (3)

Abstract: the term 'low monodimensionality' and the phrase 'annotated graph parameters' are used without a one-sentence gloss or pointer to the formal definition, which reduces immediate accessibility for readers outside the immediate sub-area.
Introduction (or §1): the assertion that topological-minor-free classes 'essentially delimit the tractability for this logic on subgraph-closed classes' is stated without a supporting hardness reference or cross-pointer; a single sentence or citation would strengthen the claim.
Notation and definitions: ensure that the precise mapping from the low-monodimensionality parameter to the annotated-graph parameter of Sau et al. is stated with an explicit equation or lemma number so that the reduction step can be checked at a glance.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our manuscript, the accurate summary of its contributions, and the recommendation for minor revision. The work extends algorithmic meta-theorems by identifying the low-monodimensionality fragment of CMSO (augmented with the disjoint-paths predicate) and establishing its FPT model-checking complexity on topological-minor-free classes via reduction to the annotated-graph meta-theorem of Sau, Stamoulis, and Thilikos. No specific major comments appear in the report, so we address the overall evaluation below.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper extends the annotated-graph framework from the cited prior work of Sau, Stamoulis, and Thilikos but introduces a new structural parameter (low monodimensionality) and proves a fresh FPT result for the enhanced CMSO fragment on topological-minor-free classes. No equation or claim in the abstract reduces the tractability statement to a definitional identity, a fitted input renamed as prediction, or an unverified self-citation chain; the argument is presented as an explicit reduction that incorporates the disjoint-paths predicate without increasing the parameter bound. The derivation therefore retains independent content beyond its inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on the definition of low monodimensionality (a new structural restriction introduced in the paper) and on the correctness of the prior SODA 2025 framework for annotated graphs. No numerical free parameters appear in the abstract. The disjoint-paths predicate is treated as an added primitive whose interaction with the fragment is handled by the reduction.

axioms (2)

standard math Standard definitions of fixed-parameter tractability and topological-minor-free graph classes.
Invoked implicitly when stating the complexity result.
domain assumption The annotated-graph framework of Sau, Stamoulis, and Thilikos (SODA 2025) correctly reduces model checking under bounded structural parameters.
The paper states it follows this approach.

invented entities (1)

low monodimensionality no independent evidence
purpose: Structural restriction on quantified sets that makes the logic fragment tractable.
Newly defined in the paper to generalize previously known logics.

pith-pipeline@v0.9.0 · 5516 in / 1493 out tokens · 23920 ms · 2026-05-09T19:46:48.311471+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

25 extracted references · 24 canonical work pages · 1 internal anchor

[1]

Journal of Algorithms , volume =

1 Stefan Arnborg, Jens Lagergren, and Detlef Seese. Easy problems for tree-decomposable graphs.Journal of Algorithms, 12(2):308–340, 1991.doi:10.1016/0196-6774(91)90006-K. 2 Julien Baste, Michael R. Fellows, Lars Jaffke, Tomás Masarík, Mateus de Oliveira Oliveira, Geevarghese Philip, and Frances A. Rosamond. Diversity of solutions: An exploration through ...

work page doi:10.1016/0196-6774(91)90006-k 1991
[2]

3 Julien Baste, Ignasi Sau, and Dimitrios M

URL: https://doi.org/10.1016/j.artint.2021.103644,doi:10.1016/J.ARTINT.2021.103644. 3 Julien Baste, Ignasi Sau, and Dimitrios M. Thilikos. A complexity dichotomy for hitting connected minors on bounded treewidth graphs: the chair and the banner draw the boundary. InProc. of the 31st Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 951–970, 2...

work page doi:10.1016/j.artint.2021.103644 2021
[3]

Twin-width I: Tractable FO Model Checking

9 É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.doi:10.1145/3486655. 10 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 gra...

work page doi:10.1145/3486655 2022
[4]

doi:10.1016/j.jctb.2020. 09.010. 13 Bruno Courcelle. The monadic second-order logic of graphs. I. recognizable sets of finite graphs. Information and Computation, 85(1):12–75, 1990.doi:10.1016/0890-5401(90)90043-H. 14 Bruno Courcelle. The Monadic Second-Order logic of graphs. I. Recognizable sets of finite graphs.Information and Computation, 85(1):12–75,

work page doi:10.1016/j.jctb.2020 2020
[5]

Informatics Appl.26, 5 (1992), 403–424

doi:10.1051/ita/1992260302571. 16 Bruno Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. InHandbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, pages 313–400. World Scientific,

work page doi:10.1051/ita/1992260302571
[6]

21 Erik D

doi:10.1109/LICS.2007.31. 21 Erik D. Demaine, Fedor V. Fomin, Mohammadtaghi Hajiaghayi, and Dimitrios M. Thilikos. Bidimensional parameters and local treewidth.SIAM J. Discrete Math., 18(3):501–511, 2004/05.doi:10.1137/S0895480103433410. 22 Rodney G. Downey and Michael R. Fellows.Fundamentals of Parameterized Complexity. Texts in Computer Science. Springe...

work page doi:10.1109/lics.2007.31 2007
[7]

Proceedings of the 55th Annual ACM Symposium on Theory of Computing , pages =

24 Jan Dreier, Nikolas Mählmann, and Sebastian Siebertz. First-order model checking on structurally sparse graph classes. InProc. of the 55th Annual ACM Symposium on Theory of Computing (STOC), pages 567–580, 2023.doi:10.1145/3564246.3585186. 25 Jan Dreier, Nikolas Mählmann, Sebastian Siebertz, and Szymon Toruńczyk. Indiscernibles and Flatness in Monadica...

work page doi:10.1145/3564246.3585186 2023
[8]

Approximate evaluation of first-order counting queries

27 Jan Dreier and Peter Rossmanith. Approximate evaluation of first-order counting queries. InProceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 1720–1739. SIAM, 2021.doi:10.1137/1.9781611976465.104. 28 Zdeněk Dvořák, Daniel Král, and Robin Thomas. Deciding first-order properties for sparse graphs. InProceedings of the IEEE 51...

work page doi:10.1137/1.9781611976465.104 2021
[9]

Testing first-order properties for subclasses of sparse graphs.Journal of the ACM, 60(5):36:1–36:24, 2013.doi:10.1145/2499483

29 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.doi:10.1145/2499483. 42 Low Monodimensionality Fragments ofCMSO 30 Heinz-Dieter Ebbinghaus and Jörg Flum.Finite model theory. Springer Science & Business Media,

work page doi:10.1145/2499483 2013
[10]

Measuring what matters: a hybrid approach to dynamic programming with treewidth.J

31 Eduard Eiben, Robert Ganian, Thekla Hamm, and O-joung Kwon. Measuring what matters: a hybrid approach to dynamic programming with treewidth.J. Comput. System Sci., 121:57–75, 2021.doi:10.1016/j.jcss.2021.04.005. 32 Fedor V. Fomin, Petr A. Golovach, Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. Compound logics for modification problems.ACM T...

work page doi:10.1016/j.jcss.2021.04.005 2021
[11]

Deciding first-order properties of locally tree-decomposable structures.Journal of the ACM, 48(6):1184–1206, 2001.doi:10.1145/504794.504798

33 Markus Frick and Martin Grohe. Deciding first-order properties of locally tree-decomposable structures.Journal of the ACM, 48(6):1184–1206, 2001.doi:10.1145/504794.504798. 34 Jakub Gajarský, Nikolas Mählmann, Rose McCarty, Pierre Ohlmann, Michal Pilipczuk, Wojciech Przybyszewski, Sebastian Siebertz, Marek Sokolowski, and Szymon Torunczyk. Flipper games...

work page doi:10.1145/504794.504798 2001
[12]

37 Martin Grohe

doi:10.1137/1.9781611977554.ch141. 37 Martin Grohe. Logic, graphs, and algorithms.Electronic Colloquium on Computational Complexity, TR07,

work page doi:10.1137/1.9781611977554.ch141
[13]

Algorithmic meta theorems

38 Martin Grohe. Algorithmic meta theorems. InProc. of the 34th International Workshop on Graph-Theoretic Concepts in Computer Science (WG), volume 5344 ofLecture Notes in Computer Science, page 30, 2008.doi:10.1007/978-3-540-92248-3\_3. 39 Martin Grohe, Ken-ichi Kawarabayashi, Dániel Marx, and Paul Wollan. Finding topological subgraphs is fixed-parameter...

work page doi:10.1007/978-3-540-92248-3 2008
[14]

and Kreutzer, S

URL:http://citeseerx.ist.psu.edu/viewdoc/download?doi= 10.1.1.395.8282. 41 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.doi:10.1145/3051095. 42 Martin Grohe and Nicole Schweikardt. First-order query evaluation with cardinality conditions. InProcee...

work page doi:10.1145/3051095 2017
[15]

Quickly excluding an apex- forest, 2025.arXiv:2404.17306

43 Jędrzej Hodor, Hoang La, Piotr Micek, and Clément Rambaud. Quickly excluding an apex- forest, 2025.arXiv:2404.17306. 44 Bart M. P. Jansen and Céline M. F. Swennenhuis. Steiner Tree Parameterized by Multiway Cut and Even Less. InProc. of the 32nd Annual European Symposium on Algorithms (ESA), volume 308 ofLIPIcs, pages 76:1–76:16, 2024.doi:10.4230/LIPIC...

work page doi:10.4230/lipics.esa.2024.76 2025
[16]

Lower bounds for the complexity of monadic second- order logic

46 Stephan Kreutzer and Siamak Tazari. Lower bounds for the complexity of monadic second- order logic. InProceedings of the 2010 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 189–198. IEEE,

2010
[17]

Elements of Finite Model Theory

URL:http://www.cs.toronto.edu/%7Elibkin/fmt,doi: 10.1007/978-3-662-07003-1. 50 Daniel Marx, Paul Seymour, and Paul Wollan. Rooted grid minors.J. Combin. Theory Ser. B, 122:428–437, 2017.doi:10.1016/j.jctb.2016.07.003. 51 Michał Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Toruńczyk, and Alex- andre Vigny. Algorithms and data structures for f...

work page doi:10.1007/978-3-662-07003-1 2017
[18]

52 Evangelos Protopapas, Dimitrios M

doi:10.4230/LIPIcs.ICALP.2022.102. 52 Evangelos Protopapas, Dimitrios M. Thilikos, and Sebastian Wiederrecht. Colorful minors,

work page doi:10.4230/lipics.icalp.2022.102 2022
[19]

Colorful Minors

URL:https://arxiv.org/abs/2507.10467,arXiv:2507.10467. 53 Neil Robertson and Paul D. Seymour. Graph Minors. V. Excluding a planar graph.Journal of Combinatorial Theory, Series B, 41(2):92–114, 1986.doi:10.1016/0095-8956(86)90030-4. 54 NeilRobertsonandPaulD.Seymour. GraphMinors.XIII.TheDisjointPathsProblem.Journal of Combinatorial Theory, Series B, 63(1):6...

work page internal anchor Pith review Pith/arXiv arXiv doi:10.1016/0095-8956(86)90030-4 1986
[20]

doi:10.1016/j.jctb.2009.07

work page doi:10.1016/j.jctb.2009.07 2009
[21]

Thilikos

56 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.arXiv:2406.18465. 57 Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. Parameterizing the quantification of CMSO: model checking on minor-closed graph classes. In...

work page arXiv 2024
[22]

58 Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M

doi:10.1137/1.9781611978322.124. 58 Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M. Thilikos, and Alexandre Vigny. Model checking disjoint-paths logic on topological-minor-free graph classes. CoRR, abs/2302.07033,

work page doi:10.1137/1.9781611978322.124
[23]

59 Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M

This is the full version of [59].arXiv:2302.07033. 59 Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M. Thilikos, and Alexandre Vigny. Model checking disjoint-paths logic on topological-minor-free graph classes. InProc. of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 68:1–68:12. ACM, 2024.doi:10.1145...

work page doi:10.1145/3661814.3662089 2024
[24]

61 Detlef Seese

doi:10.1145/3595922. 61 Detlef Seese. Linear time computable problems and first-order descriptions.Mathematical Structures in Computer Science, 6(6):505–526, 1996.doi:10.1017/S0960129500070079. 62 Sebastian Siebertz and Alexandre Vigny. Advances in algorithmic meta theorems (invited paper). In Siddharth Barman and Slawomir Lasota, editors,44th IARCS Annua...

work page doi:10.1145/3595922 1996
[25]

URL:https://arxiv.org/abs/2306.01724,arXiv:2306.01724

work page arXiv