Details of Grant 

EPSRC Reference:	EP/P00430X/2
Title:	Perturbation Analysis for Probabilistic Verification
Principal Investigator:	Chen, Dr T
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science and Information Systems
Organisation:	Birkbeck College
Scheme:	First Grant - Revised 2009
Starts:	02 September 2017	Ends:	30 November 2018	Value (£):	85,032
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.bbk.ac.uk/