www.prismmodelchecker.org
[FKPB26] Syyeda Zainab Fatmi, Stefan Kiefer, David Parker and Franck van Breugel. On the Continuity of the Probabilistic Bisimilarity Distance. In Proc. 37th International Conference on Concurrency Theory (CONCUR'26). September 2026. [pdf] [bib] [Studies continuity of probabilistic bisimilarity distance for labelled Markov chains, with an implementation and evaluation in PRISM. ]
Downloads:  pdf pdf (713 KB)  bib bib
Links: [Google] [Google Scholar]
Abstract. The probabilistic bisimilarity distance provides a quantitative measure of behavioural difference for labelled Markov chains, but it may be discontinuous under perturbations of the transition probabilities. This lack of continuity undermines its applicability to empirically derived models, where transition probabilities are often approximations. Recently, we introduced robust probabilistic bisimilarity as a sufficient condition for continuity at distance zero. In this paper, we show that it is also a necessary condition, that is, two states are robustly probabilistic bisimilar if and only if their probabilistic bisimilarity distance is small for any small enough perturbation of the transition probabilities. We further extend robustness to non-bisimilar state pairs to establish a complete characterization for continuity of the probabilistic bisimilarity distance. Based on this characterization, we develop a polynomial time algorithm to decide continuity. Finally, we complement our theoretical contributions with an experimental evaluation demonstrating the proposed approach in practice. Our results show that the extra step of deciding continuity requires minimal additional cost when compared to computing the probabilistic bisimilarity distance.

Publications