Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Spectrum of Approximate Probabilistic Bisimulations

Timm Spork, Christel Baier, Joost-Pieter Katoen, Jakob Piribauer, Tim Quatmann

TL;DR

This work addresses robustness in probabilistic bisimulation by introducing and relating several approximate notions for labeled Markov chains, including $\varepsilon$-bisimulation, $\varepsilon$-APB, and $\varepsilon$-perturbed bisimulation, plus approximate weak/branching variants. It provides formal definitions, interrelations, and practical implications for quotienting and abstraction in probabilistic model checking, along with tight bounds for unbounded reachability under $\varepsilon$-bisimilarity and complexity results (NP-completeness) for key decision problems. The results reveal both the potential and the pitfalls of using approximate notions (e.g., non-additivity and possible distinctions between bisimilar models) and establish a nuanced taxonomy that guides logic preservation and abstraction strategies. The findings have practical impact for scalable verification, enabling robust abstractions while delineating the limits of approximation in probabilistic systems.

Abstract

This paper studies various notions of approximate probabilistic bisimulation on labeled Markov chains (LMCs). We introduce approximate versions of weak and branching bisimulation, as well as a notion of $\varepsilon$-perturbed bisimulation that relates LMCs that can be made (exactly) probabilistically bisimilar by small perturbations of their transition probabilities. We explore how the notions interrelate and establish their connections to other well-known notions like $\varepsilon$-bisimulation.

A Spectrum of Approximate Probabilistic Bisimulations

TL;DR

This work addresses robustness in probabilistic bisimulation by introducing and relating several approximate notions for labeled Markov chains, including -bisimulation, -APB, and -perturbed bisimulation, plus approximate weak/branching variants. It provides formal definitions, interrelations, and practical implications for quotienting and abstraction in probabilistic model checking, along with tight bounds for unbounded reachability under -bisimilarity and complexity results (NP-completeness) for key decision problems. The results reveal both the potential and the pitfalls of using approximate notions (e.g., non-additivity and possible distinctions between bisimilar models) and establish a nuanced taxonomy that guides logic preservation and abstraction strategies. The findings have practical impact for scalable verification, enabling robust abstractions while delineating the limits of approximation in probabilistic systems.

Abstract

This paper studies various notions of approximate probabilistic bisimulation on labeled Markov chains (LMCs). We introduce approximate versions of weak and branching bisimulation, as well as a notion of -perturbed bisimulation that relates LMCs that can be made (exactly) probabilistically bisimilar by small perturbations of their transition probabilities. We explore how the notions interrelate and establish their connections to other well-known notions like -bisimulation.
Paper Structure (12 sections, 46 theorems, 9 equations, 16 figures, 1 table)

This paper contains 12 sections, 46 theorems, 9 equations, 16 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Epsilon-Bisimulation, Epsilon-APB and Up-To-(n, Epsilon)-Bisimulation
  4. Definitions and Interrelation
  5. Preservation of Logical Properties
  6. Epsilon-Perturbed Bisimulation
  7. Branching and Weak Epsilon-Bisimulation
  8. Conclusion and Future Work
  9. Proofs of Section 2
  10. Proofs of Section 3
  11. Proofs of Section 4
  12. Proofs of Section 5

Key Result

Lemma 2

A reflexive and symmetric relation $R \subseteq S \times S$ that only relates states with the same label is an $\varepsilon$-bisimulation iff for all $(s,t) \in R$ there is a map $\Delta\colon \mathit{Succ}(s) \to \mathit{Distr}(\mathit{Succ}(t))$ such that

Figures (16)

  • Figure 1: The relationship of different approximate probabilistic bisimulations.
  • Figure 2: The LMC used in \ref{['Example: Epsilon-bisimulation not transitive']}.
  • Figure 3: The LMC used in \ref{['Example: Epsilon-APBs']}, adapted from RBBTEAPC.
  • Figure 4: An LMC in which $s_0 \sim_\varepsilon t_0$ and $\vert \mathrm{Pr}_{s_0}(\lozenge^{\leq n+1} g) - \mathrm{Pr}_{t_0}(\lozenge^{\leq n+1} g) \vert = 1 - (1-\varepsilon)^{n+1}$.
  • Figure 5: The LMC used in \ref{['Example: cex thm:unbounded_reach']}.
  • ...and 11 more figures

Theorems & Definitions (61)

  • Definition 1: AAPPRBBTEAPC
  • Example 2
  • Lemma 2
  • Definition 3: RPCTLMC
  • Example 4: RBBTEAPC
  • Definition 5: AAPPSAAPBPCTL
  • Proposition 5
  • Theorem 6: RBBTEAPC
  • Example 7
  • Example 8
  • ...and 51 more