Approximating a Behavioural Pseudometric without Discount for Probabilistic Systems

Desharnais, Gupta, Jagadeesan and Panangaden introduced a family ofbehavioural pseudometrics for probabilistic transition systems. Thesepseudometrics are a quantitative analogue of probabilistic bisimilarity.Distance zero captures probabilistic bisimilarity. Each pseudometric has adiscount factor, a real number in the interval (0, 1]. The smaller the discountfactor, the more the future is discounted. If the discount factor is one, thenthe future is not discounted at all. Desharnais et al. showed that thebehavioural distances can be calculated up to any desired degree of accuracy ifthe discount factor is smaller than one. In this paper, we show that thedistances can also be approximated if the future is not discounted. A keyingredient of our algorithm is Tarski's decision procedure for the first ordertheory over real closed fields. By exploiting the Kantorovich-Rubinsteinduality theorem we can restrict to the existential fragment for which moreefficient decision procedures exist