Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Murdoch J. Gabbay, Luca Zanolini

TL;DR

The paper introduces Coalition Logic, a three-valued modal fixed-point framework for declaratively specifying distributed algorithms and deriving their correctness properties. Messages and explicit control flow are abstracted away, with semitopologies modeling quorums and three truth-values capturing normal, crashed, and faulty outcomes. Paxos is presented as a logical theory (TyPax) with backward and forward axioms encoding correctness and liveness, from which standard properties (validity, agreement, termination) are derived. A Simplified variant (TySPax) isolates the essential logical ingredients, demonstrating the framework's ability to reason about complex distributed protocols and guide declarative verification. The work highlights potential future extensions to more adversarial fault models and tooling to automate reasoning in Coalition Logic, with implications for robust protocol design in blockchains and other safety-critical distributed systems.

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.

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

TL;DR

The paper introduces Coalition Logic, a three-valued modal fixed-point framework for declaratively specifying distributed algorithms and deriving their correctness properties. Messages and explicit control flow are abstracted away, with semitopologies modeling quorums and three truth-values capturing normal, crashed, and faulty outcomes. Paxos is presented as a logical theory (TyPax) with backward and forward axioms encoding correctness and liveness, from which standard properties (validity, agreement, termination) are derived. A Simplified variant (TySPax) isolates the essential logical ingredients, demonstrating the framework's ability to reason about complex distributed protocols and guide declarative verification. The work highlights potential future extensions to more adversarial fault models and tooling to automate reasoning in Coalition Logic, with implications for robust protocol design in blockchains and other safety-critical distributed systems.

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.

Paper Structure

This paper contains 64 sections, 63 theorems, 82 equations, 11 figures.

Table of Contents

  1. Introduction
  2. Initial overview
  3. Motivation and background (further details)
  4. Structure of the paper
  5. Three truth-values
  6. Basic definition of ${\mathbf 3}$, and some truth-tables
  7. Valid and correct truth-values
  8. The rich implication and equivalence structure of ${\mathbf 3}$
  9. Weak and strong implications, and others
  10. Equivalence $\equiv$
  11. Coalition Logic
  12. A preliminary: semitopologies
  13. Syntax of the logic
  14. Denotation (semantics) of the syntax
  15. The fixedpoint operator $\mu \mathsf{X}$
  16. ...and 49 more sections

Key Result

Lemma 2.2.4

Suppose $\mathit{tv}\in{\mathbf 3}$ is a truth-value. Then:

Figures (11)

  • Figure 1: Truth-tables for some operations on ${\mathbf 3}$ (Remark \ref{['rmrk.three.elementary']})
  • Figure 2: Truth-tables for notions of equivalence (Definition \ref{['defn.equivalent']})
  • Figure 3: Term and predicate syntax of Coalition Logic (Definition \ref{['defn.predicate.syntax']})
  • Figure 4: Denotational semantics of Coalition Logic (Definition \ref{['defn.denotation']})
  • Figure 5: Derived syntactic sugar expressions (Definition \ref{['defn.3.derived']})
  • ...and 6 more figures

Theorems & Definitions (217)

  • Definition 2.1.1: Three-valued truth-values
  • Remark 2.1.2
  • Remark 2.1.3
  • Definition 2.2.1
  • Remark 2.2.2
  • Remark 2.2.3
  • Lemma 2.2.4
  • proof
  • Lemma 2.2.5
  • proof
  • ...and 207 more