Learning Linear Temporal Properties
This work addresses the challenge of automated specification mining for formal verification, offering practical tools for domains like protocol analysis, though it is incremental in improving scalability over existing methods.
The paper tackles the problem of learning Linear Temporal Logic (LTL) formulas from examples by presenting two algorithms: one that guarantees minimal formulas using SAT-based reduction but may not scale well, and another that combines SAT with decision trees for better scalability at the cost of minimality, demonstrating performance on synthetic benchmarks and a leader election protocol.
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.