Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

TL;DR

We address robustness of CTMC model-checking under perturbations of transition probabilities and exit rates by introducing (epsilon, delta)-bisimulation, which decouples additive tolerances on transition probabilities from multiplicative, via the bound $|ln(E(s)) - ln(E(s'))| ≤ delta$. The framework establishes fundamental properties, including that the union of all (epsilon, delta)-bisimulations is itself an (epsilon, delta)-bisimulation, additivity in epsilon and delta, and equivalence to strong bisimulation when epsilon = delta = 0. Time-bounded reachability bounds are obtained by uniformizing the CTMC and applying results from the discrete-time setting, yielding $|Pr_s(lozenge^{≤ t} g) - Pr_{s'}(lozenge^{≤ t} g)| ≤ 1 - e^{-q t (e^{delta}(1 + epsilon) - 1)}$, with tighter analyses for the (0, delta)-case via Erlang CTMCs and spectral techniques, and extensions to nonnegative rewards via a reward-to-time transformation. The work positions (epsilon, delta)-bisimilarity relative to quasi-lumpability, proportional lumpability, and UCTMC analysis, and discusses computation and potential extensions such as (epsilon, delta, mu)-bisimulation and preservation of CSL-model checking properties.

Abstract

We introduce $(\varepsilon, δ)$-bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $(\varepsilon, δ)$-bisimulation allows the use of different tolerances for the transition probabilities ($\varepsilon$, additive) and total exit rates ($δ$, 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,δ)$-bisimilar states, are established.

Figures (1)

• Figure 1: Three CTMCs where the copies of the states can be related by a $\tau$-quasi-lumpability iff $\tau \geq 1$. The numbers indicate the transition rates between states.