Computer Science > Logic in Computer Science
[Submitted on 26 Jun 2024]
Title:Parameterizing the quantification of CMSO: model checking on minor-closed graph classes
View PDFAbstract: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.
Submission history
From: Dimitrios Thilikos [view email][v1] Wed, 26 Jun 2024 16:20:14 UTC (403 KB)
References & Citations
Bibliographic and Citation Tools
Bibliographic Explorer (What is the Explorer?)
Litmaps (What is Litmaps?)
scite Smart Citations (What are Smart Citations?)
Code, Data and Media Associated with this Article
CatalyzeX Code Finder for Papers (What is CatalyzeX?)
DagsHub (What is DagsHub?)
Gotit.pub (What is GotitPub?)
Papers with Code (What is Papers with Code?)
ScienceCast (What is ScienceCast?)
Demos
Recommenders and Search Tools
Influence Flower (What are Influence Flowers?)
Connected Papers (What is Connected Papers?)
CORE Recommender (What is CORE?)
arXivLabs: experimental projects with community collaborators
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.