# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 4 A Partition-Refinement Algorithm for Probabilistic Bisimulation (Detailed)
### Complexity Analysis
The space complexity follows as all data structures are linear in the number of transitions and states. As \(n_{p}\leqslant m_{p}\), this complexity can be stated as \(O\left(m_{a}+m_{p}+n_{a}\right)\). Note that it is reasonable that the number of probabilistic transitions \(m_{p}\) is at least equal to the number of action states \(n_{a}-1\) as otherwise there are unreachable action states. This allows formulating our complexity more compactly. Corollary 1: _Algorithm 2 has time complexity \(O\left((m_{a}+m_{p})\log n_{p}+m_{p}\log n_{a})\right)\) and space complexity \(O\left(m_{a}+m_{p}\right)\) if all action states are reachable._  
The only other algorithm to determine probabilistic bisimilarity for PLTS is by [PERSON], [PERSON] [4]. The algorithm uses extended ordered binary trees and is claimed to have a complexity of \(O\left(mn(\log m+\log n)\right)\) where \(m\) is the number of transitions (including distributions) and \(n\) the number of action states. For a fair comparison, we reconstructed their complexity in terms of \(n_{a}\), \(n_{p}\), \(m_{a}\) and \(m_{p}\). Their space complexity is \(O\left(n_{a}n_{p}|Act|\right)\) and the time complexity is \(O\left(m_{a}n_{a}\log n_{a}+n_{a}n_{p}\log n_{p}+n_{a}^{2}n_{p}\right)\). The last part \(n_{a}^{2}n_{p}\) is not mentioned in the analysis in [4]. It is due to taking the time into account for \"inserting \(Pre(\alpha,\mu_{i})\) into \(v.states\)\" (see page 208 of [4]) for the version of ordered balanced trees used, and we believe it to be forgotten [26]. This complexity is not easily comparable to ours. We make two reasonable assumptions to facilitate comparison. The first assumption is that the number of action transitions is equal to the number of distributions: \(m_{a}=n_{p}\). As second assumption, we use that \(\log n_{p}\) and \(\log n_{a}\) only differ by a constant. In the rare case that the support of distributions is large, i.e., if all or nearly all action states have a positive probability in each distribution, then \(m_{p}\) is equal or close to \(n_{a}n_{p}\). In this case our space complexity becomes \(O\left(n_{a}n_{p}\right)\) and our time complexity is \(O\left(n_{a}n_{p}\log n_{p}\right)\), which is comparable _mutatis mutandis_ to the complexity in [4]. However, in the more common case where the support of distributions is limited by some constant \(c\), i.e., \(m_{p}\leqslant cn_{p}\), we can simplify the space and time complexities to those in the following Table 2. \begin{table}
\begin{tabular}{l c c} \hline \hline  & **GRV** (this article) & **BEM**[4] \\ \hline
**Space complexity** & \(O\left(n_{p}\right)\) & \(O\left(n_{a}n_{p}|Act|\right)\) \\
**Time complexity** & \(O\left(n_{p}\log n_{a}\right)\) & \(O\left(n_{a}n_{p}\log n_{a}+\frac{n_{a}^{2}n_{p}}{a_{p}}\right)\) \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Space and time complexity of the GRV algorithm and the BEM algorithm. In the table the underlined part stems from the extra time needed for insertions. It is clear th,t if the assumptions mentioned are satisfied, the complexity of the present algorithm stands out well. This is confirmed in the next section where we report on the performance on a number of benchmarks of implementations of both algorithms.