Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic

TL;DR

This paper presents a scalable, anytime algorithm for learning larger fragments of linear temporal logic (LTL) formulas from traces, improving on previous methods in size and computational efficiency.

Contribution

The authors introduce a novel algorithm that can construct significantly larger LTL formulas and is capable of providing intermediate results without exhaustive computation.

Findings

The algorithm scales to formulas an order of magnitude larger than previous methods.

It is an anytime algorithm that often outputs a usable formula before completion.

Performance evaluated successfully on publicly available benchmarks.

Abstract

Linear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and many other areas. We consider the problem of learning LTL formulas for classifying traces; despite a growing interest of the research community, existing solutions suffer from two limitations: they do not scale beyond small formulas, and they may exhaust computational resources without returning any result. We introduce a new algorithm addressing both issues: our algorithm is able to construct formulas an order of magnitude larger than previous methods, and it is anytime, meaning that it in most cases successfully outputs a formula, albeit possibly not of minimal size. We evaluate the performances of our algorithm using an open source implementation against publicly available benchmarks.