Characterizing consensus in the Heard-Of model

2020/04/20 by Balasubramanian, A. R., Walukiewicz, Igor · 1 citation
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2004.09621

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.

Cited by

• Equivalence and Separation between Heard-Of and Asynchronous Message-Passing Models

Related

• Set-Consensus Collections are Decidable
• Derivation of Heard-Of Predicates From Elementary Behavioral Patterns
• Agreement Functions for Distributed Computing Models
• Consensus Needs Broadcast in Noiseless Models but can be Exponentially Easier in the Presence of Noise
• A Speedup Theorem for Asynchronous Computation with Applications to Consensus and Approximate Agreement