Robust Probabilistic Bisimilarity for Labelled Markov Chains
For researchers and practitioners using probabilistic bisimilarity in systems verification, this work solves the discontinuity problem caused by approximate transition probabilities.
The paper introduces robust probabilistic bisimilarity for labelled Markov chains to address the lack of robustness under small perturbations of transition probabilities, ensuring continuity of the distance function. The proposed algorithm computes this efficiently and performs well in practice.
Despite its prevalence, probabilistic bisimilarity suffers from a lack of robustness under minuscule perturbations of the transition probabilities. This can lead to discontinuities in the probabilistic bisimilarity distance function, undermining its reliability in practical applications where transition probabilities are often approximations derived from experimental data. Motivated by this limitation, we introduce the notion of robust probabilistic bisimilarity for labelled Markov chains, which ensures the continuity of the probabilistic bisimilarity distance function. We also propose an efficient algorithm for computing robust probabilistic bisimilarity and show that it performs well in practice, as evidenced by our experimental results.