Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

arXiv (Cornell University)

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.

Authors 5

1. Timm Spork

   Technische Universität Dresden

   Affiliation as printed

   Technische Universität Dresden , Dresden , Germany

2. Christel Baier

   Technische Universität Dresden

   Affiliation as printed

   Technische Universität Dresden , Dresden , Germany

3. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany

4. Sascha Klüppelholz

   Technische Universität Dresden

   Affiliation as printed

   Technische Universität Dresden , Dresden , Germany

5. Jakob Piribauer

   Technische Universität Dresden · Leipzig University

   Affiliation as printed

   Technische Universität Dresden , Dresden , Germany

   Universität Leipzig , Leipzig , Germany