Multiagent Transition Systems for Composing Fault-Resilient Protocol Stacks

TL;DR

This paper introduces a mathematical framework using multiagent transition systems to specify, analyze, and compose fault-resilient distributed protocols, ensuring correctness and completeness in complex protocol stacks.

Contribution

It presents a novel formalism for fault-resilient protocol specification and analysis, including notions of safety, liveness, and completeness, with applications to blockchain and consensus protocols.

Findings

Framework successfully models fault resilience in distributed systems.

Applied to grassroots social networking and cryptocurrencies.

Enables compositional correctness proofs for protocol stacks.

Abstract

We present a novel mathematical framework for the specification and analysis of fault-resilient distributed protocols and their implementations, with the following components: 1. Transition systems that allow the specification and analysis of computations with safety and liveness faults and their fault resilience. 2. Notions of safe, live and complete implementations among transition systems and their composition, with which the correctness (safety and liveness) and completeness of a protocol stack as a whole follows from each protocol implementing correctly and completely the protocol above it in the stack. 3. Applying the notion of monotonicity, pertinent to histories of distributed computing systems, to ease the specification and proof of correctness of implementations among distributed computing systems. 4. Multiagent transition systems, further characterized as centralized/distributed and synchronous/asynchronous; safety and liveness fault-resilience of implementations among them and their composition. The framework is being employed in the specification of a grassroots ordering consensus protocol stack, with a grassroots dissemination protocol and its implementation of grassroots social networking and of sovereign cryptocurrencies, and an efficient Byzantine atomic broadcast protocols as initial applications.