Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LTL$_f$ Learning Meets Boolean Set Cover

Gabriel Bathie, Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon, Pierre Vandenhove

TL;DR

This work addresses scalable learning of $ extbf{LTL}_f$ formulas from finite traces by coupling bottom-up enumeration with a Boolean Set Cover subroutine, enabling large expressive formulas while controlling growth via a specialized solver. The authors introduce Bolt, a CPU-based tool that integrates a VFB-style enumeration up to a size threshold with a beam-search Boolean Set Cover module, yielding substantial speedups and smaller formulas on a broad benchmark suite of over 15,000 tasks. Empirical results show Bolt outperforming state-of-the-art CPU approaches (and competing with GPU methods on compatible tasks), solving more tasks and delivering smaller or equal formulas in the majority of cases. The work also provides a comprehensive benchmark suite and a general, extensible framework that could be applied to other logics or specification languages, highlighting Boolean Set Cover as a broadly useful subroutine for scalable formula learning.

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.

LTL$_f$ Learning Meets Boolean Set Cover

TL;DR

This work addresses scalable learning of formulas from finite traces by coupling bottom-up enumeration with a Boolean Set Cover subroutine, enabling large expressive formulas while controlling growth via a specialized solver. The authors introduce Bolt, a CPU-based tool that integrates a VFB-style enumeration up to a size threshold with a beam-search Boolean Set Cover module, yielding substantial speedups and smaller formulas on a broad benchmark suite of over 15,000 tasks. Empirical results show Bolt outperforming state-of-the-art CPU approaches (and competing with GPU methods on compatible tasks), solving more tasks and delivering smaller or equal formulas in the majority of cases. The work also provides a comprehensive benchmark suite and a general, extensible framework that could be applied to other logics or specification languages, highlighting Boolean Set Cover as a broadly useful subroutine for scalable formula learning.

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.

Paper Structure

This paper contains 14 sections, 2 theorems, 1 equation, 4 figures, 2 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. LTLf Learning
  3. Problem Definition
  4. The VFB Algorithm
  5. Boolean Set Cover
  6. Definition and Properties of Boolean Set Cover
  7. Domination for positive Boolean Formulas
  8. Divide and Conquer
  9. Algorithm for Boolean Set Cover
  10. Experiments
  11. Benchmarks and State of the Art
  12. Experiments
  13. Perspectives
  14. Pseudocode for the VFB algorithm (Section \ref{['sec:ltl_learning']})

Key Result

Lemma 1

Let $P$, $N$, $\mathcal{F}$ be an instance of Boolean Set Cover. There exists a positive Boolean formula $\theta$ such that $\llbracket\theta\rrbracket = P$ if and only if for all $p\in P$, $n\in N$, there is $F\in\mathcal{F}$ such that $p\in F$ and $n\notin F$. Moreover, when it exists, there is su

Figures (4)

  • Figure 1: Overview of $\textbf{LTL}_f\xspace$ Learning with Boolean Set Cover
  • Figure 2: Characteristic sequences and table of $\varphi = \mathop{\textbf{X!}} a$ with $P = \{aabaa, baaa\}$ and $N = \{abab, aab\}$. We also use characteristic vector for the vector of all first bits of the characteristic sequences. Looking at the characteristic vector suffices to check whether $\varphi$ is a solution: it must have $1$'s at all positions of $P$ and $0$'s at all positions of $N$. However, we need to keep in memory the whole characteristic table to check for observational equivalence.
  • Figure 3: Comparison of running times (logarithmic axes) between Scarlet Raha.Roy.ea:2024 and Bolt. The diagonal lines represent ratios of time between the two tools: from bottom to top, Bolt is $100$x faster, $10$x faster, equal, $10$x slower, and $100$x slower than Scarlet. Tasks that time out are assumed to be $200$ s so that they are apart in the plot. The timeout used in practice is $60$ s. The color represents the ratio of the size of the formula returned by Bolt against the size of the formula returned by Scarlet.
  • Figure 4: Ablation study: removing Boolean Set Cover.

Theorems & Definitions (3)

  • Lemma 1: Existence of a solution
  • Definition 2
  • Lemma 3