Computing Probabilistic Bisimilarity Distances

Behavioural equivalences like probabilistic bisimilarity rely on the transition probabilities and, as a result, are sensitive to minuscule changes of those probabilities. Such behavioural equivalences are not robust, as first observed by Giacalone, Jou and Smolka. Probabilistic bisimilarity distances, a robust quantitative generalization of probabilistic bisimilarity, capture the similarity of the behaviour of states of a probabilistic model. The smaller the distance, the more alike the states behave. In particular, states are probabilistic bisimilar if and only if the distance between them is zero. In this dissertation, we focus on algorithms to compute probabilistic bisimilarity distances for two probabilistic models: labelled Markov chains and probabilistic automata.

In the late nineties, Desharnais, Gupta, Jagadeesan and Panangaden defined probabilistic bisimilarity distances on the states of a labelled Markov chain. This provided a quantitative generalization of probabilistic bisimilarity, which was introduced by Larsen and Skou a decade earlier. Several algorithms to approximate and compute these probabilistic bisimilarity distances have been put forward. In this dissertation, we correct and generalize some of these policy iteration algorithms. Moreover, we develop several new algorithms which have better performance in practice and can handle much larger systems.

Similarly, Deng, Chothia, Palamidessi and Pang presented probabilistic bisimilarity distances on the states of a probabilistic automaton. This provided a robust quantitative generalization of probabilistic bisimilarity introduced by Segala and Lynch. Although the complexity of computing probabilistic bisimilarity distances for probabilistic automata has already been studied and shown to be in NP coNP and PPAD, we are not aware of any practical algorithms to compute those distances. In this dissertation, we provide several key results that may prove to be useful for the development of algorithms to compute probabilistic bisimilarity distances for probabilistic automata. In particular, we present a polynomial time algorithm that decides distance one. Furthermore, we give an alternative characterization of the probabilistic bisimilarity distances as a basis for a policy iteration algorithm.