Conference Papers Year : 2025

Parameterizing the quantification of CMSO: model checking on minor-closed graph classes

Ignasi Sau
Giannos Stamoulis

Abstract

Given a graph G and a vertex set X, the annotated treewidth tw(G, X) of X in G is the maximum treewidth of an X-rooted minor of G, i.e., a minor H where the model of each vertex of H contains some vertex of X. That way, tw(G, X) can be seen as a measure of the contribution of X to the tree-decomposability of G. We introduce the logic CMSO/tw as the fragment of monadic second-order logic on graphs obtained by restricting set quantification to sets of bounded annotated treewidth. We prove the following Algorithmic Meta-Theorem (AMT): for every non-trivial minor-closed graph class, model checking for CMSO/tw formulas can be done in quadratic time. Our proof works for the more general CMSO/tw+dp logic, that is CMSO/tw enhanced by disjoint-path predicates. Our AMT can be seen as an extension of Courcelle's theorem to minor-closed graph classes where the bounded-treewidth condition in the input graph is replaced by the bounded-treewidth quantification in the formulas. Our results yield, as special cases, all known AMTs whose combinatorial restriction is non-trivial minor-closedness.
Fichier principal
Vignette du fichier
SODA-2025.pdf (1) Télécharger le fichier
Origin Publisher files allowed on an open archive

Dates and versions

lirmm-04918933 , version 1 (29-01-2025)

Licence

Identifiers

Cite

Ignasi Sau, Giannos Stamoulis, Dimitrios M. Thilikos. Parameterizing the quantification of CMSO: model checking on minor-closed graph classes. SODA 2025 - 36th Annual ACM-SIAM Symposium on Discrete Algorithms, Jan 2025, New Orleans, United States. pp.403-445, ⟨10.1137/1.9781611978322.12⟩. ⟨lirmm-04918933⟩
0 View
0 Download

Altmetric

Share

More