Rabin’s choice coordination problem studies the use of probability for breaking symmetry. In the model described here a group of six tourists must decide between two meeting places. However they may not communicate as a group. The protocol allows them to visit the two places alternatively, and to write numbers in their own notepad, and in the ones left outside the two places. The protocol eventually always terminates allowing the six tourists to meet at the same place, but we study the minimum probability that the tourists meet within a limited time of T steps.
The initial model has a parameter (BOUND) that limits its state-space. Using our SMC techniques we can set this parameter arbitrarily to 100, making the state-space of 5.10^6 intractable to numerical model-checking. Fortunately, it is possible to infer the correct probabilities from tractable parametrisations. The PLASMA Lab project that contains the example is available here.
Using the smart sampling algorithm and a Chernoff bound of epsilon=delta=0.01, we estimate the minimum probability for different values of T. We report the results in the table below. We noticed that for the values 24, 30, 32 that are closed to the probability threshold the analysis required a much greater budget to get better results. For 30 and 32 the precision is outside the precision 0.01 of the Chernoff bound, which can be explained by the rarity of the best scheduler.
| T | True probability (inferred) | Estimated probability | Simulation budget |
| 17 | 0.5 | 0.495 | 10^5 |
| 20 | 0.5 | 0.496 | 10^5 |
| 24 | 0.5 | 0.499 | 10^6 |
| 25 | 0.75 | 0.745 | 10^5 |
| 30 | 0.75 | 0.778 | 5.10^7 |
| 32 | 0.75 | 0.845 | 10^5 |
| 33 | 0.875 | 0.869 | 10^5 |
We also analyze this model with a BOUND of 100 for several values of the number of tourists. We compute the minimum number of rounds needed for the tourists to converge.
| Number of tourists | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 8 | 10 |
| Minimum number of rounds | 4.0 | 5.0 | 7.0 | 8.0 | 10.0 | 11.0 | 12.0 | 13.0 | 14.0 |
