# Active and sparse methods in smoothed model checking

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 23 references that are in the map.
- First posted on arXiv 20 Apr 2021.

## Builds on (most cited first, 4 of 4)

- [Expectation Propagation for approximate Bayesian inference](https://mlsanity.com/paper/1301.2294/) (2013)
- [Streaming Sparse Gaussian Process Approximations](https://mlsanity.com/paper/1705.07131/) (2017)
- [Scalable Gaussian Process Classification via Expectation Propagation](https://mlsanity.com/paper/1507.04513/) (2015)
- [Smoothed Model Checking for Uncertain Continuous Time Markov Chains](https://mlsanity.com/paper/1402.1450/) (2014)

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

- [Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking](https://mlsanity.com/paper/2205.05398/) (2022)

## Abstract (arXiv)

Smoothed model checking based on Gaussian process classification provides a powerful approach for statistical model checking of parametric continuous time Markov chain models. The method constructs a model for the functional dependence of satisfaction probability on the Markov chain parameters. This is done via Gaussian process inference methods from a limited number of observations for different parameter combinations. In this work we consider extensions to smoothed model checking based on sparse variational methods and active learning. Both are used successfully to improve the scalability of smoothed model checking. In particular, we see that active learning-based ideas for iteratively querying the simulation model for observations can be used to steer the model-checking to more informative areas of the parameter space and thus improve sample efficiency. Online extensions of sparse variational Gaussian process inference algorithms are demonstrated to provide a scalable method for implementing active learning approaches for smoothed model checking.