Smoothed model checking for uncertain continuous-time Markov chains
From MaRDI portal
Publication:259074
DOI10.1016/J.IC.2016.01.004zbMATH Open1336.68162arXiv1402.1450OpenAlexW2157413433MaRDI QIDQ259074FDOQ259074
Dimitrios Milios, Luca Bortolussi, Guido Sanguinetti
Publication date: 10 March 2016
Published in: Information and Computation (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1402.1450
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
Applications of continuous-time Markov processes on discrete state spaces (60J28) Gaussian processes (60G15) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Bio-PEPA: A framework for the modelling and analysis of biological systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- Markov Chains
- On the influence of the kernel on the consistency of support vector machines
- Title not available (Why is that?)
- Stochastic epidemic models and their statistical analysis
- System design of stochastic models using robustness of temporal properties
- Statistical probabilistic model checking with a focus on time-bounded properties
- Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
- Bayesian statistical model checking with application to Simulink/Stateflow verification
- Model Repair for Probabilistic Systems
- Time-Bounded Verification of CTMCs against Real-Time Specifications
- LTL Model Checking of Interval Markov Chains
- Three-Valued Abstraction for Continuous-Time Markov Chains
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Data-Driven Statistical Learning of Temporal Logic Properties
- Constraint Markov chains
- Theoretical Aspects of Computing - ICTAC 2004
- Title not available (Why is that?)
- Essentials of Stochastic Processes
Cited In (15)
- Active and sparse methods in smoothed model checking
- Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
- Parameter synthesis for Markov models: covering the parameter space
- Model checking Markov population models by stochastic approximations
- Automaton-ABC: a statistical method to estimate the probability of spatio-temporal properties for parametric Markov population models
- Statistical abstraction for multi-scale spatio-temporal systems
- Precise parameter synthesis for stochastic biochemical systems
- Sampling-Based Verification of CTMCs with Uncertain Rates
- Deniable Functional Encryption
- Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes
- Sequential Convex Programming for the Efficient Verification of Parametric MDPs
- Geometric fluid approximation for general continuous-time Markov chains
- Parameter synthesis in Markov models: a gentle survey
- Efficient sensitivity analysis for parametric robust Markov chains
- A formal approach for tuning stochastic oscillators
Uses Software
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)
