EPSRC logo

Details of Grant 

EPSRC Reference: EP/M023656/1
Title: Towards comprehensive verification of stochastic systems
Principal Investigator: Kiefer, Dr S
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: University of Oxford
Scheme: First Grant - Revised 2009
Starts: 01 July 2015 Ends: 30 June 2017 Value (£): 97,590
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
27 Jan 2015 EPSRC ICT Prioritisation Panel - Jan 2015 Announced
Summary on Grant Application Form
In order to develop safe and reliable systems, advanced mathematical models of the systems are often created and their properties formally verified. This requires developing involved algorithms for verification, because the size of the models and the speed of the computation is often a big challenge. This project is concerned with developing algorithms for the verification of properties of one particular class of models, called Markov decision processes. These models are useful for formally describing systems exhibiting probabilistic choices and controllable decisions. Probability is present naturally in many systems, for instance as failure rates of system components, while the controllable choices correspond e.g. to deciding which of the working components to allocate for which task.

The aim of the verification algorithms for Markov decision processes is to describe the best possible way of controlling the system in order to achieve a given property, or to give the worst-case scenario. Acknowledging that the properties of systems that are required are often very complex and interlocked, the properties we will consider are given as "multi-objective queries" composed of several smaller objectives. Such queries can possibly require making complex control decisions. An example of such a query would be to finish the computation as fast as possible (objective 1), while minimising the amount of energy consumed (objective 2). This gives rise to trade-offs between the objectives, and poses new theoretical challenges.

The project's main aims concern the design of verification algorithms and their implementation, which will be ultimately evaluated on a case-study modelling an energy network. We will start from theoretical results, proceeding to practically usable algorithms based on machine-learning and approximation techniques. Our algorithms will be developed as part of a freely available open-source tool. This will be the first tool allowing to combine various types of objectives into one query, and to visualise the result in a user-friendly way.

The outputs of the project will have impact in areas where fail-safe systems are crucial, and where advanced control is required. Such areas include future smart energy grids, healthcare, air traffic control and trading algorithms.

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.ox.ac.uk