Learning Finite Linear Temporal Logic Specifications with a Specialized Neural Operator

Understand

Finite linear temporal logic ($\mathsf{LTL}_f$) is a powerful formal representation for modeling temporal sequences.

• We address the problem of learning a compact $\mathsf{LTL}_f$ formula from labeled traces of system behavior.
• We propose a novel neural network operator and evaluate the resulting architecture, Neural$\mathsf{LTL}_f$.
• Our approach includes a specialized recurrent filter, designed to subsume $\mathsf{LTL}_f$ temporal operators, to learn a highly accurate classifier for traces.