# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 3 A Partition Refinement Algorithm for Probabilistic Bisimulation (Outline)
### Refining the Set of Constellations and Restoring the Invariants
For all \(a\in Act\), investigate all blocks \(B\) such that there is an action state \(s\in B\) with \(s\stackrel{{ a}}{{\rightarrow}}B_{C}\) as these blocks are the only candidates to be unstable. Replace each such block \(B\) in \(\mathcal{B}\) by \(\{\mathit{left}_{a}(B)\), \(\mathit{mid}_{a}(B)\), \(\mathit{right}_{a}(B)\}\setminus\emptyset\) to restore stability under \(B_{C}\) and \(C\setminus B_{C}\). Invariants 1 and 2 are preserved by splitting \(B\). For Invariant 2, this is trivial by construction. For Invariant 1, note that the states in different blocks among \(\mathit{left}_{a}(B)\), \(\mathit{mid}_{a}(B)\), \(\mathit{right}_{a}(B)\) cannot be probabilistically bisimilar as they have unique transitions to states \(B_{C}\) and \(C\setminus B_{C}\) and these target states cannot be bisimilar by Invariant 1. Thus, if two states of \(B\) are probabilistically bisimilar then both are in the same subset \(\mathit{left}_{a}(B)\), \(\mathit{mid}_{a}(B)\), or \(\mathit{right}_{a}(B)\) of \(B\). We next turn to the case of a set of probabilistic states \(B\), see the right-side of Figure 2. Again, we assume that the non-trivial constellation \(C\) is replaced by its two non-empty subsets \(B_{C}\) and \(C\setminus B_{C}\). As in the previous case, although the block \(B\) is stable under the constellation \(C\), this may not be the case under the subsets \(B_{C}\) and \(C\setminus B_{C}\). To restore stability, we now consider for all \(q\), \(0\leqslant q\leqslant 1\), the sets  
\[B_{q} = \{\ u\in B\ |\ u[B_{C}]=q\ \}.\]  
Note that, for finitely many \(q\in[0,1]\), we have \(B_{q}\
eq\varnothing\). Observe that each set \(B_{q}\) is stable under \(B_{C}\) as by construction \(u[B_{C}]=v[B_{C}]=q\) for any \(u,v\in B_{q}\). The set \(B_{q}\) is also stable under \(C\setminus B_{C}\). To see this consider two states \(u,v\in B_{q}\). As block \(B\subseteq U\) is stable under constellation \(C\subseteq S\), \(u[C]=v[C]\). Hence, \(u[C\setminus B_{C}]=u[C]-u[B_{C}]=v[C]-v[B_{C}]=v[C\setminus B_{C}]\). By Lemma 1, the new blocks \(B_{q}\) are also stable under the other constellations in \(\mathcal{C}\). According to Lemma 2, only those blocks \(B\) that contain a probabilistic state \(u\in B\) such that \(u[B_{C}]>0\) can be unstable under \(B_{C}\) and \(C\setminus B_{C}\). Thus, at Line 13 of Algorithm 1 we consider all those blocks \(B\) and replace each of them by the non-empty subsets \(B_{q}\), \(0\leqslant q\leqslant 1\) at Line 14 in \(\mathcal{B}\). This makes the partition stable again under all constellations in \(\mathcal{C}\), in particular under the new constellations \(B_{C}\) and \(C\setminus B_{C}\). Again, it is straightforward to see that Invariants 1 and 2 are not violated by replacing the block \(B\) by the blocks \(B_{q}\). For Invariant 1, if states are probabilistically bisimilar in \(B\), they remain in the same block \(B_{q}\). For Invariant 2, as \(B\) is refined, partition \(\mathcal{B}\) remains a refinement of partition \(\mathcal{C}\). For the detailed algorithm in Section 4, it is required to group the sets \(B_{q}\) as follows: \(\mathit{left}_{p}(B):=B_{0}\), \(\mathit{right}_{p}(B):=B_{1}\), and \(\mathit{mid}_{p}(B)=\{\ B_{q}\ |\ 0{<}q{<}1\ \}\). This does not play a role here, but \(\mathit{left}_{p}(B)\), \(\mathit{mid}_{p}(B)\), and \(\mathit{right}_{p}(B)\) are already indicated in Figure 2, in particular \(\mathit{mid}_{p}(B)=\{B_{\frac{1}{4}},B_{\frac{1}{2}},B_{\frac{3}{4}}\}\).