Sampling-Based Verification of CTMCs with Uncertain Rates

Thom S. Badings*, Nils Jansen, Sebastian Junges, Marielle Stoelinga, Matthias Volk

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

4 Citations (Scopus)
50 Downloads (Pure)


We employ uncertain parametric CTMCs with parametric transition rates and a prior on the parameter values. The prior encodes uncertainty about the actual transition rates, while the parameters allow dependencies between transition rates. Sampling the parameter values from the prior distribution then yields a standard CTMC, for which we may compute relevant reachability probabilities. We provide a principled solution, based on a technique called scenario-optimization, to the following problem: From a finite set of parameter samples and a user-specified confidence level, compute prediction regions on the reachability probabilities. The prediction regions should (with high probability) contain the reachability probabilities of a CTMC induced by any additional sample. To boost the scalability of the approach, we employ standard abstraction techniques and adapt our methodology to support approximate reachability probabilities. Experiments with various well-known benchmarks show the applicability of the approach.
Original languageEnglish
Title of host publicationComputer Aided Verification (CAV 2022)
Subtitle of host publication34th International Conference, CAV 2022, Haifa, Israel, August 7–10, 2022, Proceedings, Part II
EditorsSharon Shoham, Yakir Vizel
Number of pages22
ISBN (Electronic)978-3-031-13188-2
Publication statusPublished - 6 Aug 2022
Event34th International Conference on Computer Aided Verification, CAV 2022 - Haifa, Israel
Duration: 7 Aug 202210 Aug 2022
Conference number: 34

Publication series

NameLecture notes in computer science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference34th International Conference on Computer Aided Verification, CAV 2022
Abbreviated titleCAV 2022


  • This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.


Dive into the research topics of 'Sampling-Based Verification of CTMCs with Uncertain Rates'. Together they form a unique fingerprint.

Cite this