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.