LTL$_f$ Learning Meets Boolean Set Cover
This addresses a fundamental problem in AI and formal methods with broad applications, though it appears incremental as it builds on existing methods with a new trade-off.
The paper tackles the problem of learning Linear Temporal Logic formulas from finite traces by implementing a CPU tool called Bolt that learns formulas over 100x faster on 70% of benchmarks and produces smaller or equal formulas in 98% of cases.
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.