Temporal Logic Sketching: A Computer-aided Approach to Writing Formal Specifications

当今复杂系统的工程过程需要对系统必须满足的规范有很好的理解。然而，将这种理解转化为正确和完整的规范是非常困难和容易出错的。关键的属性很容易被忽略，而且熟练掌握正式规范语言所需的培训工作可能与预期的收益不成比例。提议的项目旨在为如何弥合正式规范和工程师对复杂系统的直观理解之间的差距这一基本问题提供答案。它的目标是开发一种完全新颖的、计算机辅助的方法来编写正式规范，称为时序逻辑草图，并在开源软件工具中实现这种方法。愿景是未来的工程师编写部分规范（规范草图），同时省略难以形式化的部分。通过与工程师交互（例如，通过查询系统期望行为的示例），草图工具推断出开发人员心中的完整规范。为了进一步减轻规范负担，草图工具应该提供一个选项，以透明地将常见的“软约束”合并到结果规范中，例如健壮性或服务质量。该项目将重点关注四种规范语言，它们被认为是在验证和合成应用程序中表达时间属性的事实上的标准（因此被称为“时间逻辑草图”）：线性时间逻辑（LTL）、计算树逻辑（CTL）、CTL*和信号时间逻辑（STL）。特别是，它有三个主要目标：1)我们将扩展我们在学习LTL公式方面的初步工作，并将为上面列出的逻辑开发成熟的学习算法。通过使用数学优化技术，我们将设计我们的算法来产生“人类可解释”的公式。这个设计目标对这个项目至关重要，但直到最近才在机器学习社区引起关注。2)我们将开发时间逻辑草图的基本原理，并将其作为软件工具实现。与我们之前在基于学习的验证上的工作类似，我们将结合归纳技术（即上面的学习算法）和演绎技术（来自数学逻辑）。3)我们将开发LTL， CTL， CTL*和STL的扩展，通过设计，纳入鲁棒性和质量保证。与现有方法相反，这些扩展将不具有布尔值，而是具有多值语义，这允许对不同程度的满足进行推理。我们相信时序逻辑草图的原则将显著地改进编写形式化规范的过程（甚至超越时序逻辑）。这将克服在实践中广泛采用核查和合成技术的最大障碍之一。

The engineering process of today’s complex systems requires a good understanding of the specification that the system has to fulfill. However, translating this understanding into correct and complete specifications is notoriously hard and error-prone. Crucial properties are easy to miss and the training effort required to reach proficiency with formal specification languages can be disproportionate to the expected benefits.The proposed project seeks to provide answers to the fundamental question of how to bridge the gap between formal specifications and an engineer's intuitive understanding of a complex system. Its goal is to develop a completely novel, computer-aided approach to writing formal specifications, named temporal logic sketching, and to implement this approach in an open-source software tool. The vision is that a future engineer writes a partial specification (a specification sketch), while leaving out parts that are difficult to formalize. By interacting with the engineer (e.g., by querying for examples of the system's desired behavior), a sketching tool infers the complete specification the developer has in mind. To alleviate the specification burden further, the sketching tool should offer an option to transparently incorporate common "soft-constraints" into the resulting specification, such as robustness or quality of service.This project will focus on four specification languages that are considered the de facto standard for expressing temporal properties in verification and synthesis applications (hence the name "temporal logic sketching"): Linear Temporal Logic (LTL), Computational Tree Logic (CTL), CTL*, and Signal Temporal Logic (STL). In particular, it has three main objectives:1) We will expand our preliminary work on learning LTL formulas and will develop fully-fledged learning algorithms for the logics listed above. By using mathematical optimization techniques, we will design our algorithms to produce "human-interpretable" formulas. This design goal is essential for this project, but has only recently gained attention in the machine learning community.2) We will develop the fundamentals of temporal logic sketching and implement them as a software tool. Similar to our previous work on learning-based verification, we will combine inductive techniques (i.e., the learning algorithms above) and deductive techniques (from mathematical logic).3) We will develop extensions of LTL, CTL, CTL*, and STL that, by design, incorporate robustness and quality guarantees. Contrary to existing approaches, these extensions will not have a Boolean but a many-valued semantics, which permits reasoning about various degrees of satisfaction.We are convinced that the principles of temporal logic sketching will significantly improve the process of writing formal specifications (even beyond temporal logics). This will overcome one of the largest obstacles for a widespread adaptation of verification and synthesis technology in practice.