TLINet: Differentiable Neural Network Temporal Logic Inference

TL;DR

TLINet is a neural-symbolic framework that learns interpretable Signal Temporal Logic formulas from data using differentiable computation, improving over existing methods in interpretability, expressibility, and efficiency.

Contribution

Introduces TLINet, a differentiable neural network framework for learning STL formulas, with novel approximation methods for max operators ensuring correctness.

Findings

Outperforms state-of-the-art baselines in interpretability

Achieves more compact and expressive STL formulas

Demonstrates improved computational efficiency

Abstract

There has been a growing interest in extracting formal descriptions of the system behaviors from data. Signal Temporal Logic (STL) is an expressive formal language used to describe spatial-temporal properties with interpretability. This paper introduces TLINet, a neural-symbolic framework for learning STL formulas. The computation in TLINet is differentiable, enabling the usage of off-the-shelf gradient-based tools during the learning process. In contrast to existing approaches, we introduce approximation methods for max operator designed specifically for temporal logic-based gradient techniques, ensuring the correctness of STL satisfaction evaluation. Our framework not only learns the structure but also the parameters of STL formulas, allowing flexible combinations of operators and various logical structures. We validate TLINet against state-of-the-art baselines, demonstrating that our approach outperforms these baselines in terms of interpretability, compactness, rich expressibility, and computational efficiency.