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.

翻译：从数据中提取系统行为的正式描述日益受到关注。信号时序逻辑（STL）是一种富有表现力的形式化语言，用于描述具有可解释性的时空属性。本文介绍了TLINet，一种用于学习STL公式的神经符号框架。TLINet中的计算是可微的，使得在训练过程中能够使用现成的基于梯度的工具。与现有方法相比，我们引入了专门针对时序逻辑梯度技术设计的max算子近似方法，确保了STL满足性评估的正确性。我们的框架不仅学习STL公式的结构，还学习其参数，允许灵活的算子组合及多种逻辑结构。我们将TLINet与最先进的基线方法进行了验证，结果表明我们的方法在可解释性、紧凑性、丰富表达力和计算效率方面均优于这些基线方法。