# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 3 A Partition Refinement Algorithm for Probabilistic Bisimulation (Outline)
### Outline of the Algorithm
Thus, termination of the algorithm is guaranteed. The partition consisting of singletons of action states and of probabilistic states is the finest that can be obtained, but this is only possible if all states are not bisimilar. In practice, the main loop of the algorithm stops well before reaching that point. The algorithm maintains the following three invariants:  
**Invariant 1**. : Probabilistic bisimilarity \(\simeq_{p}\) is a refinement of \(\mathcal{B}\). **Invariant 2**. : Partition \(\mathcal{B}\) is a refinement of partition \(\mathcal{C}\). **Invariant 3**. : Partition \(\mathcal{B}\) is stable under the set of constellations \(\mathcal{C}\) (mentioned already above). Invariant 1 states that if two action states or two probabilistic states are probabilistically bisimilar, then they are in the same block of partition \(\mathcal{B}\). Thus, the partition-refinement algorithm will not separate states if they are bisimilar. By Invariant 2, we have that, at the end and at the start of each iteration, each constellation in \(\mathcal{C}\) is a union of blocks in \(\mathcal{B}\). Invariant 3 says that blocks in partition \(\mathcal{B}\) cannot be split by blocks in constellation \(\mathcal{C}\). In Lines 2 and 3 of Algorithm 1, the set of constellation and the initial partition are set such that the invariants hold. All probabilistic states are put in one block, and all action states with exactly the same actions labelling outgoing transitions are also put together in blocks. (Note the universal quantification over all actions \(a\) in \(A\) for the set comprehension at Line 4 to ensure that only maximal blocks are included in \(\mathcal{B}\) for it being a partition indeed.) The set of constellations contains two constellations namely one with all action states, and one with all probabilistic states. It is straightforward to see that Invariants 1 and 2 hold. Invariant 3 is valid because all transitions from action states go to probabilistic states and vice versa. Invariants 1-3 guarantee correctness of Algorithm 1. That is, from the invariants, it follows that, upon termination, when all constellations have become trivial, the computed partition \(\mathcal{B}\) identifies probabilistically bisimilar action states and probabilistically bisimilar probabilistic states. **Theorem 1**. : _Consider the partition \(\mathcal{B}\) resulting from Algorithm 1. We find that (i) two action states are in the same block of \(\mathcal{B}\) iff they are probabilistically bisimilar, and (ii) two probabilistic states are in the same block of \(\mathcal{B}\) iff they are probabilistically bisimilar._  
Proof. : Upon termination, because of the while loop of Algorithm 1, all constellations of \(\mathcal{C}\) are trivial, i.e. each constellation in \(\mathcal{C}\) consists of exactly one block of \(\mathcal{B}\). Hence, by Invariant 2, the partitions \(\mathcal{B}\) and \(\mathcal{C}\) coincide. Thus, by Invariant 3, each block of \(\mathcal{B}\) is stable under each block in \(\mathcal{B}\). In other words, partition \(\mathcal{B}\) is stable under itself. By the Stability Property of Lemma 3, we have that \(\mathcal{B}\) is a probabilistic bisimulation on \(S\). It follows that two action states in the same block of \(\mathcal{B}\) are probabilistically bisimilar. Reversely, by Invariant 1, probabilistically bisimilar action states are in the same block of \(\mathcal{B}\). Thus, \(\simeq_{p}\) and \(\mathcal{B}\) coincide on \(S\). In other words, two action states are in the same block of \(\mathcal{B}\) iff they are probabilistically bisimilar. To compare \(\simeq_{p}\) and the relation \(\mathcal{B}\) on \(U\), choose probabilistic states \(u,v\in U\) such that \(u\,\mathcal{B}\,v\). Thus, \(u\) and \(v\) are in the same block of \(\mathcal{B}\). By stability of block \(B\) for \(\mathcal{B}\) it follows that \(u[B^{\prime}]=v[B^{\prime}]\), for each block \(B^{\prime}\subseteq S\). Since \(\simeq_{p}\) and \(\mathcal{B}\) coincide on \(S\) this implies \(u[B^{\prime}]=v[B^{\prime}]\) for all \(B^{\prime}\in S/\simeq_{p}\).