English

Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

Logic in Computer Science 2025-05-23 v2

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.

Keywords

Cite

@article{arxiv.2505.15587,
  title  = {Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains},
  author = {Timm Spork and Christel Baier and Joost-Pieter Katoen and Sascha Klüppelholz and Jakob Piribauer},
  journal= {arXiv preprint arXiv:2505.15587},
  year   = {2025}
}

Comments

Full version of a paper accepted for publication at CAV 2025

R2 v1 2026-07-01T02:28:47.598Z