TY - GEN
T1 - Distributed Model Checking on Graphs of Bounded Treedepth
AU - Fomin, Fedor V.
AU - Fraigniaud, Pierre
AU - Montealegre, Pedro
AU - Rapaport, Ivan
AU - Todinca, Ioan
N1 - Publisher Copyright:
© Fedor V. Fomin, Pierre Fraigniaud, Pedro Montealegre, Ivan Rapaport, and Ioan Todinca.
PY - 2024/10/24
Y1 - 2024/10/24
N2 - 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.
AB - 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.
KW - CONGEST model
KW - local computing
KW - proof-labeling schemes
UR - http://www.scopus.com/inward/record.url?scp=85208418576&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.DISC.2024.25
DO - 10.4230/LIPIcs.DISC.2024.25
M3 - Conference contribution
AN - SCOPUS:85208418576
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 38th International Symposium on Distributed Computing, DISC 2024
A2 - Alistarh, Dan
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 38th International Symposium on Distributed Computing, DISC 2024
Y2 - 28 October 2024 through 1 November 2024
ER -