Declarative distributed algorithms as axiomatic theories in three-valued modal logic over semitopologies

TL;DR

This paper demonstrates how to specify distributed algorithms declaratively using modal logic, enabling high-level reasoning and verification of protocols like broadcast and agreement.

Contribution

It introduces a novel modal logic-based axiomatic approach to specify distributed algorithms, facilitating correctness proofs and error detection.

Findings

Successfully specified protocols in modal logic

Found errors in an industrial protocol using the method

Formalized proofs in Lean 4

Abstract

We illustrate how to formally specify distributed algorithms as declarative axiomatic theories in a modal logic, using as illustrative examples a simple voting protocol, a simple broadcast protocol (Bracha Broadcast), and a simple agreement protocol (Crusader Agreement). The methods scale well and have been used to find errors in a proposed industrial protocol. The key novelty is to use modal logic to capture a declarative, high-level representation of essential system properties -- the logical essence of the algorithm -- while abstracting away from explicit state transitions of an abstract machine that implements it. It is like the difference between specifying code in a functional or logic programming language, versus specifying code in an imperative one. Thus we present axiomatisations of Declarative Bracha Broacast and Declarative Crusader Agreement. A logical axiomatisation in the style we propose provides a precise, compact, human-readable specification that abstractly captures essential system properties, while eliding low-level implementation details; it is more precise than a natural language description, yet more abstract than source code or a logical specification thereof. This creates new opportunities for reasoning about correctness, resilience, and failure, and could serve as a foundation for human- and machine verification efforts, design improvements, and even alternative protocol implementations. The proofs in this paper have been formalised in Lean 4.