| Summary: | Probabilistic bisimilarity is a fundamental notion of equivalence on labelled Markov chains. It has a natural generalisation to a probabilistic bisimilarity pseudometric, whose definition involves the Kantorovich metric on probability distributions. The pseudometric has discounted and undiscounted variants, according to whether one discounts the future in observing discrepancies between states. This paper is concerned with the complexity of computing probabilistic bisimilarity and the probabilistic bisimilarity pseudometric on labelled Markov chains. We show that the problem of computing probabilistic bisimilarity is P-hard by reduction from the monotone circuit value problem. We also show that the discounted pseudometric is rational and can be computed exactly in polynomial time using the network simplex algorithm and the continued fraction algorithm. In the undiscounted case we show that the pseudometric is again rational and can be computed exactly in polynomial time using the ellipsoid algorithm. Finally, using the notion of couplings on Markov chains, we show that the pseudometric can be used to compute bounds on the variational distance of trace distributions, which is NP-hard to compute directly. © 2012 Springer-Verlag Berlin Heidelberg.
|
|---|