Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Constrained LTL Specification Learning from Examples

Changjian Zhang, Parv Kapoor, Ian Dardik, Leyi Cui, Romulo Meira-Goes, David Garlan, Eunsuk Kang

TL;DR

This work tackles learning linear temporal logic (LTL) specifications from positive and negative traces by introducing constrained LTL learning, which lets users impose first-order constraints on the syntax of the learned formula and specify optimization goals. The authors encode the learning problem into $Alloy^{Max}$ and reduce it to MaxSAT, enabling efficient yet expressive search over formula structure with lasso-trace semantics and bounded formula size. The paper provides a detailed six-part encoding (syntax, semantics, problem-specific, learning objective, structural constraints, and optimization) and demonstrates the approach in ATLAS across specification mining, repair, and invariant weakening use cases, achieving competitive or superior performance to state-of-the-art methods. The results show that expressive constraints and MaxSAT-based optimization significantly broaden the applicability and quality of learned LTL formulas while maintaining practical efficiency for realistic problem sizes.

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.

Constrained LTL Specification Learning from Examples

TL;DR

This work tackles learning linear temporal logic (LTL) specifications from positive and negative traces by introducing constrained LTL learning, which lets users impose first-order constraints on the syntax of the learned formula and specify optimization goals. The authors encode the learning problem into and reduce it to MaxSAT, enabling efficient yet expressive search over formula structure with lasso-trace semantics and bounded formula size. The paper provides a detailed six-part encoding (syntax, semantics, problem-specific, learning objective, structural constraints, and optimization) and demonstrates the approach in ATLAS across specification mining, repair, and invariant weakening use cases, achieving competitive or superior performance to state-of-the-art methods. The results show that expressive constraints and MaxSAT-based optimization significantly broaden the applicability and quality of learned LTL formulas while maintaining practical efficiency for realistic problem sizes.

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.

Paper Structure

This paper contains 41 sections, 5 theorems, 14 equations, 9 figures, 1 table.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. Limitations of existing methods
  4. Proposed approach
  5. Summary
  6. Preliminaries
  7. Linear Temporal Logic
  8. LTL Learning from Examples
  9. Alloy and Alloy$^{Max}$
  10. Problem Formulation
  11. Constrained LTL Learning
  12. Syntactic Constraint $\Phi$
  13. Optimization Objective $\Psi$
  14. Technical Approach
  15. Syntax Encoding
  16. ...and 26 more sections

Key Result

Theorem 10.1

Given a constrained learning problem $\langle AP, \mathcal{S}, \Phi, \Psi \rangle$ and an upper bound of nodes $n$, a solution to the translated $\textnormal{Alloy}^{\textnormal{Max}}$ problem is an LTL formula that is consistent with $\mathcal{S}$, satisfies $\Phi$, and optimizes against $\Psi$.

Figures (9)

  • Figure 1: Overview of a constrained LTL learning problem in ATLAS.
  • Figure 2: A multi-processing algorithm under analysis.
  • Figure 3: A positive example trace of the algorithm in Figure \ref{['fig:peterson']}.
  • Figure 4: A negative example trace generated from the algorithm.
  • Figure 5: Abstract syntax of syntactic constraint $\Phi$.
  • ...and 4 more figures

Theorems & Definitions (5)

  • Theorem 10.1: Soundness
  • Theorem 10.2: Completeness
  • Theorem 10.3
  • Theorem 10.4
  • Theorem 10.5