Verification of Peterson's Algorithm for Leader Election in a Unidirectional Asynchronous Ring Using NuSMV

Amin Ansari

The finite intrinsic nature of the most distributed algorithms gives us this ability to use model checking tools for verification of this type of algorithms. In this paper, I attem…