Robust Probabilistic Bisimilarity for Labelled Markov Chains

TL;DR

The paper addresses the lack of robustness of probabilistic bisimilarity distances to small perturbations in transition probabilities, which can yield discontinuities that undermine reliability in approximate models. It defines robust probabilistic bisimilarity for labelled Markov chains, and proves it is a robust bisimulation (the greatest such) that ensures the distance $\delta_{\tau}$ is continuous under perturbations. It presents a polynomial-time algorithm for computing robust bisimilarity based on a Refine/Filter/Prune/Bisim scheme and validates the approach with experiments on QVBS benchmarks and Java PathFinder variants, showing practical feasibility albeit with higher computation than traditional bisimilarity. The work also discusses implications, potential logical characterizations, and directions for future research on robustness and perturbation models.

Abstract

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.