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 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 language | English |
---|---|
Title of host publication | Quantitative Evaluation of Systems |
Subtitle of host publication | 18th International Conference, QEST 2021, Paris, France, August 23–27, 2021, Proceedings |
Publisher | Springer Nature |
Pages | 217-234 |
Number of pages | 18 |
ISBN (Electronic) | 978-3-030-85172-9 |
ISBN (Print) | 978-3-030-85171-2 |
DOIs | |
Publication status | Published - 19 Aug 2021 |
Event | 18th International Conference on Quantitative Evaluation of SysTems - Paris, France Duration: 23 Aug 2021 → 27 Aug 2021 https://www.qest.org/qest2021/ |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Volume | 12846 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 18th International Conference on Quantitative Evaluation of SysTems |
---|---|
Abbreviated title | QEST 2021 |
Country/Territory | France |
City | Paris |
Period | 23/08/21 → 27/08/21 |
Internet address |