This problem is based on the synchronous leader election protocol of Itai & Rodeh [IR90]. This protocol solves the following problem.
Given a synchronous ring of N processors design a protocol such that they will be able to elect a leader (a uniquely designated processor) by sending messages around the ring.
These models were taken from the Prism case studies here. A PLASMA Lab project file containing Leader Sync models and the property used for this experiment can be downloaded here.
We estimated the property of a leader being elected within L rounds. This property can be expressed in B-LTL as:
F<=#(L*(N+1)) “elected”
L is the number of rounds, N is the number of processors and “elected” is a RML label expressing the fact that one leader has been elected. Here are the results of our experiments for various values of L, N and K.
N=3
N=4
N=5
