Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

Abstract

We introduce $(\epsilon ,\hat{I}´)$-bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $(\epsilon ,\hat{I}´)$-bisimulation allows the use of different tolerances for the transition probabilities ($\epsilon$, additive) and total exit rates ($\hat{I}´$, multiplicative) of states. Fundamental properties of the notion, as well as bounds on the absolute difference of time- and reward-bounded reachability probabilities for $(\epsilon ,\hat{I}´)$-bisimilar states, are established.

Full version of a paper accepted for publication at CAV 2025