Computing probabilistic bisimilarity distances for labelled Markov chains

The most prominent behavioural equivalence for labelled Markov chains is probabilistic bisimilarity, due to Larsen and Skou. Numerous quantititative generalizations of this behavioural equivalence have been proposed. We focus on the probabilistic bisimilarity pseudometric due to Desharnais et al., whose definition involves the Kantorovich metric on probability distributions. Chen, van Breugel and Worrell showed that this probabilistic bisimilarity pseudometric can be computed exactly in polynomial time using the ellipsoid algorithm. Bacci et al. later introduced a more practical algorithm to compute the probabilistic bisimilarity distances for a labelled Markov chain.

We present a transformation mapping each labelled Markov chain to a Markov decision process (MDP) where the probabilistic bisimilarity distances of the labelled Markov chain correspond to the optimal values of the MDP. The policy iteration algorithm, which can be used to compute the optimal values of the MDP, thus can be applied to compute the probabilistic bisimilarity distances for the labelled Markov chain. We show that the algorithm by Bacci et al. is the simple policy iteration algorithm and it takes exponential time in the worst case.

This is joint work with Franck van Breugel.