What can be certified compactly? Compact local certification of MSO properties in tree-like graphs

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

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.