New hope for epistemic reasoning in byzantine fault-tolerant distributed systems

Abstract

The epistemic approach to the study of various models of distributed systems has shown to be fruitful over the last three decades. In this talk, I will present some of the results in the area w.r.t. the byzantine fault-tolerant model. By extending Fagin et al.’s classic runs-and-systems framework, we have developed a comprehensive framework that also allows modelling misbehaviours of byzantine agents. In this extended framework, we prove the so-called Brain-in-a-Vat Lemma (formalizing the brain-in-a-vat scenario), one of our central results. In this talk we will take a closer look at this result to see how using its various knowledge limitations can be represented in the logical language. We will also take a look at some of our most recent results on the topic, one of them being an alternative axiomatization of the so-called hope modality that has been introduced in the context of epistemic analysis of byzantine fault-tolerant systems. We will see that, essentially, hope can be described using a standard KB4_n system. We will also see how we can combine KB4_n hope modalities with S5_n knowledge modalities in a joint logic enriched with both common hope and common knowledge. Interestingly, in the corresponding logics some of the main properties of the above-mentioned systems such as the bound on the maximal number of byzantine faulty agents and the brain-in-a-vat related properties become frame-characterizable.