# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 4 A Partition-Refinement Algorithm for Probabilistic Bisimulation (Detailed)
### Explanation of the Detailed Algorithm  
Algorithm 1 focuses on how, by refining partitions and sets of constellations, probabilistic bisimulation can be calculated. In Algorithm 2, we stress the details of carrying out concrete refinement steps to realise the required time bound. As already indicated, the overall structure of both algorithms is the same.  
The initial Lines 2 and 3 of Algorithm 2 are the same as those of Algorithm 1. In Line 3, the partition \(\mathcal{B}\) is set to contain one block with all probabilistic states and a number of blocks of action states, grouped per common outgoing action labels. Thus, two action states are in the same block initially if their menu, i.e., the set of actions for which there is a transition, is identical. This initial partition \(\mathcal{B}\) is calculated using a simple partition refinement algorithm on outgoing transitions of states. This operation is linear in the number of outgoing action transitions when using grouping of transitions as explained in Section 4.1.  
At Line 4, the incoming transitions are ordered on actions as indicated in Section 4.1. At Line 5, an array with one instance of _state_to_constellation_cnt_ for each action label is made where each instance contains the number of action transitions that contain that action label. The reference _state_to_constellation_cnt_ for each action transition is set to refer to the appropriate instance in this array. This is done by simply traversing all transitions \(s\stackrel{{ a}}{{\rightarrow}}u\) grouped by action labels and incrementing the appropriate entry in the array containing all _state_to_constellation_cnt_ variables. The appropriate entry can be found using the temporary variable _transition_cnt_ptr_ associated to state \(s\). If no entry for _state_to_constellation_cnt_ exists yet, the variable _transition_cnt_ptr_ belonging to \(s\) is _null_ and an appropriate entry must be created.  
In Line 6, selecting a non-trivial constellation is straightforward, as a stack of non-trivial constellations is maintained. Initially, this stack contains \(\mathcal{C}=\{\mathcal{S},\mathcal{U}\}\). To obtain the required time complexity, we select \(B_{C}\) such that \(|B_{C}|\leq\frac{1}{2}|C|\) in Line 7. This is done in constant time as we know the number of states in \(C\). Hence, either the first or second block \(B\) of constellation \(C\) satisfies that \(|B|\leq\frac{1}{2}|C|\) (for if the first block contains more than half the states the second one cannot). We replace the constellation \(C\) by \(B_{C}\) and \(C\backslash B_{C}\) in \(\mathcal{C}\), see Line 8, and put the constellation \(C\backslash B_{C}\) on the stack of non-trivial constellations if it is non-trivial.  
From Line 9 to Line 19, the partition \(\mathcal{B}\) is refined to restore the invariants, especially Invariant 3. This is done by first marking the blocks (Line 11 and Line 16) such that it is clear how they must be split, and by subsequently splitting the blocks (Lines 12-14, and Lines 17-19). Both operations are described in the next two subsections.