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. © 2014 Springer International Publishing.
CITATION STYLE
Gascón, A., & Tiwari, A. (2014). A synthesized algorithm for interactive consistency. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8430 LNCS, pp. 270–284). Springer Verlag. https://doi.org/10.1007/978-3-319-06200-6_23
Mendeley helps you to discover research relevant for your work.