A declarative approach to specifying distributed algorithms using three-valued modal logic

TL;DR

This paper introduces Coalition Logic, a three-valued modal logic framework for declaratively specifying and verifying distributed algorithms like Paxos, emphasizing logical correctness without explicit message-passing modeling.

Contribution

It presents a novel three-valued modal logic framework for specifying distributed algorithms declaratively and demonstrates its application to Paxos for correctness verification.

Findings

Coalition Logic effectively models distributed algorithms.

The framework can derive correctness properties of Paxos.

Logical errors in algorithms can be identified within the framework.

Abstract

We present Coalition Logic, a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus algorithm. Our methodology represents a distributed algorithm as a logical theory, enabling correctness properties to be derived directly within the framework -- or revealing logical errors in the algorithm's design when they exist. Coalition Logic adopts a declarative approach, specifying the overall logic of computation without prescribing control flow. Notably, message-passing is not explicitly modeled, distinguishing our framework from approaches like TLA+. This abstraction emphasises the logical essence of distributed algorithms, offering a novel perspective on their specification and reasoning. We define the syntax and semantics of Coalition Logic, explore its theoretical properties, and demonstrate its applicability through a detailed treatment of the Paxos consensus algorithm. By presenting Paxos as a logical theory and deriving its standard correctness properties, we showcase the framework's capacity to handle non-trivial distributed systems. We envision Coalition Logic as a versatile tool for specifying and reasoning about distributed algorithms. The Paxos example highlights the framework's ability to capture intricate details, offering a new lens through which distributed algorithms can be specified, studied, and checked.