A Tight Meta-theorem for LOCAL Certification of MSO$_2$ Properties within Bounded Treewidth Graphs
Linda Cook, Eun Jung Kim, Tomáš Masařík
TL;DR
The paper establishes a tight, general LOCAL certification framework for any MSO$_2$-expressible property on graphs of bounded treewidth, achieving an $O(\log n)$-size proof labeling scheme in a single round. The approach combines locally verifiable treewidth via guidance systems and elimination trees with an MSO$_1$-based model-checking backbone, enabling local verification through compact evaluation trees and a bottom-up tree product. A key innovation is reducing MSO$_2$ certification to MSO$_1$ on graphs with bounded locally verifiable treewidth by universe expansion, followed by robust local certificates for the evaluation trees that witness correctness. The results improve prior bounds, connect to minor-closed property certifiability, and advance the practical viability of compact, one-round proofs for structural graph properties in distributed settings.
Abstract
Distributed networks are prone to errors so verifying their output is critical. Hence, we develop LOCAL certification protocols for graph properties in which nodes are given certificates that allow them to check whether their network as a whole satisfies some fixed property while only communicating with their local network. Most known LOCAL certification protocols are specifically tailored to the problem they work on and cannot be translated more generally. Thus we target general protocols that can certify any property expressible within a certain logical framework. We consider Monadic Second Order Logic (MSO$_2$), a powerful framework that can express properties such as non-$k$-colorability, Hamiltonicity, and $H$-minor-freeness. Unfortunately, in general, there are MSO$_2$-expressible properties that cannot be certified without huge certificates. For instance, non-3-colorability requires certificates of size $Ω(n^2/\log n)$ on general $n$-vertex graphs (Göös, Suomela 2016). Hence, we impose additional structural restrictions on the graph. We provide a LOCAL certification protocol for certifying any MSO$_2$-expressible property on graphs of bounded treewidth and, consequently, a LOCAL certification protocol for certifying bounded treewidth. That is for each integer $k$ and each MSO$_2$-expressible property $Π$ we give a LOCAL Certification protocol to certify that a graph satisfies $Π$ and has treewidth at most $k$ using certificates of size $\mathcal{O}(\log n)$ (which is asymptotically optimal). Our LOCAL certification protocol requires only one round of distributed communication, hence it is also proof-labeling scheme. Our result improves upon work by Fraigniaud, Montealegre, Rapaport, and Todinca (Algorithmica 2024), Bousquet, Feuilloley, Pierron (PODC 2022), and the very recent work of Baterisna and Chang.