Epistemic Reasoning with Byzantine-Faulty Agents

Abstract

We introduce a novel comprehensive framework for epistemic reasoning in multi-agent systems where agents may behave asynchronously and may be byzantine faulty. Extending Fagin et al.´s classic runs-and-systems framework to agents who may arbitrarily deviate from their protocols, it combines epistemic and temporal logic and incorporates fine-grained mechanisms for specifying distributed protocols and their behaviors. Besides our framework´s ability to express any type of faulty behavior, from fully byzantine to fully benign, it allows to specify arbitrary timing and synchronization properties. As a consequence, it can be adapted to any message-passing distributed computing model we are aware of, including synchronous processes and communication, (un-)reliable uni-/multi-/broadcast communication, and even coordinated action. The utility of our framework is demonstrated by formalizing the brain-in-a-vat scenario, which exposes the substantial limitations of what can be known by asynchronous agents in fault-tolerant distributed systems. Given the knowledge of preconditions principle, this restricts preconditions that error-prone agents can use in their protocols. In particular, it is usually necessary to relativize preconditions with respect to the correctness of the acting agent.