Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Murdoch J. Gabbay

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.

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

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.
Paper Structure (44 sections, 26 theorems, 30 equations, 13 figures)

This paper contains 44 sections, 26 theorems, 30 equations, 13 figures.

Table of Contents

  1. Introduction
  2. Introducing the declarative, axiomatic approach
  3. Motivation: distributed algorithms
  4. Map of the paper
  5. Motivation and an illustrative example: voting
  6. Protocol description
  7. Three-valued logic
  8. Semitopologies
  9. 3-twined semitopologies
  10. Definition, discussion, and examples
  11. The fundamental logical characterisation of being 3-twined, and its corollaries
  12. A simple voting protocol
  13. The modal logic
  14. (Unique/affine) existence in three-valued logic
  15. A simple modal logic
  16. ...and 29 more sections

Key Result

Proposition 2.2.3

For truth-values $\mathit{tv},\mathit{tv}'\in{\mathbf 3}$, we have:

Figures (13)

  • Figure 1: Truth-tables for three-valued connectives on ${\mathbf 3}=\{{\mathbf t},{\mathbf b},{\mathbf f}\}$ (Definition \ref{['defn.THREE']}(\ref{['item.THREE.connectives']}))
  • Figure 2: Connectives derived from ${\pmb\neg}$, $\mathrel{\pmb\wedge}$, and $\mathsf{T}\space$ (Remark \ref{['rmrk.3.core']})
  • Figure 3: Specification of a simple voting protocol (Definition \ref{['defn.voting']})
  • Figure 4: Modalities (Definition \ref{['defn.semitopology.logic']})
  • Figure 6: Existence, affine existence, and unique existence (Definition \ref{['defn.unique.exist']})
  • ...and 8 more figures

Theorems & Definitions (81)

  • Example 2.1.1
  • Remark 2.1.2
  • Definition 2.2.1
  • Remark 2.2.2
  • Proposition 2.2.3
  • Definition 2.3.1
  • Definition 2.3.2
  • Lemma 2.3.3
  • Remark 2.3.4
  • Remark 2.3.5
  • ...and 71 more