We present a novel mathematical framework for the specification, implementation and analysis of distributed computing systems, with the following novel components: (1) Transition systems with faults, which allow the specification and analysis of computations with safety and liveness faults and their fault resilience. (2) A notion of correct implementations among transition systems that requires both safety and liveness, and their composition, with which the correctness (safety and liveness) of a protocol stack as a whole follows from each protocol implementing correctly 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. (5) The notion of safety and liveness fault-resilient implementations and their composition. (6) An algebraic definition and operational characterization of the notion of a grassroots family of distributed multiagent transition systems, in which disjoint instances may be deployed independently at multiple locations and over time, and can subsequently interoperate once interconnected; sufficient condition for such a family to be grassroots; and a notion of a grassroots implementation of such a family. While new, the framework is being employed in the specification of a grassroots ordering consensus protocol stack, with sovereign cryptocurrencies, an NFT trade network, and an efficient Byzantine atomic broadcast protocol as the first applications.
View on arXiv