Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

Lecture notes in computer science, pp. 56–81

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.

Authors 5

1. Timm Spork corresponding

   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