Characterizing consensus in the Heard-Of model
Logic in Computer Science
2020-04-22 v1
Abstract
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.
Cite
@article{arxiv.2004.09621,
title = {Characterizing consensus in the Heard-Of model},
author = {A. R. Balasubramanian and Igor Walukiewicz},
journal= {arXiv preprint arXiv:2004.09621},
year = {2020}
}