# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 5 Benchmarks
To further understand the practical usability of the GRV algorithm, we applied it to a number of benchmarks taken from the PRISM Benchmark Suite (www.prismmodelchecker.org/benchmarks/) and the mCRL2 toolset (www.mcrl2.org/). The tests taken from PRISM were first translated into mCRL2 code to generate the corresponding PLTSs. Table 3 collects the results for the experiments conducted. The _ant_N_M_grid_ examples refer to the ant-on-a-grid puzzle for an \(N\) by \(M\) grid with the ant initially placed at the approximate center of the grid. The models _airplane_N_ are instances of an airplane ticket problem using \(N\) seats. In the airplane ticket problem, \(N\) passengers enter a plane. The first passenger lost his boarding pass and therefore takes a random seat. Each subsequent passenger will take his own seat unless it is already taken, in which case he randomly selects an empty seat as well. The intriguing question is to determine the probability that the last passenger will have his or her own seat (see [28] for a more detailed account). The following three benchmarks stem from PRISM: The _brp_N_MAX_ models are instances of the bounded retransmission protocol when transmitting \(N\) packages and bounding the number of retransmissions to _MAX_. The _self_stab_N_ and _shared_coin_N_K_ are extensions of the self stabilisation protocol and the shared coin protocol, respectively. For the self stabilisation protocol, \(N\) processes are involved in the protocol, each holding a token initially. The shared coin protocol is modelled using \(N\) processes and setting the threshold to decide _head_ or _tail_ to \(K\). Finally, the _random_N_ tests are randomly generated PLTSs with \(N\) action states. All the models are available in the mCRL2 toolset. At the left of Table 3, the characteristics for each PLTS are given: the number of action states (\(n_{a}\)), the number of action transitions (\(m_{a}\)), the number of distributions (\(n_{p}\)), and the cumulative support of the distributions (\(m_{p}\)). The symbol \"K\" is an indicator for 1000 states. The same characteristics for the minimised PLTS are also provided. Furthermore, the runtime for minimising the probabilistic transition system in seconds as well as the required memory in megabytes are indicated for both algorithms. As mentioned earlier, we limited the runtime to 5 h.  
Figure 5: Scaling of runtime results for the ant-on-a-grid puzzle  
The experiments show that the GRV algorithm outperforms the reference algorithm quite substantially in all studied cases. In the case of \"_random_100_\" the difference is four orders of magnitude, despite the fact that this state space has only 100 K action states. The second last column of Table 3 lists the relative speed-up, i.e. the quotient of the time needed by BEM over the time needed by GRV, when applicable. Memory usage is comparable for both algorithms for small cases, whereas for larger examples the BEM algorithm requires up to one order of magnitude more memory than the GRV algorithm. The right-most column of Table 3 contains the relative efficiency in memory, i.e. the quotient of the memory used by BEM over the memory used by GRV, for the cases where BEM terminated before the deadline.