Active and sparse methods in smoothed model checking

TL;DR

This paper enhances smoothed model checking for continuous time Markov chains by integrating sparse variational methods and active learning, significantly improving scalability and efficiency in parameter space exploration.

Contribution

It introduces scalable active learning and sparse variational Gaussian process techniques to advance smoothed model checking for complex Markov models.

Findings

Active learning improves sample efficiency in model checking.

Sparse variational methods enhance scalability.

Online algorithms enable practical application in large models.

Abstract

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.