Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

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