Smoothed model checking for uncertain continuous-time Markov chains
From MaRDI portal
Abstract: We consider the problem of computing the satisfaction probability of a formula for stochastic models with parametric uncertainty. We show that this satisfaction probability is a smooth function of the model parameters. This enables us to devise a novel Bayesian statistical algorithm which performs statistical model checking simultaneously for all values of the model parameters from observations of truth values of the formula over individual runs of the model at isolated parameter values. This is achieved by exploiting the smoothness of the satisfaction function: by modelling explicitly correlations through a prior distribution over a space of smooth functions (a Gaussian Process), we can condition on observations at individual parameter values to construct an analytical approximation of the function itself. Extensive experiments on non-trivial case studies show that the approach is accurate and several orders of magnitude faster than naive parameter exploration with standard statistical model checking methods.
Recommendations
- Active and sparse methods in smoothed model checking
- Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
- Statistical probabilistic model checking with a focus on time-bounded properties
- Theoretical Aspects of Computing - ICTAC 2004
- Bayesian statistical model checking with application to Simulink/Stateflow verification
Cites work
- scientific article; zbMATH DE number 5988004 (Why is no real title available?)
- Assessing approximate inference for binary Gaussian process classification.
- Bayesian statistical model checking with application to Simulink/Stateflow verification
- Bio-PEPA: A framework for the modelling and analysis of biological systems
- Constraint Markov chains
- Data-driven statistical learning of temporal logic properties
- Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
- Essentials of stochastic processes.
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Gaussian processes for machine learning.
- Hybrid performance modelling of opportunistic networks
- LTL model checking of interval Markov chains
- Markov Chains
- Model repair for probabilistic systems
- On the influence of the kernel on the consistency of support vector machines
- Statistical probabilistic model checking with a focus on time-bounded properties
- Stochastic epidemic models and their statistical analysis
- System design of stochastic models using robustness of temporal properties
- Theoretical Aspects of Computing - ICTAC 2004
- Three-Valued Abstraction for Continuous-Time Markov Chains
- Time-Bounded Verification of CTMCs against Real-Time Specifications
Cited in
(16)- Sampling-Based Verification of CTMCs with Uncertain Rates
- Geometric fluid approximation for general continuous-time Markov chains
- Active and sparse methods in smoothed model checking
- Sequential convex programming for the efficient verification of parametric MDPs
- Parameter synthesis in Markov models: a gentle survey
- An MM algorithm to estimate parameters in continuous-time Markov chains
- Statistical abstraction for multi-scale spatio-temporal systems
- Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes
- Deniable Functional Encryption
- Precise parameter synthesis for stochastic biochemical systems
- Efficient sensitivity analysis for parametric robust Markov chains
- Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
- Automaton-ABC: a statistical method to estimate the probability of spatio-temporal properties for parametric Markov population models
- Parameter synthesis for Markov models: covering the parameter space
- Model checking Markov population models by stochastic approximations
- A formal approach for tuning stochastic oscillators
This page was built for publication: Smoothed model checking for uncertain continuous-time Markov chains
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q259074)
