Towards comprehensive verification of stochastic systems
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.