{"ID":2863508,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2509.24616","arxiv_id":"2509.24616","title":"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.","short_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...","url_abs":"https://arxiv.org/abs/2509.24616","url_pdf":"https://arxiv.org/pdf/2509.24616v2","authors":"[\"Gabriel Bathie\",\"Nathanaël Fijalkow\",\"Théo Matricon\",\"Baptiste Mouillon\",\"Pierre Vandenhove\"]","published":"2025-09-29T11:20:20Z","proceeding":"cs.AI","tasks":"[\"cs.AI\",\"cs.FL\",\"cs.LO\"]","methods":"[]","has_code":false}