Scalable and quality-aware synthesis of reactive systems from linear temporal logic specifications

点击翻译按钮获取中文摘要

Ensuring the correct behaviour of critical systems, e.g. a flight control software, a power-plant controller, is paramount to the safe and reliable operation of such systems. Unfortunately, widely used techniques, such as testing the involved software in various settings, cannot guarantee the absence of undesired behaviour in general. Formal methods apply mathematically rigorous analyses to such questions and when applied successfully are able to guarantee the correct behaviour of the involved system. Reactive systems, i.e. non-terminating systems that interact with an environment, are often a suitable abstraction for the critical system that one wants to study. The desired behaviour is often specified in a temporal logic, especially linear temporal logic, which allows the specification of behaviour by relating different points in time. While model-checking, i.e. the automatic analysis to determine if a given system abstraction fulfils a given temporal logic specification, has been successfully transferred to industrial practice, synthesis of reactive systems, i.e. the automatic construction of a reactive systems from a temporal logic specification, has not been widely adopted. There are two factors that hinder the move from theory to practice: first, known algorithms are not able to handle large specifications needed to specify complex systems; second, known algorithms often yield implementations of reactive systems with poor quality, e.g. in terms of size, resource efficiency, and reaction time. The proposed project investigates new and unconventional approaches to the synthesis problem. The goal is to obtain algorithms that are able to process large specifications and that are able to produce implementations with a high level of quality. While the main motivation for this project is to address two factors standing in the way of industrial application, the project also wishes to contribute to the theory of automata and temporal logics by investigating fundamental questions that arise from the study of these new techniques.