Related publications: [KNP12a]
In this case study we consider a number of selfstabilising algorithms from the literature.
A selfstabilising protocol for a network of processes is a protocol which, when started from some possibly illegal start configuration, returns to a legal/stable configuration without any outside intervention within some finite number of steps. For further details on selfstabilisation see here.
In each of the protocols we consider, the network is a ring of identical processes. The stable configurations are those where there is exactly one process designated as "privileged" (has a token). This privilege (token) should be passed around the ring forever in a fair manner.
For each of the protocols, we compute the minimum probability of reaching a stable configuration and the maximum expected time (number of steps) to reach a stable configuration (given that the above probability is 1) over every possible initial configuration of the protocol.
The first protocol we consider is due to Herman [Her90]. The protocol operates synchronously, the ring is oriented, and communication is unidirectional in the ring. In this protocol the number of processes in the ring must be odd.
Each process in the ring has a local boolean variable xi, and there is a token in place i if xi=x(i1). In a basic step of the protocol, if the current values of xi and x(i1) are equal, then it makes a (uniform) random choice as to the next value of xi, and otherwise it sets it equal to the current value of x(i1).
By way of example, the PRISM source code for the case where there are three processes in the ring is given below.
// herman's self stabilising algorithm [Her90] // gxn/dxp 13/07/02 // the procotol is synchronous with no nondeterminism (a DTMC) dtmc const double p = 0.5; // module for process 1 module process1 // Boolean variable for process 1 x1 : [0..1]; [step] (x1=x3) > p : (x1'=0) + 1p : (x1'=1); [step] !(x1=x3) > (x1'=x3); endmodule // add further processes through renaming module process2 = process1 [ x1=x2, x3=x1 ] endmodule module process3 = process1 [ x1=x3, x3=x2 ] endmodule // cost  1 in each state (expected number of steps) rewards "steps" true : 1; endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) init true endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) formula num_tokens = (x1=x2?1:0)+(x2=x3?1:0)+(x3=x1?1:0); // label  stable configurations (1 token) label "stable" = num_tokens=1;
The table below shows statistics for protocol we have built for different numbers of processes (size of the ring). The first section gives the number of states and transitions in the DTMC representing the model. The second part refers to the MTBDD used to store it: the total number of nodes and the number of leaves (terminal nodes).
N:  Model:  MTBDD:  
States:  Transitions:  Nodes:  Leaves:  
3  8  28  24  3  
5  32  244  75  4  
7  128  2,188  158  5  
9  512  19,684  273  6  
11  2,048  177,148  420  7  
13  8,192  1,594,324  599  8  
15  32,768  14,348,908  810  9  
17  131,072  129,140,164  1,053  10  
19  524,288  1,162,261,468  1,328  11  
21  2,097,152  10,460,353,204  1,635  12 
We first check the correctness of the protocol, namely that:
We then study its performance, in particular:
For the latter, we consider the worstcase behaviour over all possible initial configurations and over all initial configurations with k tokens.
These properties can be expressed in PRISM as follows.
const int k; // number of tokens const int K; // number of steps // labels label "k_tokens" = num_tokens=k; // configurations with k tokens // From any configuration, a stable configuration is reached with probability 1 filter(forall, "init" => P>=1 [ F "stable" ]) // Maximum expected time to reach a stable configuration (for all configurations) R=? [ F "stable" {"init"}{max} ] // Maximum/minimum expected time to reach a stable configuration (for all ktoken configurations) R=? [ F "stable" {"k_tokens"}{max} ] R=? [ F "stable" {"k_tokens"}{min} ]
The minimum probability of reaching a stable state is 1 for all models built (up to N = 21).
The worstcase expected time, over all initial configurations, is shown in the plot below (marked "PRISM"). For comparison, we also plot the upper bound on this value proved by Kiefer et al. [KMO+11] of (approximately) 0.64N^{2}. As the graph illustrates, the actual worstcase value is considerably lower. Elsewhere, McIver and Morgan [MM05a] showed that the the worstcase time for initial configurations with 3 tokens is 4abc/N, where a, b and c are the distances between the three tokens. This therefore represents a lower bound on the worstcase expected time and is also shown in the plot. Kiefer, conjecture that this represents the worstcase for any number of tokens. Our results corroborate this conjecture precisely for all models built.
Further evidence of the correctness of McIver and Morgan's conjecture is shown in the graph below, where we plot, as k varies, the maximum expected time to reach a stable configuration given that the initial number of tokens equals k. As can be seen, for all models up to N = 21, the worst case is for k = 3 tokens and the maximum expected time decreases for increasing values of k.
Lastly, we examine the effect of the probabilistic value used for the random choice in Herman's algorithm (p in the PRISM code above).
As the plot below indicates, for values of N = 9 or below, p = 0.5 is the optimum value. However, interestingly, for larger values of N, this does not hold. In fact, in these case, values of p other than 0.5 (i.e. biased coins) result in better performance (lower expected execution time) for the protocol.
Moreover, zooming in on the above plots reveals unexpected trends for values of p close to 0.5:



