# Smoothed Model Checking for Uncertain Continuous Time Markov Chains

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Feb 2014.

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

- [Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes](https://mlsanity.com/paper/2211.02375/) (2022)
- [Neural Predictive Monitoring under Partial Observability](https://mlsanity.com/paper/2108.07134/) (2021)
- [Efficient Sensitivity Analysis for Parametric Robust Markov Chains](https://mlsanity.com/paper/2305.01473/) (2023)
- [Learning-Based Approaches to Predictive Monitoring with Conformal Statistical Guarantees](https://mlsanity.com/paper/2312.01959/) (2023)
- [Active and sparse methods in smoothed model checking](https://mlsanity.com/paper/2104.09940/) (2021)
- [Conformal Predictive Monitoring for Multi-Modal Scenarios](https://mlsanity.com/paper/2509.01338/) (2025)
- [Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking](https://mlsanity.com/paper/2205.05398/) (2022)

## Abstract (arXiv)

We consider the problem of computing the satisfaction probability of a formula for stochastic models with parametric uncertainty. We show that this satisfaction probability is a smooth function of the model parameters. This enables us to devise a novel Bayesian statistical algorithm which performs statistical model checking simultaneously for all values of the model parameters from observations of truth values of the formula over individual runs of the model at isolated parameter values. This is achieved by exploiting the smoothness of the satisfaction function: by modelling explicitly correlations through a prior distribution over a space of smooth functions (a Gaussian Process), we can condition on observations at individual parameter values to construct an analytical approximation of the function itself. Extensive experiments on non-trivial case studies show that the approach is accurate and several orders of magnitude faster than naive parameter exploration with standard statistical model checking methods.