Distributed Model Checking on Graphs of Bounded Treedepth
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911868224798720 |
|---|---|
| author | Fomin, Fedor V. Fraigniaud, Pierre Montealegre, Pedro Rapaport, Ivan Todinca, Ioan |
| author_facet | Fomin, Fedor V. Fraigniaud, Pierre Montealegre, Pedro Rapaport, Ivan Todinca, Ioan |
| contents | We establish that every monadic second-order logic (MSO) formula on graphs with bounded treedepth is decidable in a constant number of rounds within the CONGEST model. To our knowledge, this marks the first meta-theorem regarding distributed model-checking. Various optimization problems on graphs are expressible in MSO. Examples include determining whether a graph $G$ has a clique of size $k$, whether it admits a coloring with $k$ colors, whether it contains a graph $H$ as a subgraph or minor, or whether terminal vertices in $G$ could be connected via vertex-disjoint paths. Our meta-theorem significantly enhances the work of Bousquet et al. [PODC 2022], which was focused on distributed certification of MSO on graphs with bounded treedepth. Moreover, our results can be extended to solving optimization and counting problems expressible in MSO, in graphs of bounded treedepth. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_03321 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Distributed Model Checking on Graphs of Bounded Treedepth Fomin, Fedor V. Fraigniaud, Pierre Montealegre, Pedro Rapaport, Ivan Todinca, Ioan Data Structures and Algorithms We establish that every monadic second-order logic (MSO) formula on graphs with bounded treedepth is decidable in a constant number of rounds within the CONGEST model. To our knowledge, this marks the first meta-theorem regarding distributed model-checking. Various optimization problems on graphs are expressible in MSO. Examples include determining whether a graph $G$ has a clique of size $k$, whether it admits a coloring with $k$ colors, whether it contains a graph $H$ as a subgraph or minor, or whether terminal vertices in $G$ could be connected via vertex-disjoint paths. Our meta-theorem significantly enhances the work of Bousquet et al. [PODC 2022], which was focused on distributed certification of MSO on graphs with bounded treedepth. Moreover, our results can be extended to solving optimization and counting problems expressible in MSO, in graphs of bounded treedepth. |
| title | Distributed Model Checking on Graphs of Bounded Treedepth |
| topic | Data Structures and Algorithms |
| url | https://arxiv.org/abs/2405.03321 |