TLINet: Differentiable Neural Network Temporal Logic Inference

TL;DR

TLINet addresses the interpretability gap in data-driven temporal reasoning by learning STL formulas directly from time-series data via a differentiable neural-symbolic framework. It introduces a vectorized STL encoding (vSTL) and modular neural components for predicates, temporals, and Booleans, enabling end-to-end learning and subsequent decoding into compact STL formulas. To preserve STL semantics while enabling gradient-based optimization, it develops two sound max-approximation schemes—sparse softmax and averaged max/minmax—with regularizers to promote sparsity and compactness. The approach yields state-of-the-art classification performance with concise, interpretable specifications across naval surveillance, obstacle avoidance, and periodic signal tasks, highlighting practical impact for safe and transparent autonomous systems. The work also provides theoretical guarantees (soundness) for the proposed max-approximations and outlines future extensions to unsupervised learning scenarios.

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.

Figures (14)

• Figure 1: An example of a $5$-layer TLINet.
• Figure 2: The computation graph of the predicate module, where $\mathbf{a}$ and $b$ are parameters of the module.
• Figure 3: The sequence of robustness $r(t)=-s(t)+0.1$ for predicate $\mu:=s(t)< 0.1$ given a signal $\mathbf s$. The positive and negative robustness implies the degree of satisfaction and violation of the signal to the predicate, respectively.
• Figure 4: An example of time function. The time interval is $I=[4,8]$. The length of the signal is $13$. The time function with $\eta=0.1,0.5,1$ is shown in yellow, blue, and red, respectively.
• Figure 5: The procedure from signal $\mathbf s$ to the robustness vector $\mathbf{r}^v(\mathbf{s},\phi_1)$. The signal $\mathbf s$ is shown in red. The robustness vector of predicate $\mathbf{r}^v(\mathbf{s},\mu)$ is shown in yellow. The robustness padding vector of predicate $\mathbf{r}^v_p(\mathbf{s},\mu)$ is shown in green. The robustness vector $\mathbf{r}^v(\mathbf{s},\phi_1)$ is shown in blue.

Theorems & Definitions (19)

• Definition 1
• Definition 2
• Definition 3
• Definition 4: Robustness Vector
• Definition 5
• Proposition 1
• proof
• Example 1
• Definition 6: Time Function
• Remark 1