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.

Potential Impact:
Outside the academic community, our research has both commercial and non-commercial impact. As for the commercial impact, companies from various areas will be able to use the tools we develop (or they can develop their own tools based on our academic publications). These areas include mainly the industries where the correctness of results obtained from modelling is of utmost importance, making the usual approach by testing prone to missing important bugs in the systems. An example of such industry is medical engineering, where the devices developed, such as pacemakers or radiotherapy machines, need to work safely under any conditions. As a second example, systems such as air-traffic control will in the future exhibit a larger scale of automation, exposing the need for formal verification of the navigation algorithms used. As a third example, the energy industry has been undergoing major changes in recent years, with larger proportions of electricity supplied into the system coming from small domestic solar power-plants. This has brought about the challenge of designing the control of a grid so that power outages are prevented when the weather rapidly changes, influencing the amount of electricity produced.

As a result of making their systems more safe, the interested companies can achieve huge savings on the repairs of faults, and can minimise losses caused by making non-optimal decisions. At the same time, safer systems benefit the general public, not only in the most direct way of decreasing the number of accidents and injuries caused by faulty systems, but also in indirect ways. The availability of safer systems will result in savings for the companies, which can then be reflected in the customer prices. Further, regulators will be able to use the methods developed in this project to ensure that the systems used by companies follow the required rules and restrictions.

Last but not least, selected results of the project will be presented as an advanced part of courses taught in the part-time Software Engineering programme at Oxford University Department of Computer Science. The students of these courses are professionals with various backgrounds, which enables them to provide useful perspectives on the practical usability of the results, and to help identify new applications.