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.

翻译：从有限迹中学习线性时序逻辑（LTLf）公式是一个基础性研究问题，在人工智能、软件工程、编程语言、形式化方法、信息物理系统控制以及机器人学等领域均有应用。我们实现了一种名为Bolt的新型CPU工具，其在超过70%的基准测试中学习公式的速度比现有最优方法快100倍以上，且在98%的情况下能生成更小或等价的公式。我们的核心思路是利用布尔集合覆盖问题作为子程序，通过布尔连接词组合现有公式。得益于布尔集合覆盖组件，我们的方法在计算效率与公式规模之间实现了新颖的权衡。