Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

Abstract

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.