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.