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

• Applicant: Professor Dr. Daniel Neider
• Subject Area: Theoretical Computer Science
• Term: from 2020 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 434592664

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.

• DFG Programme: Research Grants