Local certification of MSO properties for bounded treedepth graphs

TL;DR

This paper demonstrates that Monadic Second-Order (MSO) properties can be locally certified with logarithmic bits per node in graphs of bounded treedepth, advancing distributed graph verification methods.

Contribution

It proves that any MSO property can be locally certified efficiently on bounded treedepth graphs, providing a significant theoretical result in distributed graph certification.

Findings

MSO properties are locally certifiable with logarithmic bits on bounded treedepth graphs

Certification is feasible for complex logical properties in restricted graph classes

The result extends the understanding of local certification limits in distributed computing.

Abstract

The graph model checking problem consists in testing whether an input graph satisfies a given logical formula. In this paper, we study this problem in a distributed setting, namely local certification. The goal is to assign labels to the nodes of a network to certify that some given property is satisfied, in such a way that the labels can be checked locally. We first investigate which properties can be locally certified with small certificates. Not surprisingly, this is almost never the case, except for not very expressive logic fragments. Following the steps of Courcelle-Grohe, we then look for meta-theorems explaining what happens when we parameterize the problem by some standard measures of how simple the graph classes are. In that direction, our main result states that any MSO formula can be locally certified on graphs with bounded treedepth with a logarithmic number of bits per node, which is the golden standard in certification.