论文标题
表征在听觉模型中的共识
Characterizing consensus in the Heard-Of model
论文作者
论文摘要
听到的模型是分布式计算的简单且相对表达的模型。因此，它引起了验证社区的极大关注。我们给出了该模型片段中所有算法解决共识的表征。该片段足够大，可以涵盖许多突出的共识算法。表征纯粹是句法：它是根据算法文本的某些条件表示的。分布式算法验证的最新方法之一是将算法抽象到听觉模型，然后使用半自动过程验证抽象算法。在某些情况下，我们的结果允许避免这种方法的第二步。
The Heard-Of model is a simple and relatively expressive model of distributed computation. Because of this, it has gained a considerable attention of the verification community. We give a characterization of all algorithms solving consensus in a fragment of this model. The fragment is big enough to cover many prominent consensus algorithms. The characterization is purely syntactic: it is expressed in terms of some conditions on the text of the algorithm. One of the recent methods of verification of distributed algorithms is to abstract an algorithm to the Heard-Of model and then to verify the abstract algorithm using semi-automatic procedures. Our results allow, in some cases, to avoid the second step in this methodology.
