Active and sparse methods in smoothed model checking

DOI10.1007/978-3-030-85172-9_12zbMATH Open1491.68112arXiv2104.09940OpenAlexW3183852024MaRDI QIDQ832071FDOQ832071

Jane Hillston, Paul Piho

Publication date: 24 March 2022

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.

Full work available at URL: https://arxiv.org/abs/2104.09940

Recommendations

• Smoothed model checking for uncertain continuous-time Markov chains
• Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
• Statistical probabilistic model checking with a focus on time-bounded properties
• Bayesian statistical model checking with application to Simulink/Stateflow verification
• Prior-based model checking

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• The design and analysis of computer experiments.
• Gaussian processes for machine learning.
• Sparse on-line Gaussian processes
• System design of stochastic models using robustness of temporal properties
• Smoothed model checking for uncertain continuous-time Markov chains
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Stochastic Model Checking
• Active Learning
• Computer Aided Verification
• Robust satisfaction of temporal logic over real-valued signals
• Statistical model checking
• Bayesian statistical parameter synthesis for linear temporal properties of stochastic models

Uses Software

• GitHub

This page was built for publication: Active and sparse methods in smoothed model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832071)