Learning Linear Temporal Properties

TL;DR

This paper introduces two new algorithms for learning Linear Temporal Logic formulas from examples, one optimized for minimality and the other for scalability, demonstrated on synthetic and real-world data.

Contribution

It presents two novel algorithms for LTL formula learning: one SAT-based for minimal formulas, and another combining SAT with decision trees for scalability.

Findings

The SAT-based algorithm produces minimal LTL formulas consistent with data.

The combined algorithm scales to hundreds of examples but does not guarantee minimality.

Both algorithms perform well on synthetic benchmarks and real-world protocol data.

Abstract

We present two novel algorithms for learning formulas in Linear Temporal Logic (LTL) from examples. The first learning algorithm reduces the learning task to a series of satisfiability problems in propositional Boolean logic and produces a smallest LTL formula (in terms of the number of subformulas) that is consistent with the given data. Our second learning algorithm, on the other hand, combines the SAT-based learning algorithm with classical algorithms for learning decision trees. The result is a learning algorithm that scales to real-world scenarios with hundreds of examples, but can no longer guarantee to produce minimal consistent LTL formulas. We compare both learning algorithms and demonstrate their performance on a wide range of synthetic benchmarks. Additionally, we illustrate their usefulness on the task of understanding executions of a leader election protocol.