# An Efficient Algorithm to Determine Probabilistic Bisimulation
## 1 Introduction  
In [1], [PERSON] and [PERSON] proposed the notion of probabilistic bisimulation. Although described for deterministic transition systems, the same notion is also very suitable for probabilistic transition systems with nondeterminism [2; 3], i.e. so-called PLTSs. It expresses that two states are equivalent exactly when the following condition holds: if one state can perform an action ending up in a set of states, each with a certain probability, and then the other state can do the same step ending up in an equivalent set of states with the same distribution of probabilities. Two characteristic nondeterministic transition systems of which the initial states are probabilistically bisimilar are given in Figure 1.  
In [4], [PERSON] et al. gave an algorithm for probabilistic bisimulation for PLTSs, thus dealing both with probabilistic and nondeterministic choice, of time complexity \(O\left(mn\log m+\log n\right)\) and space  
Figure 1: Two probabilistically bisimilar nondeterministic transition systems. complexity \(O\left(mn\right)\), where \(n\) is the number of states and \(m\) is the number of transitions (from states to distributions over states; there is no separate measure for the size of the distributions). As far as we know, it is the only practical algorithm for bisimulation a la Larsen-Skou for PLTSs. In essence, other algorithms for probabilistic systems typically target Markov chains without nondeterminism. The algorithm in [4] performs an iterative refinement of a partition of states and a partition of transitions per action label. The crucial point is splitting the groups of states based on probabilities. For this, a specific data structure is used, called augmented ordered balanced trees, to support efficient storage, retrieval and ordering of states indexed by probabilities. In this paper, we provide a new algorithm for probabilistic bisimulation for PLTSs of time complexity \(O\left(\left(m_{a}+m_{p}\right)\log n_{p}+m_{p}\log n_{a}\right)\right)\) and space complexity \(O\left(m_{a}+m_{p}\right)\), where \(n_{a}\) is the number of states, \(m_{a}\) the number of transitions labelled with actions, \(n_{p}\) the number of distributions and \(m_{p}\) the cumulative support of the distributions. Our \(n_{a}\) coincides with the \(n\) of [PERSON] et al. We prefer to use \(m_{a}\), \(n_{p}\), and \(m_{p}\) over \(m\) as the former support a more refined analysis. A detailed comparison between the algorithms reveals that, if the distributions have a positive probability for all states, the complexities of the algorithms are similar. However, when distributions only touch a limited number of states, as is often the common situation, the implementation of our algorithm outperforms our implementation of the algorithm in [4], both in time as well as in space complexity. Similar to the algorithm of [PERSON] et al., our algorithm keeps track of a partition of states and of distributions (referred to as action states and probabilistic states below) but in line with the classical Paige-Tarjan approach [5] it also maintains a courser partition of so-called constellations. The treatment of distributions in our algorithm is strongly inspired by the work for Markov Chain lumping by [PERSON] and [PERSON], but our algorithm applies to the richer setting of non-deterministic labelled probabilistic transition systems. Using a brilliant, yet simple argument, taken from [6], the number of times a probabilistic transition is sorted can be limited by the fan-out of the source state of the transition. This leads to the observation that we can use straightforward sorting without the need of any tailored data structure such as augmented ordered balanced trees or similar as in [4; 7]. Actually, our algorithm uses a simplification of the algorithm in [6] since the calculation of so-called _majority candidates_ can be avoided, too. We implemented both the new algorithm and the algorithm from [4]. We spent quite some effort to establish that both implementations are free from programming flaws.