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.

翻译：我们证明，在CONGEST模型中，每个关于有界树深图的一元二阶逻辑（MSO）公式可在常数轮内判定。据我们所知，这标志着关于分布式模型检验的首个元定理。图上的各种优化问题均可用MSO表达，例如：判定图$G$是否包含大小为$k$的团、是否允许$k$色染色、是否包含子图或子式$H$、或终端顶点能否通过顶点不相交路径相连。我们的元定理显著改进了Bousquet等人[PODC 2022]的工作，该工作聚焦于有界树深图上MSO的分布式验证。此外，我们的结果可扩展至求解有界树深图上可用MSO表达的优化与计数问题。