Reasoning about Knowledge in Byzantine Distributed Systems

Reasoning about fault-tolerant distributed systems, which consist of networked processors without a central control that need to achieve a common goal, is notoriously difficult due to the many sources of uncertainty: varying execution speeds, unpredictable transmission delays, and partial failures make it difficult for a processor to establish local knowledge sufficient to safely perform required actions. The design and analysis of distributed algorithms is, hence, a difficult and error-prone task, which has to be done manually, on a case-by-case basis. A suitable abstraction that is both 1. high-level enough to facilitate the design of new algorithms and 2. rigorous and formal enough to form the basis of future tools does not exist today. Like in automated formal verification, one of the mandatory prerequisites for automated reasoning and decision making in multi-agent systems are precise logical languages for specifying algorithms, behaviors, and properties. Rather than just resorting to classic temporal logic languages such as LTL or CTL, which contributed much to the tremendous success of model checking approaches, we will explore the suitability of epistemic logic for this purpose. Very little is known about modeling and analysis of multi-agent systems where agents may be arbitrarily ("byzantine") faulty, and about the evolution of knowledge of the agents, i.e., learning, in the course of the information exchange caused by complex protocols. The goal of the proposed project is to close the above gaps by incorporating arbitrarily misbehaving agents into an epistemic reasoning framework and by supplementing the standard Kripke semantics with a suitable topological semantics for distributed systems, while exploiting, and being informed by, the success of Dynamic Epistemic Logic in capturing the dynamics of knowledge evolution in modal logic.

The project was devoted to reasoning about fault-tolerant distributed systems, which consist of networked processors without a central control that need to achieve a common goal. The two main methods applied were logical methods that explore the necessary and sufficient knowledge for distributed agents to be able to achieve the specified common goal and topological methods that encode the distributed configurations and protocols via appropriate topological objects, for instance simplicial complexes, and characterize the solvability of the common goal in topological terms. On the logical side, using the formalism of epistemic modal logic, the first epistemic framework encompassing fully byzantine agents has been used to show that even correct agents cannot rely on their own correctness, necessitating the decision-making to be based on the notion of belief, which is weaker than knowledge and represents knowledge modulo own correctness. At the same time, the informational content of messages in the presence of byzantine agents has been shown to require an even weaker modality of hope, reflecting the recipient's uncertainty about the reliability of the sender. Since both correctness and belief can be expressed in terms of knowledge and hope, byzantine distributed systems can be described in a logical language containing two modalities per agent, knowledge and hope. Common goals involving coordinated actions require appropriate fixpoint versions of these modalities. For instance, the epistemic analysis of the simplified version of the widely used consistent broadcasting primitive has led to the eventual common hope as the necessary condition. Dynamic versions of these logics have also been explored with self-correction of agents implemented by updating the state of the hope modality on an agent-by-agent basis. The role of a priori knowledge, both of the system designer and of the agents, in designing distributed systems has been explored both philosophically and logically. In particular, a way for agents to resolve inconsistencies by independently and autonomously updating their own a priori beliefs has been developed in the style of dynamic epistemic logic. On the topological side, combinatorial and topological modeling of consensus under oblivious message adversaries has been provided and a particularly interesting generalization of the celebrated Asynchronous Computability Theorem to continuous tasks has been achieved. Finally, at the intersection of logic and topology, the logic of simplicial complexes for distributed systems with crashes has been developed, providing a more agent-centric perspective and allowing for a more nuanced representation of the knowledge of both crashed agents and of active agents about crashed agents, with a possible third truth value "undefined".