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 $\Omega(n^2/\log n)$ on general $n$-vertex graphs (G\"o\"os, 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 $\Pi$ we give a LOCAL Certification protocol to certify that a graph satisfies $\Pi$ 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.

翻译：分布式网络易受错误影响，因此验证其输出至关重要。为此，我们针对图性质开发了LOCAL认证协议，其中节点被赋予证书，使其能够仅通过与局部网络的通信来检查整个网络是否满足某个固定性质。大多数已知的LOCAL认证协议是专门针对其处理问题设计的，无法更一般地推广。因此，我们致力于构建能够认证特定逻辑框架内可表达的任何性质的通用协议。我们考虑单子二阶逻辑（MSO$_2$），这是一个强大的框架，能够表达诸如非$k$可着色性、哈密顿性以及$H$子式自由性等性质。然而，一般而言，存在一些MSO$_2$可表达的性质，若无巨大证书则无法认证。例如，在一般的$n$顶点图上，非3可着色性需要大小为$\Omega(n^2/\log n)$的证书（Göös, Suomela 2016）。因此，我们对图施加额外的结构限制。我们提出了一个LOCAL认证协议，用于认证有界树宽图上任何MSO$_2$可表达的性质，并进而提出了一个用于认证有界树宽本身的LOCAL认证协议。即，对于每个整数$k$和每个MSO$_2$可表达的性质$\Pi$，我们给出一个LOCAL认证协议，使用大小为$\mathcal{O}(\log n)$（这是渐近最优的）的证书来认证一个图满足$\Pi$且树宽至多为$k$。我们的LOCAL认证协议仅需一轮分布式通信，因此它也是一个证明标记方案。我们的结果改进了Fraigniaud、Montealegre、Rapaport和Todinca（Algorithmica 2024）、Bousquet、Feuilloley、Pierron（PODC 2022）以及Baterisna和Chang的最新工作。