A Logic for Minor-Free Graph Classes: Model Checking, Dependence, and Combinatorial Reconfiguration
Abstract
We introduce \emph{sub-connectivity logic}, denoted by textsfFOscon, an extension of first-order logic for graphs with a specified set Z of admissible edges. Its additional atom textsfscon(x,y;z̅) asserts that x and y are connected by a path using only edges of Z and avoiding the vertices in z̅. Our main structural result states that, for every weakly sparse graph class 𝒞, the class of all expansions of graphs in 𝒞 by rooted spanning forest orders has bounded twin-width if and only if 𝒞 excludes a fixed minor. When 𝒞 excludes a fixed minor, we can also compute an additional linear order that preserves bounded twin-width in polynomial time. We translate textsfFOscon into first-order logic over an expansion by a depth-first spanning forest order of the admissible-edge graph. Combining this translation with our structural result, we obtain a model checking algorithm for textsfFOscon with running time f(|ϕ|,h(G))· |G|c, where f is computable, c is an absolute constant, and h(G) is the Hadwiger number of G. The translation and model-checking algorithm extend to binary relational structures, with the Hadwiger number measured on the Gaifman graph. For a graph class 𝒞 let 𝒞Z:={(G,Z):G∈𝒞, Z⊆ E(G)}. We show that for every weakly sparse graph class 𝒞, the class 𝒞Z is monadically dependent for textsfFOscon if and only if 𝒞 excludes a fixed minor. For monotone classes that admit efficient minor encodings, a corresponding hardness result makes this frontier computationally tight. We give applications to combinatorial reconfiguration and solution discovery problems, and study a guarded extension of textsfFOscon motivated by database queries.
Related
- First-Order Model Checking on Monadically Dependent Graph Classes
- Multiple Nonlinear Waves by (Quantum) Neural Networks: Checking the AI supremacy
- Co-Decompositions and FO Model Checking
- Stochastic Mirror-Prox Optimisation of Group Distributionally Robust Multimodal Logistic Regression for Multilingual Fact-Checking Verdict Prediction
- Optimizing Both Checking and Update Costs in Random Walk Search
BibTeX
@misc{mahlmann2026logic,
title = {{A Logic for Minor-Free Graph Classes: Model Checking, Dependence, and Combinatorial Reconfiguration}},
author = {Nikolas Mählmann and Patrice Ossona de Mendez and Nicole Schirrmacher and Sebastian Siebertz and Giannos Stamoulis and Dimitrios M. Thilikos and Alexandre Vigny},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.05263},
eprint = {2610.05263},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.05263},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - A Logic for Minor-Free Graph Classes: Model Checking, Dependence, and Combinatorial Reconfiguration
AU - Nikolas Mählmann
AU - Patrice {Ossona de Mendez}
AU - Nicole Schirrmacher
AU - Sebastian Siebertz
AU - Giannos Stamoulis
AU - {Dimitrios M. } Thilikos
AU - Alexandre Vigny
PY - 2026
DA - 2026/10/04
PB - arXiv
DO - 10.48550/arxiv.2610.05263
UR - https://arxiv.org/abs/2610.05263
AB - We introduce \emph{sub-connectivity logic}, denoted by textsfFOscon, an extension of first-order logic for graphs with a specified set Z of admissible edges. Its additional atom textsfscon(x,y;z̅) asserts that x and y are connected by a path using only edges of Z and avoiding the vertices in z̅. Our main structural result states that, for every weakly sparse graph class 𝒞, the class of all expansions of graphs in 𝒞 by rooted spanning forest orders has bounded twin-width if and only if 𝒞 excludes a fixed minor. When 𝒞 excludes a fixed minor, we can also compute an additional linear order that preserves bounded twin-width in polynomial time. We translate textsfFOscon into first-order logic over an expansion by a depth-first spanning forest order of the admissible-edge graph. Combining this translation with our structural result, we obtain a model checking algorithm for textsfFOscon with running time f(|ϕ|,h(G))· |G|^c, where f is computable, c is an absolute constant, and h(G) is the Hadwiger number of G. The translation and model-checking algorithm extend to binary relational structures, with the Hadwiger number measured on the Gaifman graph. For a graph class 𝒞 let 𝒞_Z:={(G,Z):G∈𝒞, Z⊆ E(G)}. We show that for every weakly sparse graph class 𝒞, the class 𝒞_Z is monadically dependent for textsfFOscon if and only if 𝒞 excludes a fixed minor. For monotone classes that admit efficient minor encodings, a corresponding hardness result makes this frontier computationally tight. We give applications to combinatorial reconfiguration and solution discovery problems, and study a guarded extension of textsfFOscon motivated by database queries.
ER -