Hope for Epistemic Reasoning with Faulty Agents!

In this paper, we study a new epistemic modal operator, termed hope, which has been introduced recently in the context of a novel epistemic reasoning framework for distributed multi-agent systems with arbitrarily (“byzantine”) faulty agents. It has been proved that both preconditions of actions used in agent protocols, as well as assertions about the epistemic states of agents obtained for analysis purposes, need to be restricted in a particular way for such systems. Hope has been proposed as the most promising candidate for analysis purposes, and defined in terms of the standard knowledge operator. To support the challenging next step of defining the semantics of common hope and eventual common hope, which are crucial for the analysis of fault-tolerant distributed agreement algorithms, we provide a suitable axiomatization of individual hope that avoids knowledge altogether, and prove its (strong) soundness and (strong) completeness.