# Sampling-Based Verification of CTMCs with Uncertain Rates

arXiv: https://arxiv.org/abs/2205.08300 · HTML: https://mlsanity.com/paper/2205.08300/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 May 2022.

## Built on by (most cited first, 5 of 5)

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions](https://mlsanity.com/paper/2301.01526/) (2023)
- [Decision-Making Under Uncertainty: Beyond Probabilities](https://mlsanity.com/paper/2303.05848/) (2023)
- [Certifiably Robust Policies for Uncertain Parametric Environments](https://mlsanity.com/paper/2408.03093/) (2024)
- [Learning-Based Approaches to Predictive Monitoring with Conformal Statistical Guarantees](https://mlsanity.com/paper/2312.01959/) (2023)

## Abstract (arXiv)

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.