On the distributed evaluation of recursive queries over graphs

TL;DR

This paper explores the use of first-order and fixpoint logics for expressing and evaluating distributed graph functionalities, demonstrating their efficiency, translation into local rule programs, and robustness in various network settings.

Contribution

It introduces local fragments of these logics that enable efficient, bounded-message distributed evaluation while maintaining expressive power and robustness across network types.

Findings

FO and FP can be evaluated with polynomial messages of logarithmic size

Logical formulas can be translated into local rule programs for distributed computation

Local fragments have tighter bounds and are robust in various network models

Abstract

Logical formalisms such as first-order logic (FO) and fixpoint logic (FP) are well suited to express in a declarative manner fundamental graph functionalities required in distributed systems. We show that these logics constitute good abstractions for programming distributed systems as a whole, since they can be evaluated in a fully distributed manner with reasonable complexity upper-bounds. We first prove that FO and FP can be evaluated with a polynomial number of messages of logarithmic size. We then show that the (global) logical formulas can be translated into rule programs describing the local behavior of the nodes of the distributed system, which compute equivalent results. Finally, we introduce local fragments of these logics, which preserve as much as possible the locality of their distributed computation, while offering a rich expressive power for networking functionalities. We prove that they admit tighter upper-bounds with bounded number of messages of bounded size. Finally, we show that the semantics and the complexity of the local fragments are preserved over locally consistent networks as well as anonymous networks, thus showing the robustness of the proposed local logical formalisms.