Document Open Access Logo

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

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.80.pdf
  • Filesize: 1.07 MB
  • 27 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
  • Theory of computation → Graph algorithms analysis
  • Theory of computation → Parameterized complexity and exact algorithms
  • Mathematics of computing → Graph theory
Keywords
  • Monadic second-order logic
  • Dynamic programming
  • Graph minors
  • Monodimentionality
  • Annotated parameters

Metrics

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.

Cite As Get BibTex

Ignasi Sau, Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M. Thilikos, and Alexandre Vigny. Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph Classes. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 80:1-80:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.80

Author Details

Ignasi Sau
  • LIRMM, Univ Montpellier, CNRS, Montpellier, France
Nicole Schirrmacher
  • University of Bremen, Germany
Sebastian Siebertz
  • University of Bremen, Germany
Giannos Stamoulis
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
Dimitrios M. Thilikos
  • LIRMM, Univ Montpellier, CNRS, Montpellier, France
Alexandre Vigny
  • LIMOS, Univ Clermont Auvergne, Clermont Auvergne INP, France

Funding

  • Sau, Ignasi: National Research Agency (ANR) project ELIT (ANR-20-CE48-0008-01).
  • Schirrmacher, Nicole: French-German Collaboration ANR/DFG Project UTMA (ANR-20-CE92-0027, DFG 446200270).
  • Thilikos, Dimitrios M.: French-German Collaboration ANR/DFG Project UTMA (ANR-20-CE92-0027, DFG 446200270), Franco-Norwegian project PHC AURORA 2024-2025 (Projet n° 51260WL), and French National Research Agency GODASse ANR-24-CE48-4377 and France 2030 grant reference number ANR-24-RRII-0002 operated by the Inria Quadrant Program.
  • Vigny, Alexandre: French National Research Agency ANR-23-IACL-0006.

Acknowledgements

We wish to thank the anonymous reviewers for their comments and remarks.

