Parameterizing the quantification of CMSO: model checking on minor-closed graph classes
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917706086744064 |
|---|---|
| author | Sau, Ignasi Stamoulis, Giannos Thilikos, Dimitrios M. |
| author_facet | Sau, Ignasi Stamoulis, Giannos Thilikos, Dimitrios M. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_18465 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Parameterizing the quantification of CMSO: model checking on minor-closed graph classes Sau, Ignasi Stamoulis, Giannos Thilikos, Dimitrios M. Logic in Computer Science Data Structures and Algorithms 5C85, 68R10, 05C75, 05C83, 05C75, 05C69 G.2.2; F.2.2 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. |
| title | Parameterizing the quantification of CMSO: model checking on minor-closed graph classes |
| topic | Logic in Computer Science Data Structures and Algorithms 5C85, 68R10, 05C75, 05C83, 05C75, 05C69 G.2.2; F.2.2 |
| url | https://arxiv.org/abs/2406.18465 |