Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
Logic in Computer Science
2025-05-23 v2
Abstract
We introduce -bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, -bisimulation allows the use of different tolerances for the transition probabilities (, 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 -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