Sampling-Based Verification of CTMCs with Uncertain Rates

TL;DR

This paper introduces a sampling-based method for verifying continuous-time Markov chains with uncertain transition rates, providing probabilistic guarantees on reachability probabilities through scenario-optimization and abstraction techniques.

Contribution

It presents a novel approach combining scenario-optimization with parametric CTMCs and uncertainty modeling, enabling scalable probabilistic verification with confidence guarantees.

Findings

Effective prediction regions for reachability probabilities

Scalable approach using abstraction techniques

Validated on well-known benchmarks

Abstract

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.