Statusvortrag im Rahmen des Promotionsver­fahrens von Herrn Timm Spork

Abstract:

The state-space explosion problem is a well-known bottleneck for the tractability of probabilistic model checking. A widely adopted technique to combat this issue involves grouping states related by probabilistic bisimulations. These equivalences, intuitively, identify states with the same label and transition probabilities. Since exact probabilities are, however, oftentimes not available in practice, approximate probabilistic bisimulations emerged, which allow the transition probabilities of related states to differ by a small value.

In this talk, we define three new types of approximate probabilistic bisimulation for discrete-time Markov chains: ε-perturbed bisimulation, weak ε-bisimulation, and branching ε-bisimulation. We compare our notions to one another, as well as to approaches from the literature, and derive tight bounds on the absolute difference of reachability probabilities of states related by branching resp. weak ε-bisimulations. 

Moreover, we introduce (ε, δ)-bisimulations for continuous-time Markov chains. In contrast to existing work, (ε, δ)-bisimulations use separate tolerance values for the probabilities (ε, additive) and exit rates (δ, multiplicative). We demonstrate that this separation of concerns allows us to express the (dis)similarities of related models in a more fine-grained manner than existing notions, and provide tight bounds on the absolute difference of time- and reward-bounded reachability probabilities of (ε, δ)-bisimilar models.