A Synthesized Algorithm for Interactive Consistency

Adrià Gascón, Ashish Tiwari

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

Abstract

We revisit the interactive consistency problem introduced by Pease, Shostak and Lamport. We first show that their algorithm does not achieve interactive consistency if faults are transient, even if faults are non-malicious. We then present an algorithm that achieves interactive consistency in the presence of non-malicious, asymmetric and transient faults, but only under an additional guaranteed delayed ack assumption. We discovered our algorithm using an automated synthesis technique that is based on bounded model checking and QBF solving. Our synthesis technique is general and simple, and it is a promising approach for synthesizing distributed algorithms.
Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication6th International Symposium, NFM 2014, Houston, TX, USA, April 29 – May 1, 2014. Proceedings
EditorsJulia M. Badger, Kristin Yvonne Rozier
PublisherSpringer International Publishing
Pages270-284
Number of pages15
ISBN (Electronic)978-3-319-06200-6
ISBN (Print)978-3-319-06199-3
DOIs
Publication statusPublished - 2014

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume8430
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'A Synthesized Algorithm for Interactive Consistency'. Together they form a unique fingerprint.

Cite this