# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 4 A Partition-Refinement Algorithm for Probabilistic Bisimulation (Detailed)
### Complexity Analysis  
The complexity of the algorithm is determined below. Recall that \(n_{a}\) and \(n_{p}\) are the number of action states and probabilistic states, respectively, while \(m_{a}\) is the number of action transitions and \(m_{p}\) is the cumulative size of the supports of the distributions. Theorem 4.2: _The total time complexity of the algorithm is \(O\left((m_{a}+m_{p})\log n_{p}+(m_{p}+n_{a})\log n_{a}\right)\) and the space complexity is \(O\left(m_{a}+m_{p}+n_{a}\right)\)._  
Proof. : In Algorithm 2, the cost of each computation step is indicated. The initialisation of the algorithm at Lines 2-5 is linear in \(n_{a}\), \(n_{p}\) and \(m_{a}\). At Line 3, calculating \(\{S_{A}\mid A\subseteq Act\}\) can be done by iteratively splitting \(S\) using the outgoing transitions grouped per action label. This is linear in the number of action transitions. At Line 4, grouping the incoming transitions per action is also linear as argued in Section 4.1. The while loop at Line 6 is executed for each \(B_{C}\subseteq C\) where \(|B_{C}|\leqslant\frac{1}{2}|C|\). As \(B_{C}\) becomes a constellation itself, each state can only be part of this splitting step \(\log_{2}(n_{a})\) times and \(\log_{2}(n_{p})\) times, respectively. The steps in Lines 10-13 and Lines 16-18 require steps proportional to the number of incoming action transitions and probabilistic transitions, respectively, in \(B_{C}\), apart from a sorting penalty which we treat separately below. The cumulative complexity of this part is therefore \(O\left(m_{a}\log n_{p}+m_{p}\log n_{a}\right)\). At Lines 14 and 19, the states in \(B^{\prime}\) are moved to a new block. This requires to group the incoming action transitions in a block \(B^{\prime}\) per action, which can be done in time linear in the number of these transitions. Block \(B^{\prime}\) is not the largest block of \(B\) considered and therefore \(|B^{\prime}|\leqslant\frac{1}{2}|B|\). Hence, each state can only be \(\log_{2}(n_{p})\) or \(\log_{2}(n_{a})\) times be involved in the operation to move to a new block. Hence, the total time to be attributed to moving is \(O\left((m_{a}+n_{p})\log n_{p}+(m_{p}+n_{a})\log n_{a}\right)\). While marking, probabilistic states in \(mid_{p}(B)\) need to be sorted. An ingenious argument by [PERSON] and [PERSON] [6] shows that this will at most contribute \(O\left(m_{p}\log n_{p}\right)\) to the total complexity: Let \(K\) be the total number of times sorting takes place. Assume, for \(1\leqslant i\leqslant K\), that the total number of distributions in \(mid_{p}(B)\) when sorting it for the \(i\)-th time is \(k_{i}\). Clearly, \(k_{i}\leqslant n_{p}\). Each time a distribution in \(mid_{p}(B)\) is involved in sorting, the number of reachable constellations with non-zero probability from this distribution is increased by one. Before sorting it could reach \(C\), and after sorting it can reach both new constellations \(B_{C}\) and \(C\backslash B_{C}\) with non-zero probability. Note that this does not hold for the states in \(left_{p}(B)\) and \(right_{p}(B)\), and this is the reason why we have to treat them separately. In particular, to obtain complexity \(O(m_{p}\log n_{p})\), it is not allowed to involve the states in \(left_{p}(B)\) and \(right_{p}(B)\) in the sorting process as shown by an example in [6]. Due to the increased number of reachable constellations, the total number of times a probabilistic state can be involved in sorting is bounded by the size of the distribution. In other words, \(\sum_{i=1}^{K}\,k_{i}\leqslant m_{p}\). Hence, the total time that is required by sorting is bounded as follows:  
\[O\left(\sum_{i=1}^{K}\,k_{i}\log k_{i}\right)\ \leqslant\ O\left(\sum_{i=1}^{K}\,k_{i} \log n_{p}\right)\ \leqslant\ O\left(m_{p}\log n_{p}\right).\]  
Adding up the complexities leads to the conclusion that the total complexity of the algorithm is \(O\left((m_{a}+m_{p}+n_{p})\log n_{p}+(m_{p}+n_{a})\log n_{a}\right)\). As \(m_{p}\geqslant n_{p}\), the stated time complexity in the theorem follows.