Temporal logic specifications play an important role in a wide range of software analysis tasks, such as model checking, automated synthesis, program comprehension, and runtime monitoring. Given a set of positive and negative examples, specified as traces, LTL learning is the problem of synthesizing a specification, in linear temporal logic (LTL), that evaluates to true over the positive traces and false over the negative ones. In this paper, we propose a new type of LTL learning problem called constrained LTL learning, where the user, in addition to positive and negative examples, is given an option to specify one or more constraints over the properties of the LTL formula to be learned. We demonstrate that the ability to specify these additional constraints significantly increases the range of applications for LTL learning, and also allows efficient generation of LTL formulas that satisfy certain desirable properties (such as minimality). We propose an approach for solving the constrained LTL learning problem through an encoding in a first-order relational logic and reduction to an instance of the maximal satisfiability (MaxSAT) problem. An experimental evaluation demonstrates that ATLAS, an implementation of our proposed approach, is able to solve new types of learning problems while performing better than or competitively with the state-of-the-art tools in LTL learning.

翻译：时序逻辑规范在广泛的软件分析任务中扮演着重要角色，例如模型检验、自动综合、程序理解和运行时监控。给定一组以迹形式指定的正例和负例，线性时序逻辑学习旨在综合出一个线性时序逻辑规范，使其在正例迹上求值为真，在负例迹上求值为假。本文提出了一种新型的线性时序逻辑学习问题，称为约束线性时序逻辑学习。在该问题中，除了正例和负例，用户还可以选择指定一个或多个关于待学习线性时序逻辑公式属性的约束。我们证明，指定这些额外约束的能力显著扩展了线性时序逻辑学习的应用范围，并且能够高效生成满足特定期望属性（如最小性）的线性时序逻辑公式。我们提出了一种通过在一阶关系逻辑中编码并规约为最大可满足性问题实例来解决约束线性时序逻辑学习问题的方法。实验评估表明，我们方法的具体实现ATLAS能够解决新型学习问题，同时在线性时序逻辑学习方面的性能优于或可与最先进的工具相媲美。