Affordable Access

A Proof of a Leader Election Protocol in microCRL ($\mu$CRL)

Swedish Institute of Computer Science
Publication Date
  • Computer Science
  • Mathematics


In 1982 Dolev, Klawe & Rodeh presented an O(n log n) 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.

There are no comments yet on this publication. Be the first to share your thoughts.


Seen <100 times

More articles like this

New protocols for the election of a leader in a ri...

on Theoretical Computer Science Jan 01, 1987

Formal verification of a leader election protocol...

on Theoretical Computer Science Jan 01, 1997

State space generation for the HAVi leader electio...

on Science of Computer Programmin... Jan 01, 2002
More articles like this..