# Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic

arXiv: https://arxiv.org/abs/2110.06726 · HTML: https://mlsanity.com/paper/2110.06726/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 65 references that are in the map.
- First posted on arXiv 13 Oct 2021.

## Builds on (most cited first, 6 of 6)

- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [Explaining Multi-stage Tasks by Learning Temporal Logic Formulas from Suboptimal Demonstrations](https://mlsanity.com/paper/2006.02411/) (2020)
- [The Complexity of Learning Linear Temporal Formulas from Examples](https://mlsanity.com/paper/2102.00876/) (2021)
- [Learning Interpretable Models in the Property Specification Language](https://mlsanity.com/paper/2002.03668/) (2020)
- [Learning Linear Temporal Properties from Noisy Data: A MaxSAT Approach](https://mlsanity.com/paper/2104.15083/) (2021)
- [Learning Concise Models from Long Execution Traces](https://mlsanity.com/paper/2001.05230/) (2020)

## Built on by (most cited first, 9 of 9)

- [Learning Interpretable Temporal Properties from Positive Examples Only](https://mlsanity.com/paper/2209.02650/) (2022)
- [LTL learning on GPUs](https://mlsanity.com/paper/2402.12373/) (2024)
- [Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic](https://mlsanity.com/paper/2310.17410/) (2023)
- [Learning Probabilistic Temporal Logic Specifications for Stochastic Systems](https://mlsanity.com/paper/2505.12107/) (2025)
- [Reverse Engineering of Temporal Queries Mediated by LTL Ontologies](https://mlsanity.com/paper/2305.01248/) (2023)
- [Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba](https://mlsanity.com/paper/2405.20917/) (2024)
- [LTLf Learning Meets Boolean Set Cover](https://mlsanity.com/paper/2509.24616/) (2025)
- [Learning Interpretable Classifiers for PDDL Planning](https://mlsanity.com/paper/2410.10011/) (2024)
- [Automata Learning of Preferences over Temporal Logic Formulas from Pairwise Comparisons](https://mlsanity.com/paper/2505.18030/) (2025)

## Abstract (arXiv)

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.