Nicolas Bousquet, Laurent Feuilloley, and Théo Pierron.

*PODC 2022: 41st ACM Symposium on Principles of Distributed Computing, July 25-29 2022, Salerno, Italy*

doi: 10.1145/3519270.3538416

Nicolas Bousquet, Laurent Feuilloley, and Théo Pierron.

doi: 10.1145/3519270.3538416

Local certification consists in assigning labels (called
*certificates*) to the nodes of a network to certify a property
of the network or the correctness of a data structure distributed on
the network.
The verification of this certification must be local: a node
typically sees only its neighbors in the network. The main measure
of performance of a certification is the size of its certificates.

In 2011, Göös and Suomela identified $\Theta(\log n)$ as a special
certificate size: below this threshold little is possible, and several
key properties do have certifications of this type.
A certification with such small certificates is now called a
*compact local certification*, and it has become the gold standard
of the area, similarly to polynomial time for centralized computing.
A major question is then to understand which properties have $O(\log n)$
certificates, or in other words: what is the power of compact local
certification?

Recently, a series of papers have proved that several well-known network properties have compact local certifications: planarity, bounded-genus, etc. But one would like to have more general results, \emph{i.e.} meta-theorems. In the analogue setting of polynomial-time centralized algorithms, a very fruitful approach has been to prove that restricted types of problems can be solved in polynomial time in graphs with restricted structures. These problems are typically those that can be expressed in some logic, and the graph structures are whose with bounded width or depth parameters. We take a similar approach and prove the first meta-theorems for local certification.

More precisely, the logic we use is MSO, the most classic fragment for logics on graphs, where one can quantify on vertices and sets of vertices, and consider adjacency between vertices. We prove the relevance of this choice in the context of local certification by first considering properties of trees. On trees, we prove that MSO properties can be certified with labels of constant size, whereas the typical non-MSO property of isomorphism requires $\tilde{O}(n)$ size certificates (where $\tilde{O}$ hides polylogarithmic factors). We then move on to graphs of bounded treedepth, a well-known parameter that basically measures how far a graph is from a star. We first prove that an optimal certification for bounded treedepth uses certificates of size $\Theta(\log n)$, and then prove that in bounded treedepth graphs, every MSO property has a compact certification.

To establish our results, we use a variety of techniques, originating from model checking, tree automata theory, communication complexity, and combinatorics.