Constrained LTL Specification Learning from Examples

TL;DR

This paper introduces constrained LTL learning, allowing users to specify additional constraints, which broadens applications and improves efficiency in synthesizing temporal logic specifications from examples.

Contribution

The paper presents a novel constrained LTL learning framework, encoding it into MaxSAT, and demonstrates its effectiveness through the ATLAS implementation.

Findings

ATLAS solves new LTL learning problems efficiently.

Constrained learning increases application scope.

Performance is competitive with state-of-the-art tools.

Abstract

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 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.