Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LTL learning on GPUs

Mojtaba Valizadeh, Nathanaël Fijalkow, Martin Berger

TL;DR

The first GPU-based LTL learner is implemented using a novel form of enumerative program synthesis that has novel branch-free LTL semantics and handles traces at least 2048 times more numerous, and on average at least 46 times faster than existing state-of-the-art learners.

Abstract

Linear temporal logic (LTL) is widely used in industrial verification. LTL formulae can be learned from traces. Scaling LTL formula learning is an open problem. We implement the first GPU-based LTL learner using a novel form of enumerative program synthesis. The learner is sound and complete. Our benchmarks indicate that it handles traces at least 2048 times more numerous, and on average at least 46 times faster than existing state-of-the-art learners. This is achieved with, among others, novel branch-free LTL semantics that has $O(\log n)$ time complexity, where $n$ is trace length, while previous implementations are $O(n^2)$ or worse (assuming bitwise boolean operations and shifts by powers of 2 have unit costs -- a realistic assumption on modern processors).

LTL learning on GPUs

TL;DR

The first GPU-based LTL learner is implemented using a novel form of enumerative program synthesis that has novel branch-free LTL semantics and handles traces at least 2048 times more numerous, and on average at least 46 times faster than existing state-of-the-art learners.

Abstract

Linear temporal logic (LTL) is widely used in industrial verification. LTL formulae can be learned from traces. Scaling LTL formula learning is an open problem. We implement the first GPU-based LTL learner using a novel form of enumerative program synthesis. The learner is sound and complete. Our benchmarks indicate that it handles traces at least 2048 times more numerous, and on average at least 46 times faster than existing state-of-the-art learners. This is achieved with, among others, novel branch-free LTL semantics that has time complexity, where is trace length, while previous implementations are or worse (assuming bitwise boolean operations and shifts by powers of 2 have unit costs -- a realistic assumption on modern processors).
Paper Structure (13 sections, 2 theorems, 17 equations, 4 figures, 4 tables)

This paper contains 13 sections, 2 theorems, 17 equations, 4 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Formal preliminaries
  3. High-level structure of the algorithm
  4. In-memory representation of search space
  5. Relaxed uniqueness checks
  6. Divide & conquer
  7. Evaluation of algorithm performance
  8. Conclusion
  9. Worked examples of CS manipulation by bitshifts
  10. Correctness and complexity of branch-free semantics for temporal operators
  11. Related work: cache admission policies
  12. Related work: detailed comparison with Paresy ValizadehM:seabasreioag
  13. Scarlet's sample generation

Key Result

lemma 1

Let $cs$ be the characteristic sequence for $\phi$ over a trace of length $L$. The algorithm above computes the characteristic sequence for $\mathsf{F} \phi$. Assuming bitwise boolean operations and shifts by powers of two have unit costs, the complexity of the algorithm is $O(\log(L))$.

Figures (4)

  • Figure 1: High-level structure of our algorithm. LC is short for language cache.
  • Figure 2: Data representation in memory (simplified).
  • Figure 3: Here RS means random-splitting, DS deterministic-splitting. The numbers 16, 32, 64 are the used splitting window. Hsh is short for MuellerHash. The x-axis is annotated by $(trLen, \#N)$, giving the length of the single trace in $P$, and the cardinality $\# N$ of $N$. TO denotes timeout. Timeout is 2000 seconds. On the left, the y-axis gives the ratio $\frac{\text{cost of learned formula}}{\text{cost of overfitting}}$, the dotted line at 1.0 is the cost of overfitting.
  • Figure 4: Effects of masking on formula cost. Timeout is 200 seconds. Colours correspond to different $(P, N)$. The slight 'wobble' on all graphs is deliberately introduced for readability, and is not in the data.

Theorems & Definitions (4)

  • lemma 1
  • proof
  • lemma 2
  • proof