# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 3 A Partition Refinement Algorithm for Probabilistic Bisimulation (Outline)
### Stability of Blocks and Partitions  
An important notion underlying the algorithm introduced below is that of the stability of a block of a partition. If a block is not stable, it contains states that are not bisimilar. These states either have different transitions or different distributions. We first define the notion of stability more generically on sets instead of on blocks. Then, we lift it to partitions. Definition 3: (Stable Sets and Partitions). 1. _A set of action states_ \(B\subseteq S\) _is called stable under a set of probabilistic states_ \(C\subseteq U\) _with respect to an action_ \(a\in Act\) _iff_ \(s\xrightarrow{a}C\) _whenever_ \(t\xrightarrow{a}C\) _and vice versa for all_ \(s,t\in B\)_. The set_ \(B\) _is called stable under_ \(C\) _iff_ \(B\) _is stable under_ \(C\) _with respect to all actions_ \(a\in Act\)_._
2. _A set of probabilistic states_ \(B\subseteq U\) _is called stable under a set of action states_ \(C\subseteq S\) _iff_ \(u[C]=v[C]\) _for all_ \(u,v\in B\)_._
3. _A set of states_ \(B\) _with_ \(B\subseteq S\)_, respectively_ \(B\subseteq U\)_, is called stable under a partition_ \(\mathcal{C}\) _of_ \(S\cup U\)_, with_ \(C\subseteq S\) _or_ \(C\subseteq U\) _for all_ \(C\in\mathcal{C}\)_, iff_ \(B\) _is stable under each_ \(C\in\mathcal{C}\) _with_ \(C\subseteq U\)_, respectively_ \(C\subseteq S\)_._
4. _A partition_ \(\mathcal{B}\) _is called stable under a partition_ \(\mathcal{C}\) _iff all blocks_ \(B\) _of_ \(\mathcal{B}\) _are stable under_ \(\mathcal{C}\)_._  
There are two simple but important properties stating that stability is preserved when splitting sets. The first one says that subsets of stable sets are also stable. **Lemma 1**: _Let \(B\subseteq S\) be a set of action states and \(C\subseteq U\) a set of probabilistic states. If \(B\) is stable under \(C\), then any \(B^{\prime}\subseteq B\) is also stable under \(C\). Similarly, if \(C\) is stable under \(B\), then any \(C^{\prime}\subseteq C\) is also stable under \(B\)._  
We only prove the first part as the argument for the second part is essentially the same. If \(s,t\in B^{\prime}\), then also \(s,t\in B\). As \(B\) is stable under \(C\), it holds that for every action \(a\in Act\) either both satisfy \(s\stackrel{{ a}}{{\rightarrow}}C\) and \(t\stackrel{{ a}}{{\rightarrow}}C\), or neither does. Thus, \(B^{\prime}\) is stable under \(C\). The second property says that splitting a set in two parts can only influence the stability of an other set if there is a transition or a positive probability from this other set to one of the parts of the split set. **Lemma 2**: _Let \(B\subseteq S\) be a set of action states and \(C\subseteq U\) a set of probabilistic states._  
1. _Suppose_ \(B\) _is stable under_ \(C\) _with respect to an action_ \(a\)_,_ \(C^{\prime}\subseteq C\)_, and there is no_ \(s\in B\) _such that_ \(s\stackrel{{ a}}{{\rightarrow}}C^{\prime}\)_. Then,_ \(B\) _is stable under_ \(C^{\prime}\) _and_ \(C\backslash C^{\prime}\) _with respect to_ \(a\)_._
2. _Suppose_ \(C\) _is stable under_ \(B\)_,_ \(B^{\prime}\subseteq B\)_, and_ \(u[B^{\prime}]=0\) _for all_ \(u\in C\)_. Then,_ \(C\) _is stable under_ \(B^{\prime}\) _and_ \(B\backslash B^{\prime}\)_._  
We only provide the proof for the first part of this lemma. If \(s,t\in B\), then both \(s\stackrel{{ a}}{{\rightarrow}}C^{\prime}\) and \(t\stackrel{{ a}}{{\rightarrowrightarrow}}C^{\prime}\) by assumption. Thus, \(B\) is stable under \(C^{\prime}\) with respect to \(a\). Furthermore, \(B\) is stable under \(C\backslash C^{\prime}\): Suppose \(s,t\in B\) and \(s\stackrel{{ a}}{{\rightarrow}}C\backslash C^{\prime}\). Thus, \(s\stackrel{{ a}}{{\rightarrow}}C\). As \(B\) is stable under \(C\), \(t\stackrel{{ a}}{{\rightarrow}}C\), and by assumption \(t\stackrel{{ a}}{{\rightarrow}}C^{\prime}\). Therefore, \(t\stackrel{{ a}}{{\rightarrow}}C\backslash C^{\prime}\). Suppose \(s\stackrel{{ a}}{{\rightarrow}}C\backslash C^{\prime}\). Then, also \(s\stackrel{{ a}}{{\rightarrow}}C\).