# LTL learning on GPUs

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 35 references that are in the map.
- First posted on arXiv 19 Feb 2024.

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

- [Learning Linear Temporal Properties](https://mlsanity.com/paper/1806.03953/) (2018)
- [The Complexity of Learning Linear Temporal Formulas from Examples](https://mlsanity.com/paper/2102.00876/) (2021)
- [Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic](https://mlsanity.com/paper/2110.06726/) (2021)
- [Learning Concise Models from Long Execution Traces](https://mlsanity.com/paper/2001.05230/) (2020)
- [Search-Based Regular Expression Inference on a GPU](https://mlsanity.com/paper/2305.18575/) (2023)
- [WarpCore: A Library for fast Hash Tables on GPUs](https://mlsanity.com/paper/2009.07914/) (2020)
- [Learning temporal formulas from examples is hard](https://mlsanity.com/paper/2312.16336/) (2023)

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

- [Learning Probabilistic Temporal Logic Specifications for Stochastic Systems](https://mlsanity.com/paper/2505.12107/) (2025)
- [GPU accelerated program synthesis: Enumerate semantics, not syntax!](https://mlsanity.com/paper/2504.18943/) (2025)
- [LTLf Learning Meets Boolean Set Cover](https://mlsanity.com/paper/2509.24616/) (2025)
- [Interpretable Early Failure Detection via Machine Learning and Trace Checking-based Monitoring](https://mlsanity.com/paper/2508.17786/) (2025)
- [GPU-Accelerated Synthesis of Mixed-Boolean Arithmetic: Beyond Caching](https://mlsanity.com/paper/2605.08243/) (2026)
- [On Synthesis of Metric Interval Temporal Logics](https://mlsanity.com/paper/2609.01032/) (2026)

## Abstract (arXiv)

Linear temporal logic (LTL) is widely used in industrial verification. LTL formulae can be learned from traces. Scaling LTL formula learning is an open problem. We implement the first GPU-based LTL learner using a novel form of enumerative program synthesis. The learner is sound and complete. Our benchmarks indicate that it handles traces at least 2048 times more numerous, and on average at least 46 times faster than existing state-of-the-art learners. This is achieved with, among others, novel branch-free LTL semantics that has O(log n) time complexity, where n is trace length, while previous implementations are O(n2) or worse (assuming bitwise boolean operations and shifts by powers of 2 have unit costs -- a realistic assumption on modern processors).