We demonstrate how to formally specify distributed algorithms as declarative axiomatic theories in a modal logic. We exhibit the method on a simple voting protocol, a simple broadcast protocol, and a simple agreement protocol. 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 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. 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.

翻译：我们展示了如何将分布式算法形式化地表述为模态逻辑中的声明式公理化理论。我们通过一个简单的投票协议、一个简单的广播协议以及一个简单的共识协议来展示该方法。该方法具有良好的可扩展性，并已用于发现一个拟议工业协议中的错误。其核心创新在于利用模态逻辑来捕获系统基本属性的声明式高层表示——即算法的逻辑本质——同时抽象掉实现该算法的抽象机器的状态转移细节。这类似于用函数式或逻辑编程语言来规约代码，与用命令式语言规约代码之间的区别。我们提出的这种逻辑公理化风格提供了一种精确、紧凑、人类可读的规约，它抽象地捕获了系统的基本属性，同时省略了底层实现细节；它比自然语言描述更精确，又比源代码或其逻辑规约更抽象。这为推理正确性、弹性和故障创造了新的机会，并可作为人机验证工作、设计改进乃至替代协议实现的基础。