# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 3 A Partition Refinement Algorithm for Probabilistic Bisimulation (Outline)
### An Example  
We provide an example to illustrate how Algorithm 1 calculates partitions. **Example 1**. : _Consider the PLTS given in Figure 3. We provide a detailed account of the partitions that are obtained when calculating probabilistic bisimulation. The obtained partitions are listed in Table 1. In the lower table, nine partitions together with their constellations are listed that are generated for a run of Algorithm 1. In the upper table the blocks that occur in these partitions are defined. Observe that we put the blocks and constellations with action states and probabilistic states in different columns. This is only for clarity, as in the current partition and the current set of constellations they are joined._Algorithm 1 starts with four blocks of action states, \(S_{0}\) to \(S_{3}\), which contain the action states with no outgoing transitions and those with an outgoing transition labelled with \(a\), with \(b\), and with \(c\), respectively. In the algorithm, all probabilistic states are initially collected in block \(U_{0}\). There are two constellations, viz. \(S_{0}\cup S_{1}\cup S_{2}\cup S_{3}\) and \(U_{0}\). These initial partitions are listed in R0w 0 of the lower part of Table 1.  
Since the constellation with action states is non-trivial we split it, rather arbitrarily, in \(S_{0}\) and \(S_{1}\cup S_{2}\cup S_{3}\). The block \(U_{0}\) is not stable under \(S_{0}\) and \(S_{1}\cup S_{2}\cup S_{3}\) and is split in \(U_{1}=\{u_{1},u_{3},v_{1-5}\}\), \(U_{2}=\{u_{2},u_{4}\}\) and \(U_{3}=\{u_{5},u_{6}\}\). This is because we have \(u[S_{0}]=1\) for \(u\) equal to \(u_{1}\), \(u_{3}\), and \(v_{1}\) to \(v_{5}\); we have \(u[S_{0}]=\frac{1}{2}\) for \(u\) equal to \(u_{2}\) and \(u_{4}\); we have \(u_{5}[S_{0}]=0\) and \(u_{6}[S_{0}]=0\). The resulting partitions are listed at Row 1 in Table 1.  
For the second iteration, we consider the non-trivial constellation \(S_{1}\cup S_{2}\cup S_{3}\) and split it into \(S_{1}\) and \(S_{2}\cup S_{3}\). Note, the action states \(s_{1}\) to \(s_{4}\) in \(S_{1}\) do not have incoming transitions. Consequently, for all \(u\in U_{1}\), we have \(u[S_{1}]=0\); for all \(u\in U_{2}\) we have \(u[S_{1}]=0\); for all \(u\in U_{3}\) we have \(u[S_{1}]=0\). Thus, all blocks of probabilistic states are stable under \(S_{1}\) and \(S_{2}\cup S_{3}\). Hence, no block is split. In the third iteration, we split the non-trivial constellation \(S_{2}\cup S_{3}\) into \(S_{2}\) and \(S_{3}\). For all, \(u\in U_{1}\) we have \(u[S_{2}]=0\). Thus, \(U_{1}\) is stable under \(S_{2}\) and \(S_{3}\). For \(U_{2}\), the probabilistic states \(u_{2}\) and \(u_{4}\) agree on the value \(\frac{1}{2}\) for \(S_{2}\), hence for \(S_{3}\) too. Thus, \(U_{2}\) is stable as well. However, for \(u_{5}\) and \(u_{6}\) in \(U_{3}\) we have \(u_{5}[S_{2}]=1\) and \(u_{6}[S_{2}]=\frac{1}{3}\). Therefore, \(U_{1}\) needs to be split in \(U_{4}=\{u_{5}\}\) and \(U_{5}=\{u_{6}\}\). At this point, all constellations with actions states are trivial, so at iteration 4 we turn to the non-trivial constellation of probabilistic states \(U_{1}\cup U_{2}\cup U_{4}\cup U_{5}\) and split it into \(U_{1}\) and \(U_{2}\cup U_{4}\cup U_{5}\). Block \(S_{0}\) is stable since each of its states has no transitions at all. Block \(S_{1}\) is not stable: \(s_{1},s_{2}\overset{a}{\rightarrow}U_{1}\) and \(s_{1},s_{2}\overset{a}{\rightarrow}U_{2}\cup U_{4}\cup U_{5}\), but \(s_{3},s_{4}\overset{a}{\rightarrow}U_{1}\) and \(s_{3},s_{4}\overset{a}{\rightarrow}U_{2}\cup U_{4}\cup U_{5}\). Thus, \(S_{1}\) needs to be split into \(S_{4}=\{s_{1},s_{2}\}\) and \(S_{5}=\{s_{3},s_{4}\}\). Block \(S_{2}\) is stable since its states have only \(b\)-transitions into \(U_{1}\). Block \(S_{3}\) is a singleton and therefore cannot be split. The following iteration, Iteration 5, sets \(U_{2}\) and \(U_{4}\cup U_{5}\) apart as constellations. Again, in absence of transitions, block \(S_{0}\) is stable under \(U_{2}\) and \(U_{4}\cup U_{5}\). The same holds for \(S_{2}\) that has only \(b\)-transitions into \(U_{0}\).