Byzantine agreement tasks have been studied extensively through many diverse frameworks ranging from epistemic modal logic to combinatorial, topological and even game theoretical approaches. Among byzantine agreement tasks, firing rebels with relay is of particular interest, since it is a basic primitive necessary for solving more complex tasks such as Consistent Broadcast. The epistemic logic approach has yielded both necessary conditions and sufficient knowledge conditions for solving firing rebels with relay. However, these conditions are stated in terms of knowledge and in principle do not explore the conditions on the communication structure which is often assumed to be complete. That is, any process is assumed to be capable of communicating with any other process at any time. In this paper, we characterize byzantine firing rebels solvability with and without relay in terms of the communication structure of the system. We define a relation between asynchronous message schedules and directed graph sequences, which we call network abstractions. This allows us to capture the message relay capabilities of the system into a combinatorial object. Although there are some similarities between network abstractions and causal cones, there is a fundamental difference. Namely, causal cones allow only to look at events in the past, while network abstractions allow us to reason about future possibilities. Thus enabling us to reason about liveness properties, which can not be expressed by looking only at past events. Furthermore, we formalize our characterization by using a temporal epistemic logic for byzantine systems. Such formulation constitutes the necessary and sufficient a-priori knowledge regarding network connectivity for solving firing rebels with relay.
翻译:拜占庭共识任务已通过多种不同框架得到广泛研究,涵盖从认知模态逻辑到组合、拓扑甚至博弈论方法。在拜占庭共识任务中,带中继的射击叛乱问题尤为引人关注,因为它是解决更复杂任务(如一致性广播)所需的基本原语。认知逻辑方法已推导出解决带中继射击叛乱问题的必要条件和充分知识条件。然而,这些条件是以知识形式表述的,原则上并未探讨通信结构上的条件——通常假设通信结构是完备的,即任意进程可在任何时刻与任意其他进程通信。本文从系统通信结构角度,刻画了有无中继情形下拜占庭射击叛乱问题的可解性。我们定义了异步消息调度与有向图序列之间的关联关系,并称之为网络抽象。这使得我们能将系统的消息中继能力捕捉为组合对象。尽管网络抽象与因果锥存在某些相似性,但存在根本差异:因果锥仅能考察过去事件,而网络抽象允许我们推理未来可能性。因此,它能支持我们论证活性性质——这类性质无法仅通过观察过去事件加以表达。此外,我们通过面向拜占庭系统的时间认知逻辑,将上述刻画形式化。该表述构成了解决带中继射击叛乱问题所需的关于网络连通性的先验知识之充要条件。