Learning Temporal Logic Properties: an Overview of Two Recent Methods

TL;DR

This paper reviews two recent methods for learning linear temporal logic formulas from examples, addressing noise robustness and minimality, with applications to system behavior inference.

Contribution

It summarizes two novel algorithms for inferring LTL formulas under different problem settings, including noisy labels and positive-only data.

Findings

Methods handle noisy and positive-only data scenarios.

Algorithms infer LTL, STL, and automata.

Addresses robustness and minimality in formula learning.

Abstract

Learning linear temporal logic (LTL) formulas from examples labeled as positive or negative has found applications in inferring descriptions of system behavior. We summarize two methods to learn LTL formulas from examples in two different problem settings. The first method assumes noise in the labeling of the examples. For that, they define the problem of inferring an LTL formula that must be consistent with most but not all of the examples. The second method considers the other problem of inferring meaningful LTL formulas in the case where only positive examples are given. Hence, the first method addresses the robustness to noise, and the second method addresses the balance between conciseness and specificity (i.e., language minimality) of the inferred formula. The summarized methods propose different algorithms to solve the aforementioned problems, as well as to infer other descriptions of temporal properties, such as signal temporal logic or deterministic finite automata.