Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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.

Details

OriginalspracheEnglisch
TitelComputer Aided Verification
Redakteure/-innenRuzica Piskac, Zvonimir Rakamaric
Herausgeber (Verlag)Springer Science and Business Media B.V.
Seiten56-81
Seitenumfang26
ISBN (elektronisch)978-3-031-98679-6
ISBN (Print)978-3-031-98678-9
PublikationsstatusVeröffentlicht - 2025
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture notes in computer science
Band15932 LNCS
ISSN0302-9743

Konferenz

Titel37th International Conference on Computer Aided Verification
KurztitelCAV 2025
Veranstaltungsnummer37
Dauer21 - 25 Juli 2025
Webseite
OrtWestin Hotel Zagreb
StadtZagreb
LandKroatien

Externe IDs

ORCID /0000-0002-5321-9343/work/190570262
ORCID /0000-0003-1724-2586/work/190571815
ORCID /0000-0003-4829-0476/work/190572126
ORCID /0009-0008-4461-0667/work/190572206

Schlagworte

Schlagwörter

  • Approximate Probabilistic Bisimulation, Continuous-Time Markov Chains, Quasi-Lumpability, Time-Bounded Reachability