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

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

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.