Multiagent Transition Systems with Faults: A Compositional Foundation for Distributed Computing

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 faults and their fault resilience. (2) A notion of correct implementations among transition systems and their composition, with which the correctness of a protocol stack as a whole follows from each protocol implementing correctly the protocol above it in the stack. (3) A notion of monotonicity, pertinent to histories of distributed computing systems, which eases the specification and proof of correctness of implementations among distributed computing systems. (4) The notion of fault-resilient implementations and their composition. (4) Multiagent transition systems, further characterized as centralized/distributed and synchronous/asynchronous. (5) An algebraic and operational characterization of the notion of grassroots composition of multiagent transition systems, which provides for the grassroots deployment of a distributed system, where instances deployed at different locations and at different times can interoperate once interconnected; and an algebraic characterization of when a family of asynchronous distributed multiagent transition systems is grassroots. Using the framework we prove the universality of a longest-chain protocol. The framework was also applied to the specification of the blocklace (partially-ordered generalization of the blockchain) protocol stack, a grassroots sovereign cryptocurrencies network.