What Can Be Computed Locally Revisited: First-Order Logic on Sparse Graphs in Distributed Computing
L\'elia Blin, Fedor V. Fomin, Pierre Fraigniaud, Sylvain Gay, Petr A. Golovach, Pedro Montealegre, Ivan Rapaport, Ioan Todinca

TL;DR
This paper investigates the local computability of first-order logic problems on sparse graphs within distributed networks, providing new algorithms with optimal round complexity for bounded expansion graph classes.
Contribution
It resolves an open problem by demonstrating efficient distributed algorithms for local FO formulas on bounded expansion graphs, with optimal round complexity.
Findings
Deterministic algorithms identify vertices satisfying local FO formulas in O(log n) rounds.
Deciding any FO formula on bounded expansion graphs takes O(D + log n) rounds.
The work advances understanding of local computation limits in distributed graph algorithms.
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 of graphs, all problems in can be solved efficiently in a distributed manner in all graphs of . 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.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Model-Driven Software Engineering Techniques · Petri Nets in System Modeling
