Active and Sparse Methods in Smoothed Model Checking

Paul Piho, Jane Hillston

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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 incorporate sparse variational methods and active learning into the smoothed model checking setting. We use these methods 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. We demonstrate that online extensions of sparse variational Gaussian process inference algorithms provide a scalable method for implementing active learning approaches for smoothed model checking.
Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems
Subtitle of host publication18th International Conference, QEST 2021, Paris, France, August 23–27, 2021, Proceedings
PublisherSpringer Nature Switzerland AG
Number of pages18
ISBN (Electronic)978-3-030-85172-9
ISBN (Print)978-3-030-85171-2
Publication statusPublished - 19 Aug 2021
Event18th International Conference on Quantitative Evaluation of SysTems - Paris, France
Duration: 23 Aug 202127 Aug 2021

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference18th International Conference on Quantitative Evaluation of SysTems
Abbreviated titleQEST 2021
Internet address


Dive into the research topics of 'Active and Sparse Methods in Smoothed Model Checking'. Together they form a unique fingerprint.

Cite this