Distributed Model Checking on Graphs of Bounded Treedepth

TL;DR

This work establishes a meta-theorem showing that every MSO property on graphs with bounded treedepth can be decided in a constant number of CONGEST rounds, via a distributed dynamic programming framework over elimination trees and w-terminal recursive graph representations. The approach yields a precise round bound of $O(2^{2\mathsf{td}(G)})$ for closed MSO formulas, and extends to MSO optimization and counting with a $g(\mathsf{td}(G),\varphi)$ round complexity, as well as to labeled graphs with minimal communication. It also provides a distributed construction of elimination trees in $O(2^{2d})$ rounds for graphs with $\mathsf{td}(G)\le d$, and demonstrates practical impact by applying the meta-theorem to $H$-freeness in graphs of bounded expansion in $O(\log n)$ rounds, including planar graphs. The results significantly advance distributed model checking by linking logical expressiveness to structure via treedepth, and generalize prior certification results while clarifying the boundaries of tractability in distributed decision on sparse graph classes.

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.

Figures (3)

• Figure 1: Embedding of a graph $G$ into a tree $T$ of depth 6.
• Figure 2: Paths as 2-terminal recursive graphs.
• Figure 3: Tree-decompositions: graphs $G_u$, $G^{=i}_u$ and $G^{\leq i}_u$

Theorems & Definitions (16)

• Definition 1: treedepth
• Lemma 2: NesetrilOdM12
• Definition 3: treewidth
• Lemma 4: canonical tree decomposition
• Lemma 5
• Definition 6: regular predicate
• Theorem 7: BoPaTo92
• Lemma 8: bottom-up decision
• Definition 9
• Lemma 10: bottom-up optimization