Applications of Perturbation Analysis in Probabilistic Model Checking
COM1 Level 3
MR1, COM1-03-19
Abstract:
In the recent decades, probabilistic model checking has been a successful research area in formal methods. 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 discrete-time Markov chains (DTMCs) 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 aims to study the worst-case consequences of uncertainty on verification of system properties by using perturbation analysis. In particular, this thesis focuses on the long-run behavior of DTMCs and reachability properties of MDPs.
The main contributions of this thesis are a novel perturbation approach for studying the uncertainty on the computation of long-run probabilities of reducible and irreducible DTMCs 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.