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.

No additional funding sources recorded.