Perturbation Analysis in Probabilistic Model Checking
COM1 Level 3
MR1, COM1-03-19
Abstract:
Probabilistic model checking is a formal verification technique that has been applied successfully in a variety of domains, providing identification of system errors through quantitative verification of stochastic systems models such as Markov chains (MCs) and Markov decision processes (MDPs).
For real-world domains, external system factors and environmental changes must be estimated accurately in the form of probabilities in systems models; inaccurate estimates for the model probabilities can lead to invalid verification results. To address this problem, this thesis proposal aims to study the worst-case consequences of uncertainty on verification of system properties by using perturbation analysis. In particular, this thesis focuses on steady-state properties of MCs and reachability properties of MDPs.
The main contributions of this thesis proposal are a perturbation framework for using perturbation analysis in probabilistic model checking, a novel perturbation approach for studying the uncertainty on verification of steady-state properties of reducible and irreducible MCs, and an innovative technique for efficiently analyzing the effects of perturbations of model probabilities on verification of reachability properties of MDPs. We demonstrate the practical effectiveness of our approaches by applying it to several case studies.