Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph Classes
Ignasi Sau, Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M. Thilikos, Alexandre Vigny

TL;DR
This paper extends algorithmic meta-theorems to a fragment of CMSO logic, showing fixed-parameter tractability for model checking on topological-minor-free graph classes, thus broadening tractability results beyond FO logic.
Contribution
It introduces a new fragment of CMSO based on low monodimensionality and proves fixed-parameter tractability of model checking on topological-minor-free graphs.
Findings
Model checking for the new CMSO fragment is fixed-parameter tractable on topological-minor-free graphs.
The results generalize several known logics and meta-theorems.
They extend tractability results beyond first-order logic to richer logical fragments.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
