# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 3 A Partition Refinement Algorithm for Probabilistic Bisimulation (Outline)
### Outline of the Algorithm  
We present our algorithm in two stages. An abstract description of the algorithm is presented as Algorithm 1; the detailed algorithm is provided as Algorithm 2. The set-up of Algorithm 1 is a fairly standard, iterative refinement of a partition \(\mathcal{B}\), in this particular case containing both action states and probabilistic states, which are treated differently. In addition, following the approach of [PERSON] and [PERSON] [5], we maintain a coarser partition \(\mathcal{C}\), which we call the set of _constellations_. Each constellation in partition \(\mathcal{C}\) is a union of one or more blocks of \(\mathcal{B}\), thus \(\mathcal{B}\) is a refinement of \(\mathcal{C}\). A constellation \(C\in\mathcal{C}\) that consists of exactly one block in \(\mathcal{B}\) is called _trivial_. We refine partitions \(\mathcal{B}\) and \(\mathcal{C}\) until \(\mathcal{C}\) only contains trivial constellations (see Line 5 of Algorithm 1). ```
1:functionpartition-refinement
2:\(\mathcal{C}:=\setset{S,U}\)
3:\(\mathcal{B}:=\setset{U}\cup\setset{S_{A}}{A\subseteq Act}\)
4:where \(S_{A}=\setset{s\in S}{\forall a\in A\exists u\in U:s\stackrel{{ d}}{{\rightarrow}}u}\)
5:while\(\mathcal{C}\) contains a non-trivial constellation \(C\)do
6: choose block \(B_{C}\) from \(\mathcal{B}\) in \(\mathcal{C}\)
7: replace in \(\mathcal{C}\) constellation \(C\) by \(B_{\mathcal{C}}\) and \(C\backslash B_{C}\)
8:if\(C\) contains probabilistic states then
9:for all blocks \(B\) of action states in \(\mathcal{B}\) unstable under \(B_{C}\) or \(C\backslash B_{\mathcal{C}}\)do
10: refine \(\mathcal{B}\) by splitting \(B\) into blocks of states with the same actions into \(B_{C}\) and \(C\backslash B_{\mathcal{C}}\)
11:endfor
12:else
13:for all blocks \(B\) of probabilistic states in \(\mathcal{B}\) unstable under \(B_{\mathcal{C}}\)do
14: refine \(\mathcal{B}\) by splitting \(B\) into blocks of states with equal probabilities into \(B_{\mathcal{C}}\)
15:endfor
16:endif
17:endwhile
18:return\(\mathcal{B}\)
```  
**Algorithm 1** Abstract Partition Refinement Algorithm for Probabilistic Bisimulation. ```
1:functionpartition-refinement
2:\(\mathcal{C}:=\setset{S,U}\)
3:\(\mathcal{B}:=\setset{U}\cup\setsetset{S_{A}}{A\subseteq Act}\)
4:where \(S_{A}=\setset{s\in S}{\forall a\in A\exists u\in U:s\stackrel{{ d}}{{ \rightarrow}}u}\)
5:
6:endfor
7:while\(\mathcal{C}\) contains a non-trivial constellation \(C\)do
8: choose block \(B_{C}\) from \(\mathcal{B}\) in \(\mathcal{C}\)
9: replace in \(\mathcal{C}\) constellation \(C\) by \(B_{\mathcal{C}}\) and \(C\backslash B_{\mathcal{C}}\)
10:if\(C\) contains probabilistic states then
11:for all blocks \(B\) of action states in \(\mathcal{B}\) unstable under \(B_{C}\) or \(C\backslash B_{\mathcal{C}}\)do
12: refine \(\mathcal{B}\) by splitting \(B\) into blocks of states with the same actions into \(B_{C}\) and \(C\backslash B_{\mathcal{C}}\)
13:endfor
14:else
15:for all blocks \(B\) of probabilistic states in \(\mathcal{B}\) unstable under \(B_{\mathcal{C}}\)do
16: refine \(\mathcal{B}\) by splitting \(B\) into blocks of states with equal probabilities into \(B_{\mathcal{C}}\)
17:endfor
18:endif
19:endwhile
20:return\(\mathcal{B}\)
```  
**Algorithm 2** Partition Refinement Algorithm for Probabilistic Bisimulation. Among others, we preserve the invariant that the blocks in partition \(\mathcal{B}\) are always stable under partition \(\mathcal{C}\). If all constellations in \(\mathcal{C}\) are trivial, then the partitions \(\mathcal{B}\) and \(\mathcal{C}\) coincide. Hence, the blocks in \(\mathcal{B}\) are stable under itself, and according to Lemma 3 we have found a probabilistic bisimulation. Our algorithm works by iteratively refining the set of constellations \(\mathcal{C}\). When refining \(\mathcal{C}\), we must also refine \(\mathcal{B}\) to preserve the above mentioned invariant. Since the set of states of a PLTS is finite (cf. Definition 1) refinement of the partitions \(\mathcal{B}\) and \(\mathcal{C}\) cannot be repeated indefinitely.