# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 4 A Partition-Refinement Algorithm for Probabilistic Bisimulation (Detailed)
### Marking  
Given a constellation \(C\) that contains a block \(B_{C}\) and in the case of an action transition, an action \(a\), we need to know which blocks need to be split in what way. This is calculated using the functions \(aMark(B,C,B_{C},a)\) and \(pMark(B,C,B_{C})\). The first one is for marking blocks with respect to action transitions, the second for marking blocks with respect to probabilities. Both functions yield a five-tuple \(\langle B,\mathit{left},\mathit{mid},\mathit{right},\mathit{and}\mathit{large}\rangle\). Here, \(B\subseteq\mathcal{B}\) is a set of blocks that may have to be split and _left_, _mid_, and _right_ are functions that together for each block \(B\in B\) provide the sets into which \(B\) must be partitioned. The set \(\mathit{large}(B)\) is the largest set among them. For every set \(B^{\prime}\) in which \(B\) must be partitioned, except for \(\mathit{large}(B)\), it holds that \(|B^{\prime}|\leqslant\frac{1}{2}|B|\). To obtain the complexity bound, we only move such small blocks out of \(B\), i.e., those blocks not equal to \(\mathit{large}(B)\). We note that sets in \(\mathit{left}(B)\), \(\mathit{mid}(B)\) and \(\mathit{right}(B)\) can be empty. Such sets can be ignored. It is also possible that there is only one non-empty set being equal to \(B\) itself. In this case, \(B\) is stable under \(B_{C}\) and \(C\backslash B_{C}\). Furthermore, it is equal to \(\mathit{large}(B)\) and therefore \(B\) is kept intact. We now concentrate on the function \(aMark(\mathcal{B},C,B_{C},a)\) with a partition \(\mathcal{B}\), a constellation \(C\), a block \(B_{C}\) contained in \(C\), and an action \(a\). In this situation, \(C\) is a non-trivial constellation of probabilistic states. Since \(C\) contains probabilistic states only, incoming transitions for states in \(B_{C}\) are action transitions. The situation is depicted in Figure 2, at the left. The call \(aMark(\mathcal{B},C,B_{C},a)\) returns the tuple \(\langle B_{a},\mathit{left}_{a},\mathit{mid}_{a},\mathit{right}_{a},\mathit{ right}_{a},\mathit{large}_{a}\rangle\) defined as follows. \[ \begin{array}{rcl}\boldsymbol{B}_{a}&=&\{\,B\in\mathcal{B}\mid\exists s\in B \colon s\xrightarrow{a}B_{C}\,\}\\ \text{and, for each }B\in\boldsymbol{B}_{a},\\ \mathit{left}_{a}(B)&=&\{\,s\in B\mid s\xrightarrow{a}B_{C}\wedge s \xrightarrow{a}C\backslash B_{C}\,\},\\ \mathit{mid}_{a}(B)&=&\{\,s\in B\mid s\xrightarrow{a}B_{C}\wedge s \xrightarrow{a}C\backslash B_{C}\,\},\\ \mathit{right}_{a}(B)&=&\{\,s\in B\mid s\xrightarrow{a}B_{C}\wedge s \xrightarrow{a}C\backslash B_{C}\,\},\text{ and}\\ \mathit{large}_{a}(B)&:&\text{the largest set among }\mathit{left}_{a}(B),\mathit{mid}_{a}(B), \mathit{and}\mathit{right}_{a}(B).\end{array} \]  
We calculate \(\boldsymbol{B}_{a}\) by traversing the list of all transitions with action \(a\) going into \(B_{C}\) and adding each block containing any source state of these transitions to \(\boldsymbol{B}_{a}\). The blocks in \(\boldsymbol{B}_{a}\) are the only blocks that may be unstable under \(B_{C}\) and \(C\backslash B_{C}\) with respect to \(a\) (Lemma 2). The for loop at Line 10 iterates over all actions. As the incoming transitions into block \(B_{C}\) are grouped per action, all incoming transitions with the same action can easily be processed together, while the total processing time is linear in the number of incoming transitions. However, note that calculating \(\boldsymbol{B}_{a}\) is based on partition \(\mathcal{B}\), while \(\mathcal{B}\) is refined at Line 14. Thus, the calculation of \(\boldsymbol{B}_{a}\) for different actions \(a\) can be based on repeatedly refined partitions \(\mathcal{B}\). Next, we discuss how to construct the blocks \(\mathit{left}_{a}(B)\), \(\mathit{mid}_{a}(B)\), and \(\mathit{right}_{a}(B)\). While traversing \(a\)-labelled transitions into \(B_{C}\), all action states in a block \(B\) with an \(a\)-transition into \(B_{C}\) are marked and (temporarily) moved into \(\mathit{left}_{a}(B)\). The remaining states in block \(B\) form the subset \(\mathit{right}_{a}(B)\).