Supplementary Materials for Combining State Space Reductions with Global Fairness Assumption
This is a supplementary page for the experiment in Combining State Space Reductions with Global Fairness Assumption. In the page, you can try the following:
For further information please contact Shao Jie Zhang.
Population Protocols
In the population protocol model, one protocol consists of N nodes, numbered from 0 to N-1. A protocol is usually described by a set of interaction rules between an initiator u and a responder v. Such rules have conditions on the state and the input of the initiator and the responder, and specify the state of the initiator and the responder if a transition can be taken. We introduce the models in the following. The complete protocol information can be found in [4].
The two hop coloring protocol in a ring network is proposed in [2]. It is a general algorithm that enables each node in a degree-bounded graph to distinguish between its neighbors. The graph is colored such that any two nodes adjacent to the same node have different colors. Two different versions are proposed in, one nondeterministic version and one deterministic version in [2]. We choose the nondeterministic one for the experiment.
The property states that, for each node v, if u and w are distinct neighbors of v, then u and w must have different colors. The protocol is designed with the assumption of global fairness.
Given a ring colored by the protocols above, it is possible to have a protocol that gives a sense of orientation to each node on an undirected ring in [2]. The orienting rings protocol is designed to guarantee two properties. Firstly, each node has exactly one predecessor and one successor, and the predecessor and successor of a node are different. Secondly, for any two nodes u and v, u is the predecessor of v if and only if v is the successor of u; for any edge (u, v), either u is the predecessor of v or v is the predecessor of u. The protocol is designed with the assumption of global fairness.
Two leader election protocols are used for experimentation in [2], [3]. One is for complete networks and the one is for oriented odd sized networks. The protocol is designed to guarantee that eventually always there is one and only one leader in the network. Note that for complete networks, counter representation is applicable since all network nodes are identical. The protocol for complete networks requires weak fairness only, whereas the one for oriented odd sized networks requires global fairness.
The token circulation protocol in directed rings is proposed in [1], [2]. Given a ring network, this protocol is designed to circulate a token fairly. The desired behavior of this protocol is that there is only one node which holds the token. The protocol is designed with the assumption of global fairness.
Experimental Results
We extend the PAT model checker with our algorithms for model checking with global fairness and symmetry reduction. The following table reports the performance on the above collection of population protocols. The experiment test bed is a server with 2.813GHz Intel Xeon 64-bit CPU and 32 GB memory. In the table, `-' means more than 3 hours. `States' in the table means the number of states stored (not the number of states visited), and `Gain' means the relative improvement on consumed time brought by symmetry reduction. We skip the statistics on memory consumption because the dynamic garbage collection facility in PAT makes the estimation inaccurate. Nonetheless, the number of states reflects the memory usage.
|
Models |
Network Size |
Without Reduction |
Without Reduction |
|||
|
States |
Time(Sec) |
States |
Time(Sec) |
Gain |
||
|
two-hop coloring |
3 |
122856 |
36.7 |
42182 |
16.7 |
54.5% |
|
orienting rings (prop1) |
3 |
19190 |
2.27 |
6398 |
0.53 |
76.7% |
|
orienting rings (prop2) |
3 |
19445 |
2.23 |
6503 |
0.97 |
56.5% |
|
orienting rings (prop1) |
4 |
1255754 |
267.2 |
313940 |
70.5 |
73.6% |
|
orienting rings (prop2) |
4 |
1206821 |
267.1 |
302071 |
63.6 |
79.6% |
|
orienting rings (prop1) |
5 |
11007542 |
9628.1 |
2201510 |
1067.4 |
88.9% |
|
orienting rings (prop2) |
5 |
10225849 |
8322.6 |
2045935 |
954.5 |
88.5% |
|
leader election (complete) |
3 |
6946 |
0.87 |
2419 |
0.51 |
41.4% |
|
leader election (complete) |
4 |
65468 |
11.6 |
16758 |
5.00 |
56.9% |
|
leader election (complete) |
5 |
598969 |
176.1 |
120021 |
45.9 |
73.9% |
|
leader election (odd) |
3 |
55100 |
6.27 |
18561 |
2.56 |
59.2% |
|
leader election (odd) |
5 |
------- |
------- |
6444097 |
5803.96 |
ᵪ |
|
token circulation |
3 |
728 |
0.12 |
244 |
0.09 |
25.0% |
|
token circulation |
4 |
4466 |
0.35 |
1118 |
0.19 |
45.7% |
|
token circulation |
5 |
24847 |
1.86 |
4971 |
0.77 |
58.6% |
|
token circulation |
6 |
129344 |
10.7 |
21559 |
3.03 |
71.7% |
|
token circulation |
7 |
643666 |
77.2 |
91954 |
16.2 |
79.0% |
|
token circulation |
8 |
3104594 |
740.8 |
388076 |
97.1 |
86.9% |
All models with configurable parameters have been embedded in the latest distribution of PAT, which is available from www.patroot.com .
Related Papers