Boolean set cover for LTL learning

In LTL learning we have positive and negative traces (finite words) and we want to find the shortest LTL formula that satisfies all the positive traces but none of the negatives ones. To help with LTL learning, we study the Boolean set cover problem: it is a generalization of the set cover problem where we allow union and intersection and try to obtain a set with all positives without the negatives. We use it to solve approximately but efficiently LTL learning instances. We first try to solve the instances by generating all LTL formulas of a bounded size, and then use the boolean set cover heuristics to find a short formula. We present different approaches and heuristics - principally a greedy one using D&C and a notion of 'score' and another using set covers - and compare their efficiency with Scarlet, a state-of-the-art tool for LTL learning. We also show how to generate a type of benchmarks called patterns (formulas, positive and negative traces) to test the limits of our algorithms. This is based on joint work with Gabriel Bathie, Nathanaël Fijalkow, Théo Matricon and Pierre Vandenhove.

Authors

• Baptiste Mouillon

Keywords

No keywords are indexed for this paper.