Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

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

Original languageEnglish
Title of host publicationComputer Aided Verification
EditorsRuzica Piskac, Zvonimir Rakamaric
PublisherSpringer Science and Business Media B.V.
Pages56-81
Number of pages26
ISBN (electronic)978-3-031-98679-6
ISBN (print)978-3-031-98678-9
Publication statusPublished - 2025
Peer-reviewedYes

Publication series

SeriesLecture notes in computer science
Volume15932 LNCS
ISSN0302-9743

Conference

Title37th International Conference on Computer Aided Verification
Abbreviated titleCAV 2025
Conference number37
Duration21 - 25 July 2025
Website
LocationWestin Hotel Zagreb
CityZagreb
CountryCroatia

External 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

Keywords

Keywords

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