On Distributed Model Checking of MSO on Graphs

TL;DR

This paper demonstrates that Monadic Second-Order logic (MSO) properties can be efficiently checked in distributed networks with specific topological constraints, using minimal communication per link.

Contribution

It introduces distributed algorithms for MSO model-checking on certain classes of graphs, leveraging transformations of sequential algorithms for tree decompositions.

Findings

MSO can be distributively model-checked with constant messages on planar networks with bounded diameter.

The approach applies to networks with bounded degree and bounded tree-length.

Distributed algorithms are based on transformations of linear time algorithms for tree decompositions.

Abstract

We consider distributed model-checking of Monadic Second-Order logic (MSO) on graphs which constitute the topology of communication networks. The graph is thus both the structure being checked and the system on which the distributed computation is performed. We prove that MSO can be distributively model-checked with only a constant number of messages sent over each link for planar networks with bounded diameter, as well as for networks with bounded degree and bounded tree-length. The distributed algorithms rely on nontrivial transformations of linear time sequential algorithms for tree decompositions of bounded tree-width graphs.