Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model
Abstract
Successfully attaining consensus in the absence of a centralized coordinator is a fundamental problem in distributed multi-agent systems. We analyze progress in the Synod consensus protocol -- which does not assume a unique leader -- under the assumptions of asynchronous communication and potential agent failures. We identify a set of sufficient conditions under which it is possible to guarantee that a set of agents will eventually attain consensus. First, a subset of the agents must behave correctly and not permanently fail until consensus is reached, and second, at least one proposal must be eventually uninterrupted by higher-numbered proposals. To formally reason about agent failures, we introduce a failure-aware actor model (FAM). Using FAM, we model the identified conditions and provide a formal proof of eventual progress in Synod. Our proof has been mechanically verified using the Athena proof assistant and, to the best of our knowledge, it is the first machine-checked proof of eventual progress in Synod.
Cite
@article{arxiv.2103.14576,
title = {Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model},
author = {Saswata Paul and Gul A. Agha and Stacy Patterson and Carlos A. Varela},
journal= {arXiv preprint arXiv:2103.14576},
year = {2021}
}
Comments
This technical report is an extended version of the NASA Formal Methods Symposium 2021 proceedings paper with the same name