Towards comprehensive verification of stochastic systems

为了开发安全可靠的系统，通常需要建立系统的先进数学模型并对其性质进行正式验证。这需要开发相关的验证算法，因为模型的大小和计算速度通常是一个很大的挑战。这个项目关注的是开发算法来验证一种特殊类型的模型的属性，称为马尔可夫决策过程。这些模型对于正式描述显示概率选择和可控决策的系统是有用的。概率在许多系统中自然存在，例如作为系统组件的故障率，而可控选择对应于决定将哪个工作组件分配给哪个任务。马尔可夫决策过程的验证算法的目的是描述控制系统以达到给定属性或给出最坏情况的最佳可能方法。由于所需要的系统属性通常是非常复杂和连锁的，我们将考虑的属性是由几个较小的目标组成的“多目标查询”。这样的查询可能需要做出复杂的控制决策。这样的查询的一个例子是尽可能快地完成计算（目标1），同时最小化消耗的能量（目标2）。这就产生了目标之间的权衡，并提出了新的理论挑战。该项目的主要目标涉及验证算法的设计及其实施，最终将在能源网络建模的案例研究中进行评估。我们将从理论结果开始，继续到基于机器学习和近似技术的实际可用算法。我们的算法将作为一个免费的开源工具的一部分进行开发。这将是第一个允许将各种类型的目标组合到一个查询中，并以用户友好的方式将结果可视化的工具。该项目的产出将对故障安全系统至关重要和需要先进控制的领域产生影响。这些领域包括未来的智能电网、医疗保健、空中交通管制和交易算法。

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.