# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 5 Benchmarks  
Both our algorithm, below referred to as GRV, and the reference algorithm by [PERSON] [4], for which we use the abbreviation BEM, have been implemented in C++ as part of the mCRL2 toolset [9; 10] (www.mcrl2.org). This toolset is available under a Boost license which means that the source code is open and available without restriction to be inspected or used. In the implementation of BEM, some of the operations are not carried out exactly as prescribed in [4] for reasons of practicality. We have extensively tested the correctness of the implementation of the new algorithm by applying it to millions of randomly generated PLTSs, and comparing the results to those of the implementation of the BEM algorithm. This is not done because we doubt the correctness of the algorithm, but because we want to be sure that all the details of our implementation are right. We experimentally compared the performance of both implementations. All experiments have been performed on a relatively dated machine running Fedora 12 with INTEL XEON E5520 2.27 GHz CPUs and 1 TB RAM. For the probabilities exact rational number arithmetic is used which is much more time consuming than floating point arithmetic. The reported runtimes do not include the time to read the input PLTS and write the output. Our first experimental question regards the growth of the practical complexity of the BEM and GRV algorithm when concrete probabilistic transition systems grow in size. To get an impression of this, we considered the so-called \"ant on a grid\" puzzle published in the New York Times [27; 28]. In this puzzle, an ant sits on a square grid. When it reaches the leftmost or rightmost position on the grid it dies. When it reaches the upper or lower position of the grid it is free and lives happily ever after. On any remaining position, the ant chooses with equal probability to go to a neighbouring position on the grid. The question is what the probabilities for the ant are to die and stay alive, given an initial position on the grid. The specification in probabilistic mCRL2 of the ant-on-a-grid is given in Figure 4, where the dimensions of the grid are \(max_{x}\) and \(max_{y}\), and the initial position is given by \(i_{x}\) and \(i_{y}\). The actions _dead_, _live_ and _step_ indicate that the ant is dead, stays alive and makes a step. The process expression \(p\cdot q\) stands for sequential composition and \(p+q\) represents the choice in behaviour. The notations \(c\!\rightarrow\!p\) and \(c\!\rightarrow\!p\circ q\) are the if-then and if-then-else of mCRL2. The curly equal sign (\(\approx\)) in conditions stands for equality applied to data expressions. The expression \(\textbf{dist}\ d\cdot Direction[1/4]\) means that each direction \(d\) is chosen with probability \(\frac{1}{4}\). From this description, PLTSs are generated that are used as input for the probabilistic bisimulation reduction tools. Figure 4: The specification of ant-on-a-grid in mCRL2. Figure 5 depicts the runtime results of a set of experiments when increasing the total number of states of the ant on the grid model. At the left are the results when running the BEM algorithm, whereas the results for the GRV algorithm are shown at the right. Note that the \(x\)-axis only depicts the number of action states. This figure indicates that the practical running times of both algorithms are pretty much in line with the theoretical complexity. This is in agreement with our findings on other examples as well. Furthermore, it should be noted that the difference in performance is dramatic. The largest example that our implementation of the BEM algorithm can handle within a timeout of 5 h requires approximately 10,000 s compared to 2 s for GRV. The particular example regards a PLTS of 6.4\(\times 10^{5}\) action states. The graphs clearly indicate that the difference grows when the probabilistic transition systems get larger.