What Can Be Computed Locally Revisited: First-Order Logic on Sparse Graphs in Distributed Computing

TL;DR

This work reframes distributed locality through first-order logic (FO) on sparse graphs, focusing on bounded expansion classes and the CONGEST model. It shows that every local FO formula can be decided in $O( ext{log } n)$ rounds and every FO formula in $O(D+ ext{log } n)$ rounds on graphs of bounded expansion, by combining low-treedepth colorings, skeletons, and distributed quantifier elimination. The authors develop locality-preserving and controlled quantifier-elimination techniques to handle universal quantifiers and counting, extendable to counting, optimization, and distributed certification. They also establish tight lower bounds, demonstrating MSO cannot be incorporated in this framework and outlining the limitations on extending FO to bounded degeneracy and to MSO in planar/other sparse regimes. The results advance distributed meta-theorems for FO on sparse graphs and pave the way for practical certification schemes in distributed networks, with potential applications to subgraph testing, counting, and optimization tasks in planar and minor-free contexts.

Abstract

The question of 'what can be computed locally?' lies at the heart of distributed computing in networks. As established in Naor and Stockmeyer's seminal paper (STOC 1993), this question is undecidable, even for graph problems whose solutions can be checked locally. In this paper, we adopt a novel perspective on the question, by asking for which classes $Π$ of problems, and for which classes $\mathcal{G}$ of graphs, all problems in $Π$ can be solved efficiently in a distributed manner in all graphs of $\mathcal{G}$. This paper focuses on two natural candidates for such an approach, namely the class of problems expressible in first-order logic (FO), because of their intrinsic form of locality thanks to Gaifman's theorem, and the class of graphs with bounded expansion, because they form a large class of graphs encompassing, e.g., planar, bounded-treewidth, and bounded-degree graphs. The starting point of our work is the decade-old open question of Nešetřil and Ossona de Mendez (Distributed Computing 2016) on the distributed complexity of local FO formula on graphs of bounded expansion, in the standard CONGEST model of distributed computing. A formula $\varphi(x)$ is local if the satisfaction of $\varphi(x)$ depends only on the $r$-neighborhood of its free variable $x$, for some fixed $r$. For instance, the formula '$x$ belongs to a triangle' is local. We resolve the open problem positively by showing that, for every local FO formula $\varphi(x)$, and for every graph class $\mathcal{G}$ of bounded expansion, there exists a deterministic algorithm that identifies, for every $n$-vertex graph $G\in \mathcal{G}$, all vertices $v$ of $G$ such that $G\models \varphi(v)$, in $O(\log n)$ rounds. When dropping the locality condition, we show that $O(D+\log n)$ rounds are sufficient for deciding any FO formula $\varphi$ on graphs of bounded expansion.

Figures (4)

• Figure 1: Different classes of graphs, with their mutual inclusion relations. An arrow from a class $\mathcal{G}$ to a class $\mathcal{G}'$ indicates that $\mathcal{G}'$ is (strictly) included in $\mathcal{G}$.
• Figure 2: $F_{\xi^1_i}$ (left), $F_{\xi_i^2}$ (middle), and $F_{\xi^3_i}$ (right).
• Figure 3: Node gadget. In this figure is depicted the gadget for a node of degree $5$. Notice that in every proper three-coloring of the gadget the nodes $v_1, \dots, v_5$ receive the same colors. Conversely, if we color the nodes $v_1, \dots, v_5$ with the same color, we can extend the coloring into a three-coloring of all the nodes of the gadget.
• Figure 4: Crossing gadget. In every proper three-coloring of the gadget node label $x_1$ has the same color of node labeled $x_2$, as well as node labeled $y_1$ has the same color of $y_2$. Conversely, every three-coloring of $x_1, x_2, y_1$ and $y_2$ that assigns the same color to $x_1$ and $x_2$, and the same color to $y_1$ and $y_2$ can be extended into a three coloring of the gadget.

Theorems & Definitions (106)

• Proposition 1.2: Nešetřil and Ossona de Mendez NesetrilM16
• Theorem 1.4
• Theorem 1.5
• Theorem 1.6
• Theorem 1.7
• Theorem 1.8
• Definition 3.1
• Definition 3.2
• Definition 3.3
• Lemma 3.4