Perturbation Analysis for Probabilistic Verification

This project mainly concerns probabilistic model checking (PMC), which enhances classical model checking techniques to verify stochastic systems against various quantitative properties, for instance, reliability, security, and performance. PMC has witnessed successful applications from domains as diverse as randomised algorithms, network protocol design, robotics, and systems biology.

Current practice of probabilistic model checking usually assumes that numerical quantities (e.g., transition probabilities, transition rates) in stochastic models are known exactly, or can be acquired precisely. This is a handy, but unfortunately oversimplified, assumption. Indeed, real-world systems, for instance those from engineering, biology, or economics, are governed by parameters whose values must be empirically estimated. These values are of a statistical nature and thus are subject to perturbations, which raises the sensitivity or robustness issue of the verification results. Research has demonstrated that even small perturbations of probabilities might lead to significant variations in the verification result, and thus the results obtained using existing PMC algorithms and tools can be misleading or even invalid.

To tackle this issue, we propose to carry out perturbation analysis, i.e., to analyse how the verification result is affected by the perturbation of parameters and to provide a quantitative measure thereof. Concretely speaking, we will first investigate how to define the measures formally, possibly in various forms of perturbation bounds. Then we will develop efficient and effective algorithms to compute these perturbation bounds, and identify their computational complexity. Finally, we will develop software tools to facilitate the perturbation analysis. The toolkit will be employed to conduct case studies on real-world problems for a thorough evaluation of our approach and demonstration of its applicability and significance.

An immediate impact of the project is to improve the state-of-the-art probabilistic model checkers. With the theory and algorithms, as well as the toolkit, developed in this project, the probabilistic model checker is able to provide a quantitative measure of the robustness so the user can interpret the verification result more appropriately. This functionality will be integrated into mainstream probabilistic model checker such as PRISM, MRMC, etc. Such enhanced probabilistic model checkers would have a profound impact on the research and development in many areas where they have been successfully employed. Typical examples include system biology. Research in these areas usually requires analysis of numerous stochastic models (mostly Markov chains) in which the robustness of analysis results is crucial in testing or validating hypothesis and drawing valid conclusions. Hence, our results may have direct impact on these areas. Essentially they provide a valuable means to facilitate, and even accelerate, the research and development therein. To demonstrate this, we will collaborate with researchers from Department of Psychology, Middlesex University on behaviour analysis of social foraging in gulls. This is a novel research application of probabilistic model checking and is expected to be a perfect arena to showcase our results.

This project also has potential impact of software engineering, in particular, model driven software development that turns out to be crucial to produce high-quality, trustworthy software. Due to the uncertainty arising in the software environment, probabilistic models are highly favourable to model the real scenarios in a more faithful way. However, such probabilistic models are very difficult to obtain in practice, and even when they are available, the models are imprecise in terms of quantitative values. In this setting, the verification result might be misleading or even incorrect. This has become one of the major obstacles to apply model-based methodology in daily software engineering practice. The results of this project can mitigate this issue. To make the impact towards this direction, we plan to investigate the problem of adaptation tactic selection for self-adaptive systems. We also have contact with industry such as Lenovo Research and plan to apply the results to the interaction technology for emerging wearable devices. We will pay two visits to meet with Mr. Qian Ma and his team in Lenovo Research in Beijing, China.

Part of the research especially that described in WP2 is theoretical in nature. Nonetheless, the goals remain focused towards problems rooted in areas where they are of great practical interest. In particular, our results might have an impact on the model repair problem: given a model with parameters, if the model with the current value of the parameters fails to satisfy a property, the problem asks to find new values for the parameters so that the property is guaranteed to hold, while at the same time the cost of repair is minimised. They also can be applied to robust control, which aims to design controllers explicitly accounting for uncertainty, namely, to achieve robust performance and/or stability in the presence of bounded modelling errors. These problems turn out to be quite important in, for instance, distributed computing and control engineering. Our results could shed light on the research therein. In particular, for the Positive results -- improved algorithms and application of algorithms where previously there was none -- have the potential for the most immediate impact. On the other hand, negative results usually in the form of complexity lower bounds, indicate that we must look elsewhere for positive results.

Finally, we wish to share our results and ideas with industrial partners and academics at a one-day workshop held at Middlesex.