TY - GEN
T1 - Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model
AU - Paul, Saswata
AU - Agha, Gul A.
AU - Patterson, Stacy
AU - Varela, Carlos A.
N1 - Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85111344343&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85111344343&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-76384-8_16
DO - 10.1007/978-3-030-76384-8_16
M3 - Conference contribution
AN - SCOPUS:85111344343
SN - 9783030763831
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 249
EP - 267
BT - NASA Formal Methods - 13th International Symposium, NFM 2021, Proceedings
A2 - Dutle, Aaron
A2 - Muñoz, César A.
A2 - Moscato, Mariano M.
A2 - Titolo, Laura
A2 - Perez, Ivan
PB - Springer
T2 - 13th International Symposium on NASA Formal Methods, NFM 2021
Y2 - 24 May 2021 through 28 May 2021
ER -