Abstract
In 1982 Dolev, et al. [10] presented an O(nlogn) unidirectional distributed algorithm for the circular extrema-finding (or leader-election) problem. At the same time Peterson came up with a nearly identical solution. In this paper, we bring the correctness of this algorithm to a completely formal level. This relatively small protocol, which can be described on half a page, requires a rather involved proof for guaranteeing that it behaves well in all possible circumstances. To our knowledge, this is one of the more advanced case-studies in formal verification based on process algebra.
| Original language | English |
|---|---|
| Pages (from-to) | 459-486 |
| Number of pages | 28 |
| Journal | Theoretical Computer Science |
| Volume | 177 |
| Issue number | 2 |
| DOIs | |
| Publication status | Published - 1997 |