LTL$_f$ Learning Meets Boolean Set Cover
Abstract
Learning formulas in Linear Temporal Logic (LTLf) from finite traces is a fundamental research problem which has found applications in artificial intelligence, software engineering, programming languages, formal methods, control of cyber-physical systems, and robotics. We implement a new CPU tool called Bolt improving over the state of the art by learning formulas more than 100x faster over 70% of the benchmarks, with smaller or equal formulas in 98% of the cases. Our key insight is to leverage a problem called Boolean Set Cover as a subroutine to combine existing formulas using Boolean connectives. Thanks to the Boolean Set Cover component, our approach offers a novel trade-off between efficiency and formula size.
Cite
@article{arxiv.2509.24616,
title = {LTL$_f$ Learning Meets Boolean Set Cover},
author = {Gabriel Bathie and Nathanaël Fijalkow and Théo Matricon and Baptiste Mouillon and Pierre Vandenhove},
journal= {arXiv preprint arXiv:2509.24616},
year = {2026}
}
Comments
Full version of TACAS 2026 conference paper. 24 pages, 4 figures