Skip to main content

Towards comprehensive verification of stochastic systems

1st July 2015 to 20th June 2017

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.

Sponsors

Principal Investigator

Vojtěch Forejt

People

Romain Brenguier

Share this: