Agents’ Knowledge and Its Limits in Byzantine Fault-Tolerant Distributed Systems

Abstract

In this thesis, we illustrate how (temporal-)epistemic logic can be applied to study byzantine fault-tolerant asynchronous message-passing distributed systems, in which agents may misbehave in an arbitrary (“byzantine”) way. Based on our framework for modeling such systems, we start by establishing what agents can always know and what agents can never know in the presence of byzantine faulty agents. Since, as we show, standard knowledge is not achievable by agents in most cases of interest, we explore how to best capture their epistemic states in various scenarios. On that journey, we encounter differ- ent epistemic modalities, in particular, the hope modality, and study them from a purely logical point of view. More precisely, we search for appropriate axiom- atizations (meaning, sound and complete axiomatizations) for the encountered epistemic modalities and investigate how they interact with each other. Our ultimate goal is gaining insight into agents’ decision-making process in byzan- tine fault-tolerant systems, however. Therefore, we use (temporal-)epistemic logic based on some of the newly introduced epistemic modalities to analyze a canonical distributed computing problem called Firing Rebels with Relay (FRR) within the byzantine faulttolerant asynchronous model. The FRR problem is, essentially, an agreement problem requiring that every correct agent performs an action called FIRE, in an all-or-none fashion (though not necessarily simul- taneously), and only if at least one correct agent locally observed a trigger event called START. It is well-known in the distributed computing community that, in case of benign faults (like the ones when agents just stop operating or lose messages), reaching agreement is connected with certain forms of standard common knowledge. Interestingly, it turns out that a temporal-epistemic group notion of hope, namely, common eventual hope, is at the heart of any solution of the FRR problem.