Distributed Model Checking on Graphs of Bounded Treedepth

TL;DR

This paper proves that monadic second-order logic properties on graphs with bounded treedepth can be decided in a constant number of rounds in the CONGEST model, establishing a new meta-theorem for distributed model-checking.

Contribution

It introduces the first meta-theorem for distributed model-checking of MSO logic on graphs with bounded treedepth, extending previous work on distributed certification.

Findings

Decidable in constant rounds in the CONGEST model

Applicable to various graph problems expressible in MSO

Extends to optimization and counting problems

Abstract

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.