Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

TL;DR

This paper introduces a new form of approximate bisimulation for continuous-time Markov chains that separately tolerates differences in transition probabilities and exit rates, providing bounds on reachability probabilities.

Contribution

It proposes $(rac{ ext{epsilon}}{ ext{delta}})$-bisimulation, allowing different tolerances for transition probabilities and exit rates, with proven properties and bounds.

Findings

Established fundamental properties of $(rac{ ext{epsilon}}{ ext{delta}})$-bisimulation.

Derived bounds on reachability probabilities for bisimilar states.

Demonstrated applicability to 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.