A Sufficient Condition for Gaining Belief in Byzantine Fault-Tolerant Distributed Systems

At least since the ground-breaking work by Halpern and Moses [9], epistemic logic and interpreted runs and systems [6] are known as powerful tools for analyzing distributed systems. Distributed systems are multi-agent systems, where a set of n 2 agents, each executing some protocol, exchange messages in order to achieve some common goal. In the interpreted runs and systems framework, the set of all possible runs R (executions) of the agents in a system determines a set of Kripke models, formed by the evolution of the global state r(t) in all runs r I over time t N. Epistemic reasoning has been extended to fault-tolerant distributed systems right from the beginning, albeit restricted to benign faulty agents, i.e., agents that may only crash and/or drop messages [17, 18, 5, 9]. Actions performed by the agents when executing their protocol take place when they have accumulated specific epistemic knowledge.