Abstract
In 1999, Desharnais, Gupta, Jagadeesan and Panangaden introduced a quantitative generalization of probabilistic bisimilarity, a behavioral equivalence due to Larsen and Skou. Desharnais et al. assign a distance to each pair of states of a labelled Markov chain. The distance captures the behavioral similarity of the states. The smaller the distance, the more alike the states behave. Distance
zero captures probabilistic bisimilarity.
In the last decade, several algorithms have been proposed to approximate and compute these probabilistic bisimilarity distances. In this talk, I will present a simple algorithm that computes the set of state pairs that have distance one, that is, those state pairs that behave very differently. The algorithm relies on the fact that probabilistic bisimilarity has already been computed.
Experiments show that the algorithm that first decides probabilistic bisimilarity, then decides distance one, and finally computes the remaining distances using policy iteration is more than an order of magnitude faster than the algorithm that does not decide distance one. The algorithms to decide probabilistic bisimilarity and distance one also allow us to quickly determine if there are any non-trivial distances, that is, any distances different from zero and one.
Joint work with Qiyi Tang.