See [KNP12a] for further results on this model.
The protocol we consider in this section is due to Israeli and Jalfon [IJ90]. It operates asynchronously with an arbitrary scheduler, the ring is oriented and communication is bidirectional in the ring.
Each process has a boolean variable qi which represents the fact that a token is in place i. A process is active if it has a token and only active processes can be scheduled. When an active process is scheduled, it makes a (uniform) random choice as to whether to move the token to its left or right. Note that if a process ends up with two tokens, these tokens are merged into a single token.
By way of example, the PRISM source code for the case where there are three processes in the ring is given below.
// IsraeliJalfon self stabilising algorithm // dxp/gxn 10/06/02 mdp // variables to represent whether a process has a token or not // note they are global because they can be updated by other processes global q1 : [0..1]; global q2 : [0..1]; global q3 : [0..1]; // module of process 1 module process1 [] (q1=1) > 0.5 : (q1'=0) & (q3'=1) + 0.5 : (q1'=0) & (q2'=1); endmodule // add further processes through renaming module process2 = process1 [ q1=q2, q2=q3, q3=q1 ] endmodule module process3 = process1 [ q1=q3, q2=q1, q3=q2 ] endmodule // cost  1 in each state (expected steps) rewards "steps" true : 1; endrewards // formula, for use here and in properties: number of tokens formula num_tokens = q1+q2+q3; // initial states (at least one token) init num_tokens >= 1 endinit
The table below shows statistics for protocol we have built for different numbers of processes (size of the ring). The first section gives the number of states in the MDP representing the model. The second part refers to the MTBDD which represents this MDP: the total number of nodes and the number of leaves (terminal nodes).
N:  Model:  MTBDD:  
States:  Nodes:  Leaves:  
3  7  48  3  
4  15  85  3  
5  31  129  3  
6  63  177  3  
7  127  229  3  
8  255  285  3  
9  511  345  3  
10  1,023  409  3  
11  2,047  477  3  
12  4,095  549  3  
13  8,191  625  3  
14  16,383  705  3  
15  32,767  789  3  
16  65,535  877  3  
17  131,071  969  3  
18  262,143  1,065  3  
19  524,287  1,165  3  
20  1,048,575  1,269  3  
21  2,097,151  1,377  3 
We analysed the protocol through the following properties.
Which can be expressed in PRISM as follows.
const int k; // number of tokens const int K; // number of steps // labels label "k_tokens" = num_tokens=k; // configurations with k tokens // From any configuration, a stable configuration is reached with probability 1 filter(forall, "init" => P>=1 [ F "stable" ]) // Maximum expected time to reach a stable configuration (for all configurations) Rmax=? [ F "stable" {"init"}{max} ] // Maximum/minimum expected time to reach a stable configuration (for all ktoken configurations) Rmax=? [ F "stable" {"k_tokens"}{max} ] Rmin=? [ F "stable" {"k_tokens"}{min} ] // Minimum probability reached a stable configuration within K steps (for all configurations) Pmin=? [ F<=K "stable" {"init"}{min} ]
The table below gives the model checking statistics when checking that from any configuration, a stable configuration is reached with probability 1 and calculating the maximum expected time to reach a stable configuration.
N:  A stable configuration is reached with probability 1  Maximum expected time to reach a stable configuration  
Iterations:  Result:  Iterations:  Result:  
3  3  true  21  3.0  
4  5  true  39  6.0  
5  7  true  61  10.0  
6  9  true  87  15.0  
7  12  true  116  21.0  
8  14  true  149  28.0  
9  16  true  186  36.0  
10  19  true  226  45.0  
11  23  true  270  55.0  
12  25  true  317  66.0  
13  28  true  367  78.0  
14  31  true  420  91.0  
15  35  true  477  105.0  
16  38  true  537  120.0  
17  41  true  599  136.0  
18  44  true  665  153.0  
19  48  true  733  171.0  
20  52  true  805  190.0  
21  55  true  879  210.0 
In all the cases considered, the configurations which achieve the maximum expected time are those where all the processes have tokens. To illustrate this fact, in the graph below we have plotted, as k varies, the maximum expected time to reach a stable configuration given that the initial number of tokens equals k.
In addition, below we have plotted the minimum expected time to reach a stable configuration given that the initial number of tokens k.
Lastly, we have also plotted the minimum probability of reaching a stable configuration within k steps.
Now we consider the selfstabilising protocol of Beauquier, Gradinariu and Johnen [BGJ99] for an arbitrary scheduler. It operates asynchronously, the ring is oriented, communication is unidirectional in the ring, and the number processes in the ring must be odd.
Each process two boolean variables: di and pi where:
The stable configurations are those where there is only one probabilistic token. A process is active if it has a deterministic token and only active processes can be scheduled. When an active process is scheduled, it sets di to be the negation of it current value (passes the deterministic token), and if it also has a probabilistic token, it makes a (uniform) random choice as to the next value of pi (randomly selects whether to pass the probabilistic token or not).
By way of example, the PRISM source code for the case where there are three processes in the ring is given below.
// self stabilisation algorithm Beauquier, Gradinariu and Johnen // gxn/dxp 18/07/02 mdp // module of process 1 module process1 d1 : bool; // probabilistic variable p1 : bool; // deterministic variable [] d1=d3 & p1=p3 > 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1); [] d1=d3 & !p1=p3 > (d1'=!d1); endmodule // add further processes through renaming module process2 = process1 [ p1=p2, p3=p1, d1=d2, d3=d1 ] endmodule module process3 = process1 [ p1=p3, p3=p2, d1=d3, d3=d2 ] endmodule // cost  1 in each state (expected steps) rewards "steps" true : 1; endrewards // initial states  any state with more than 1 token, that is all states init true endinit // formula, for use in properties: number of tokens formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p1?1:0);
The table below shows statistics for protocol we have built for different numbers of processes (size of the ring). The first section gives the number of states in the MDP representing the model. The second part refers to the MTBDD which represents this MDP: the total number of nodes and the number of leaves (terminal nodes).
N:  Model:  MTBDD:  
States:  Nodes:  Leaves:  
3  64  141  3  
5  1,024  336  3  
7  16,384  559  3  
9  262,144  810  3  
11  4,194,304  1,089  3 
The table below gives the model checking statistics when calculating, over all configurations, the minimum probability that a stable configuration is reached and the maximum expected time to reach a stable configuration.
N:  A stable configuration is reached with probability 1  Maximum expected time to reach a stable configuration  
Iterations:  Result:  Iterations:  Result:  
3  2  true  20  2.00  
5  8  true  64  11.9  
7  21  true  170  37.8  
9  40  true  380  84.4  
11  65  true  732  162 
In all the cases considered, the configurations which achieve the maximum expected time are those where only three processes have probabilistic tokens. To illustrate this fact, in the graph below we have plotted, as k varies, the maximum expected time to reach a stable configuration given that the initial number of tokens k.
In addition, below we have plotted the minimum expected time to reach a stable configuration given that the initial number of tokens equals k.
Lastly, we have also plotted the minimum probability of reaching a stable configuration within k steps.