# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 4 A Partition-Refinement Algorithm for Probabilistic Bisimulation (Detailed)
### Marking
We keep track of the number of states in a block. Thus, we can easily maintain the size of \(\mathit{right}_{a}(B)\). To find out which states now in \(\mathit{left}_{a}(B)\) must be transferred to \(\mathit{mid}_{a}(B)\), the variables \(\mathit{state\_to\_constellation\_cnt}\) are used. Recall that these variables record for each transition \(s\xrightarrow{a}u\), with \(u\in S\), how many transitions \(s\xrightarrow{a}v\) there are to states \(v\in C\). These variables are initialised in Line 5 of Algorithm 2. When the first state is moved to \(\mathit{left}_{a}(B)\), we copy the value of \(\mathit{state\_to\_constellation\_cnt}\) of transition \(s\xrightarrow{a}u\) to the variable \(\mathit{residual\_transition\_cnt}\) belonging to state \(s\) of the transition, subtracted by one. The number \(\mathit{residual\_transition\_cnt}\) indicates how many unvisited \(a\)-transitions are left from the state \(s\) into \(C\). Every time an \(a\)-transition is visited of which the source state is already in \(\mathit{left}_{a}(B)\), we decrease \(\mathit{residual\_transition\_cnt}\) of the source state by one again. If all \(a\)-transitions into \(B_{C}\) have been visited, the number \(\mathit{residual\_transition\_cnt}\) of a state \(s\) indicates how many transitions labelled \(a\) go from \(s\) into \(C\backslash B_{C}\). Subsequently, we traverse the states in \(\mathit{left}_{a}(B)\). If a state \(s\) has a non-zero _residual_transition_cnt_, we know that there are \(a\)-transitions from \(s\) to both \(B_{C}\) and \(C\backslash B_{C}\). Therefore, we move state \(s\) into \(\mathit{mid}_{a}(B)\). Otherwise, all transitions from \(s\) with action \(a\) go to \(B_{C}\) and \(s\) must remain in \(\mathit{left}_{a}(B)\). While moving states into \(\mathit{left}_{a}(B)\) and \(\mathit{mid}_{a}(B)\), we also keep track of the sizes of these sets. Hence, it is easy to indicate in \(\mathit{large}_{a}(B)\) which set is the largest. We calculate \(\mathit{pMark}(\mathcal{B},C,B_{C})\) in a slightly different manner than \(\mathit{aMark}\). In particular, we have \(\mathit{mid}_{p}:\boldsymbol{B}\to 2^{2U}\), i.e., \(\mathit{mid}_{p}(B)\) is a set of blocks. This indicates that the block \(B\) can be partitioned in many sets, contrary to the situation with action blocks where \(B\) could be split in at most three blocks. The situation is depicted in Figure 2 at the right. The five-tuple that \(\mathit{pMark}\) returns has the following components:  
\[\boldsymbol{B}_{p} = \{\,B\in\mathcal{B}\mid\exists u\in B\colon u[B_{C}]>0\,\}\] \[\text{and, for each }B\in\boldsymbol{B}_{p},\] \[\mathit{left}_{p}(B) = \{\,u\in B\mid u[B_{C}]=1\,\},\] \[\mathit{mid}_{p}(B) = \{\,\{\,u\in B\mid u[B_{C}]=q\,\}\mid q\in\langle 0,1\,\}\,\},\] \[\mathit{right}_{p}(B) = \{\,u\in B\mid u[B_{C}]=0\,\},\text{ and}\] \[\mathit{large}_{p}(B) : \text{the largest set from }\{\mathit{left}_{p}(B)\}\cup\mathit{mid}_{p}(B)\cup\{ \mathit{right}_{p}(B)\}.\]  
The above is obtained by traversing through all incoming probabilistic transitions in \(B_{C}\). Whenever there is a state \(u\) in a block \(B\) such that \(u\mapsto_{p}B_{C}\), one of the following cases applies:  
* If \(B\) is not in \(\boldsymbol{B}_{p}\) yet, it is added now. The variable _cumulative_prob_ in state \(u\) is set to \(p\), and \(u\) is (temporarily) moved from \(B\) to \(\mathit{left}_{p}(B)\). * If \(B\) is already in \(\boldsymbol{B}_{p}\), then the probability \(p\) is added to _cumulative_prob_ of state \(u\). After the traversal of all incoming probabilistic transitions into \(B_{C}\), the variable _cumulative_prob_ of \(u\) contains \(u[B_{C}]\), i.e., the probability to reach \(B_{C}\) from the state \(u\). Those states that are left in \(B\) form the set \(\mathit{right}_{p}(B)\). We know the number of states in \(\mathit{right}_{p}(B)\) by keeping track how many states were moved to \(\mathit{left}_{p}(B)\). Next, the states temporarily stored in \(\mathit{left}_{p}(B)\) must be distributed over \(\mathit{left}_{p}(B)\) and \(\mathit{mid}_{p}(B)\).