Towards comprehensive verification of stochastic systems

Lead Research Organisation: UNIVERSITY OF OXFORD
Department Name: Computer Science

Abstract

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.

Planned 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.
 
Description In the paper "Robust Equilibria in Mean-Payoff Games", we study the problem of finding robust equilibria in multiplayer concurrent games with mean payoff objectives. A (k, t)-robust equilibrium is a strategy profile such that no coalition of size k can improve the payoff of one its member by deviating, and no coalition of size t can decrease the payoff of other players. While deciding whether there exists such equilibria is undecidable in general, we suggest algorithms for two meaningful restrictions on the complexity of strategies. The first restriction concerns memory. We show that we can reduce the problem of the existence of a memoryless robust equilibrium to a formula in the (existential) theory of reals. The second restriction concerns randomisation. We show that the existence of robust equilibria can be decided in polynomial space, and that the decision problem is PSPACE-complete.

In the paper "Optimal Assumptions for Synthesis", we study the problem constructing a correct system from its specification. This often requires assumptions about the behaviour of the environment and it is difficult for the designer to identify the assumptions that ensures the existence of a correct controller and that are not stronger than necessary. In this work, given a specification, we identify the weakest assumptions that ensure the existence of a controller. We also consider two important classes of assumptions: the ones that can be ensured by the environment and assumptions that restricts only inputs of the systems. We show that optimal assumptions correspond to a classical class of strategies in game theory called admissible strategies. Using these correspondences, we then propose an algorithm for computing optimal assumptions that can be ensured by the environment.

In the paper "Admissibility in Quantitative Graph Games", we extend the study of admissible strategies to games of infinite duration with quantitative objectives. First, we show that, under the assumption that optimal strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using some notion of adversarial and cooperative values for history of the games, and we characterize the set of outcomes that are compatible with admissible strategies. Finally, we show how these characterisations can be used to design algorithms to decide relevant verification and synthesis problems.

In the paper "Decidability Results for Multi-objective Stochastic Games", we study stochastic two-player turn-based games in which the objective of one player is to ensure several infinite-horizon total reward objectives, while the other player attempts to spoil at least one of the objectives. The games have previously been shown not to be determined, and an approximation algorithm for computing a Pareto curve has been given. The major drawback of the existing algorithm is that it needs to compute Pareto curves for finite horizon of increasing length, and the size of these Pareto curves can grow unboundedly, even when the infinite-horizon Pareto curve is small. By adapting existing results, we first give an algorithm that computes the Pareto curve for determined games. Then, as the main result of the paper, we show that for the natural class of stopping games and when there are two reward objectives, the problem of deciding whether a player can ensure satisfaction of the objectives with given thresholds is decidable.
Exploitation Route Thanks to our relatively high-profile publications that resulted from the grant, our work is already being cited by other research groups. We expect this continue and increase. Our work is stimulating further research in related areas. Out work lies at the intersection of computer-aided verification and theoretical computer science. Our work grows a vital bridge between these areas, allowing cross-fertilisation.
Sectors Digital/Communication/Information Technologies (including Software)
URL https://www.cs.ox.ac.uk/people/romain.brenguier/