@article{prisco2000revisiting,
author = {Prisco, Roberto de and Lampson, Butler and Lynch, Nancy},
title = {Revisiting the Paxos Algorithm},
year = {2000},
month = {July},
abstract = {The Paxos algorithm is an efficient and highly fault-tolerant algorithm, devised by Lamport, for reaching consensus in a distributed system. Although it appears to be practical, it seems to be not widely known or understood. This paper contains a new presentation of the Paxos algorithm, based on a formal decomposition into several interacting components. It also contains a correctness proof and a time performance and fault-tolerance analysis.

The formal framework used for the presentation of the algorithm is provided by the Clock General Timed Automaton (Clock GTA) model. The Clock GTA provides a systematic way of describing timing-based systems in which there is a notion of “normal” timing behavior, but that do not necessarily always exhibit this “normal” timing behavior.

 },
url = {http://approjects.co.za/?big=en-us/research/publication/revisiting-paxos-algorithm/},
pages = {35-91},
journal = {Theoretical Computer Science},
volume = {243},
number = {1},
note = {A preliminary version appeared as Proc. WDAG'97, Lecture Notes in Computer Science 1320, Springer, 1997, pp 111-125},
}