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:

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].

• Two hop coloring protocol:

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.

• Orienting rings protocol:

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.

• Token circulation protocols:

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

1. CristiD. Angluin, J. Aspnes, M. J. Fischer, and H. Jiang. Self-stabilizing Population Protocols. In OPODIS, volume 3974 of LNCS, pages 103–117, 2005.
2. D. Angluin, J. Aspnes, M. J. Fischer, and H. Jiang. Self-stabilizing Population Protocols. ACM Transactions on Autonomous and Adaptive Systems, 3(4):643–644, 2008.
3. H. Jiang. Distributed Systems of Simple Interacting Agents. PhD thesis, Yale University, 2007.
4. Y. Liu, J. Pang, J. Sun, and J. H. Zhao. Verification of Population Ring Protocols in PAT. In TASE, pages 81–89. IEEE, 2009.