# 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  
As we see from the high-level description of the partition refinement Algorithm 1, a non-trivial constellation \(C\) and a constituent block \(B_{C}\) are chosen (Lines 5 and 6) and \(C\) is replaced in \(\mathcal{C}\) by the smaller constellations \(B_{C}\) and \(C\setminus B_{C}\) (Line 7). This preserves Invariants 1 and 2, but Invariant 3 may be violated as stability under \(B_{C}\) or \(C\setminus B_{C}\) (or both) may be lost: On the one hand, it may be the case that two actions states \(s\) and \(t\) both have an \(a\)-transition into \(C\), but \(s\) may have one to \(B_{C}\) but \(t\) to \(C\setminus B_{C}\) only or vice versa. On the other hand, it may be the case that two probabilistic states \(u\) and \(v\) yield the same value for \(C\) as a whole, i.e. \(u[C]=v[C]\), but by no means this needs to hold for \(B_{C}\) or \(C\setminus B_{C}\), i.e. \(u[B_{C}]\
eq v[B_{C}]\) and \(u[C\setminus B_{C}]\
eq v[C\setminus B_{C}]\). Therefore, in the remainder of the body of Algorithm 1, the blocks that are unstable under \(B_{C}\) and \(C\setminus B_{C}\) are split such that Invariant 3 is restored, both for blocks of actions states (Lines 9 and 10) and for blocks of probabilistic states (Lines 13 and 14). In the next section, the detailed Algorithm 2 describes how this is done precisely. The general situation when splitting a block \(B\) for a constellation \(C\) containing a block \(B_{C}\) is depicted in Figure 2, at the left where \(B\) contains action states and at the right where \(B\) consists of probabilistic states. We first consider the case at the left. In this case, block \(B\subseteq S\) is stable under constellation \(C\subseteq U\) and \(C\) is non-trivial. Thus, \(C\) properly contains a block \(B_{C}\) of \(B\), and we distinguish two non-empty subsets of \(C\), the block \(B_{C}\) on its own and the remaining blocks together in \(C\setminus B_{C}\). As \(B\) is stable under \(C\), the block \(B\) can only be unstable under \(B_{C}\) or \(C\setminus B_{C}\) if there is an action \(a\in Act\) and a state \(s\in B\) such that \(s\xrightarrow{a}B_{C}\) (Lemma 2.1). Thus, we only investigate and split blocks, for which such a transition \(s\xrightarrow{a}B_{C}\) exists. We can restore stability by splitting \(B\) into the following three subsets:  
\[\mathit{left}_{a}(B) = \{\,s\in B\mid s\xrightarrow{a}B_{C}\wedge s\xrightarrow{a}C \setminus B_{C}\,\},\] \[\mathit{mid}_{a}(B) = \{\,s\in B\mid s\xrightarrow{a}B_{C}\wedge s\xrightarrow{a}C \setminus B_{C}\,\},\text{ and}\] \[\mathit{right}_{a}(B) = \{\,s\in B\mid s\xrightarrow{a}B_{C}\wedge s\xrightarrow{a}C \setminus B_{C}\,\}.\]  
Note that the remaining set \(\{\,s\in B\mid s\xrightarrow{a}B_{C}\wedge s\xrightarrow{a}C\setminus B_{C}\,\}\) must be empty; if not, this would imply that there is some action state \(t\) such that \(t\xrightarrow{a}C\). However, due to the existence of state \(s\) such that \(s\xrightarrow{a}B_{C}\), this would mean that block \(B\) is unstable under \(C\), contradicting Invariant 3. Figure 2: Splitting a non-stable block \(B\) into _left_, _middle_ and _right_. Checking that the sets \(\mathit{left}_{a}(B)\), \(\mathit{mid}_{a}(B)\), \(\mathit{right}_{a}(B)\) are stable under \(C\) is immediate. As subsets of stable sets are also stable (Lemma 1) and \(B\) is stable all other configurations of \(\mathcal{C}\), the sets \(\mathit{left}_{a}(B)\), \(\mathit{mid}_{a}(B)\), and \(\mathit{right}_{a}(B)\) are stable under all other configurations of \(\mathcal{C}\) too. Note that, due to the existence of state \(s\) with \(s\stackrel{{ a}}{{\rightarrow}}B_{C}\), it is not possible that both \(\mathit{left}_{a}(B)\) and \(\mathit{mid}_{a}(B)\) are equal to the empty set. It is however possible that \(\mathit{left}_{a}(B)=B\) or \(\mathit{mid}_{a}(B)=B\), leaving the other two sets empty. Lines 9 and 10 can now be read as follows.