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

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 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.