References

  1. Stefan Arnborg, Jens Lagergren, and Detlef Seese. Easy problems for tree-decomposable graphs. Journal of Algorithms, 12(2):308-340, 1991. URL: https://doi.org/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 the lens of fixed-parameter tractability theory. Artif. Intell., 303:103644, 2022. URL: https://doi.org/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. In Proc. of the 31st Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 951-970, 2020. URL: https://doi.org/10.1137/1.9781611975994.57.
  4. Julien Baste, Ignasi Sau, and Dimitrios M. Thilikos. Hitting minors on bounded treewidth graphs. I. General upper bounds. SIAM Journal on Discrete Mathematics, 34(3):1623-1648, 2020. URL: https://doi.org/10.1137/19M1287146.
  5. Mikołaj Bojańczyk and Michał Pilipczuk. Definability equals recognizability for graphs of bounded treewidth. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 407-416, 2016. URL: https://doi.org/10.1145/2933575.2934508.
  6. Mikołaj Bojańczyk, Michał Pilipczuk, Wojciech Przybyszewski, Marek Sokołowski, and Giannos Stamoulis. Low rank MSO. CoRR, abs/2502.08476, 2025. URL: https://doi.org/10.48550/arXiv.2502.08476.
  7. Mikołaj Bojańczyk. Separator logic and star-free expressions for graphs. arXiv preprint arXiv:2107.13953, 2021. URL: https://arxiv.org/abs/2107.13953.
  8. É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 Proceedings of the 54th Annual ACM SIGACT Symposium on Theory of Computing (STOC), pages 924-937, 2022. URL: https://doi.org/10.1145/3519935.3520037.
  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. URL: https://doi.org/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 graph families. Algorithmica, 7(5-6):555-581, 1992. URL: https://doi.org/10.1007/BF01758777.
  11. Samuel Braunfeld, Jaroslav Nešetřil, Patrice Ossona de Mendez, and Sebastian Siebertz. Decomposition horizons and a characterization of stable hereditary classes of graphs. European Journal of Combinatorics, page 104130, 2025. Google Scholar
  12. Julia Chuzhoy and Zihan Tan. Towards tight(er) bounds for the Excluded Grid Theorem. Journal of Combinatorial Theory, Series B, 146:219-265, 2021. URL: https://doi.org/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. URL: https://doi.org/10.1016/0890-5401(90)90043-H.
  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. URL: https://doi.org/10.1051/ita/1992260302571.
  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. Google Scholar
  16. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press, 2012. Google Scholar
  17. Bruno Courcelle, Johann A. Makowsky, and Udi Rotics. Linear time solvable optimization problems on graphs of bounded clique-width. Theory of Computing Systems, 33(2):125-150, 2000. URL: https://doi.org/10.1007/S002249910009.
  18. Marek Cygan, Daniel Lokshtanov, Marcin Pilipczuk, Michał Pilipczuk, and Saket Saurabh. Minimum bisection is fixed-parameter tractable. SIAM Journal on Computing, 48(2):417-450, 2019. URL: https://doi.org/10.1137/140988553.
  19. 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. URL: https://doi.org/10.1109/LICS.2007.31.
  20. Rodney G. Downey and Michael R. Fellows. Fundamentals of Parameterized Complexity. Texts in Computer Science. Springer, 2013. URL: https://doi.org/10.1007/978-1-4471-5559-1.
  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. In 2024 IEEE 65th Annual Symposium on Foundations of Computer Science (FOCS), pages 21-30. IEEE, 2024. Google Scholar
  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. URL: https://doi.org/10.1145/3564246.3585186.
  23. Jan Dreier, Nikolas Mählmann, Sebastian Siebertz, and Szymon Toruńczyk. Indiscernibles and Flatness in Monadically Stable and Monadically NIP Classes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023), volume 261 of Leibniz International Proceedings in Informatics (LIPIcs), pages 125:1-125:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.125.
  24. Jan Dreier, Nikolas Mählmann, and Szymon Toruńczyk. Flip-breakability: A combinatorial dichotomy for monadically dependent graph classes. In Proceedings of the 56th Annual ACM Symposium on Theory of Computing, pages 1550-1560, 2024. URL: https://doi.org/10.1145/3618260.3649739.
  25. Jan Dreier and Peter Rossmanith. Approximate evaluation of first-order counting queries. In Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 1720-1739. SIAM, 2021. URL: https://doi.org/10.1137/1.9781611976465.104.
  26. Zdeněk Dvořák, Daniel Král, and Robin Thomas. Deciding first-order properties for sparse graphs. In Proceedings of the IEEE 51st Annual Symposium on Foundations of Computer Science (FOCS), pages 133-142. IEEE, 2010. Google Scholar
  27. 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. URL: https://doi.org/10.1145/2499483.
  28. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Springer Science & Business Media, 1999. Google Scholar
  29. 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. URL: https://doi.org/10.1016/j.jcss.2021.04.005.
  30. Fedor V. Fomin, Petr A. Golovach, Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. Compound logics for modification problems. ACM Transactions on Computational Logic, 26(1):1-57, 2025. URL: https://doi.org/10.1145/3696451.
  31. Markus Frick and Martin Grohe. Deciding first-order properties of locally tree-decomposable structures. Journal of the ACM, 48(6):1184-1206, 2001. URL: https://doi.org/10.1145/504794.504798.
  32. Jakub Gajarský, Nikolas Mählmann, Rose McCarty, Pierre Ohlmann, Michal Pilipczuk, Wojciech Przybyszewski, Sebastian Siebertz, Marek Sokolowski, and Szymon Torunczyk. Flipper games for monadically stable graph classes. In 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, volume 261 of LIPIcs, pages 128:1-128:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.128.
  33. Robert Ganian, Petr Hliněnỳ, Alexander Langer, Jan Obdržálek, Peter Rossmanith, and Somnath Sikdar. Lower bounds on the complexity of MSO₁ model-checking. Journal of Computer and System Sciences, 80(1):180-194, 2014. URL: https://doi.org/10.1016/J.JCSS.2013.07.005.
  34. 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. URL: https://doi.org/10.1137/1.9781611977554.ch141.
  35. Martin Grohe. Logic, graphs, and algorithms. Electronic Colloquium on Computational Complexity, TR07, 2007. Google Scholar
  36. 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. URL: https://doi.org/10.1007/978-3-540-92248-3_3.
  37. Martin Grohe, Ken-ichi Kawarabayashi, Dániel Marx, and Paul Wollan. Finding topological subgraphs is fixed-parameter tractable. In Proceedings of the 43rd ACM Symposium on Theory of Computing (STOC), pages 479-488. ACM, 2011. URL: https://doi.org/10.1145/1993636.1993700.
  38. 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. URL: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.395.8282.
  39. 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. URL: https://doi.org/10.1145/3051095.
  40. Martin Grohe and Nicole Schweikardt. First-order query evaluation with cardinality conditions. In Proceedings of the 37th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS), pages 253-266, 2018. URL: https://doi.org/10.1145/3196959.3196970.
  41. Jędrzej Hodor, Hoang La, Piotr Micek, and Clément Rambaud. Quickly excluding an apex-forest, 2025. URL: https://arxiv.org/abs/2404.17306.
  42. Bart M. P. Jansen and Céline M. F. Swennenhuis. Steiner Tree Parameterized by Multiway Cut and Even Less. In Proc. of the 32nd Annual European Symposium on Algorithms (ESA), volume 308 of LIPIcs, pages 76:1-76:16, 2024. URL: https://doi.org/10.4230/LIPIcs.ESA.2024.76.
  43. 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. Google Scholar
  44. Stephan Kreutzer and Siamak Tazari. Lower bounds for the complexity of monadic second-order logic. In Proceedings of the 2010 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 189-198. IEEE, 2010. URL: https://doi.org/10.1109/LICS.2010.39.
  45. Dietrich Kuske and Nicole Schweikardt. First-order logic with counting. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12. IEEE, 2017. URL: https://doi.org/10.1109/LICS.2017.8005133.
  46. Dietrich Kuske and Nicole Schweikardt. Gaifman normal forms for counting extensions of first-order logic. In Proceedings of the 45th International Colloquium on Automata, Languages, and Programming (ICALP), volume 107 of LIPIcs, pages 133:1-133:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.133.
  47. Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-07003-1.
  48. Daniel Marx, Paul Seymour, and Paul Wollan. Rooted grid minors. J. Combin. Theory Ser. B, 122:428-437, 2017. URL: https://doi.org/10.1016/j.jctb.2016.07.003.
  49. 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. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.102.
  50. Evangelos Protopapas, Dimitrios M. Thilikos, and Sebastian Wiederrecht. Colorful minors, 2025. URL: https://doi.org/10.48550/arXiv.2507.10467.
  51. Neil Robertson and Paul D. Seymour. Graph Minors. V. Excluding a planar graph. Journal of Combinatorial Theory, Series B, 41(2):92-114, 1986. URL: https://doi.org/10.1016/0095-8956(86)90030-4.
  52. Neil Robertson and Paul D. Seymour. Graph Minors. XIII. The Disjoint Paths Problem. Journal of Combinatorial Theory, Series B, 63(1):65-110, 1995. URL: https://doi.org/10.1006/jctb.1995.1006.
  53. Neil Robertson and Paul D. Seymour. Graph minors XXIII. Nash-williams' immersion conjecture. J. Comb. Theory, Ser. B, 100(2):181-205, 2010. URL: https://doi.org/10.1016/j.jctb.2009.07.003.
  54. Ignasi Sau, Nicole Schirrmacher, Sebastian Siebertz, Giannos Stamoulis, Dimitrios M. Thilikos, and Alexandre Vigny. Model checking for low monodimensionality fragments of CMSO on topological-minor-free graph classes, 2026. URL: https://arxiv.org/abs/2605.00192.
  55. Ignasi Sau, Giannos Stamoulis, and Dimitrios M. Thilikos. Parameterizing the quantification of CMSO: model checking on minor-closed graph classes. In Proc. of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms, (SODA), pages 3728-3742. SIAM, 2025. URL: https://doi.org/10.1137/1.9781611978322.124.
  56. 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, 2023. This is the full version of [Schirrmacher et al., 2024]. URL: https://doi.org/10.48550/arXiv.2302.07033.
  57. 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), pages 68:1-68:12. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662089.
  58. Nicole Schirrmacher, Sebastian Siebertz, and Alexandre Vigny. First-order logic with connectivity operators. ACM Transactions on Computational Logic, 24(4), 2023. URL: https://doi.org/10.1145/3595922.
  59. Detlef Seese. Linear time computable problems and first-order descriptions. Mathematical Structures in Computer Science, 6(6):505-526, 1996. URL: https://doi.org/10.1017/S0960129500070079.
  60. Sebastian Siebertz and Alexandre Vigny. Advances in algorithmic meta theorems (invited paper). In Siddharth Barman and Slawomir Lasota, editors, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2024, volume 323 of LIPIcs, pages 2:1-2:29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2024.2.
  61. Dimitrios M. Thilikos and Sebastian Wiederrecht. The graph minors structure theorem through bidimensionality, 2025. URL: https://arxiv.org/abs/2306.01724.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact