Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model

Saswata Paul, Gul A. Agha, Stacy Patterson, Carlos A. Varela

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationNASA Formal Methods - 13th International Symposium, NFM 2021, Proceedings
EditorsAaron Dutle, César A. Muñoz, Mariano M. Moscato, Laura Titolo, Ivan Perez
PublisherSpringer
Pages249-267
Number of pages19
ISBN (Print)9783030763831
DOIs
StatePublished - 2021
Event13th International Symposium on NASA Formal Methods, NFM 2021 - Virtual, Online
Duration: May 24 2021May 28 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12673 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference13th International Symposium on NASA Formal Methods, NFM 2021
CityVirtual, Online
Period5/24/215/28/21

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Verification of Eventual Consensus in Synod Using a Failure-Aware Actor Model'. Together they form a unique fingerprint.

Cite this