This paper presents a novel framework for inferring timed temporal logic properties from data. The dataset comprises pairs of finite-time system traces and corresponding labels, denoting whether the traces demonstrate specific desired behaviors, e.g. whether the ship follows a safe route or not. Our proposed approach leverages decision-tree-based methods to infer Signal Temporal Logic classifiers using primitive formulae. We formulate the inference process as a mixed integer linear programming optimization problem, recursively generating constraints to determine both data classification and tree structure. Applying a max-flow algorithm on the resultant tree transforms the problem into a global optimization challenge, leading to improved classification rates compared to prior methodologies. Moreover, we introduce a technique to reduce the number of constraints by exploiting the symmetry inherent in STL primitives, which enhances the algorithm's time performance and interpretability. To assess our algorithm's effectiveness and classification performance, we conduct three case studies involving two-class, multi-class, and complex formula classification scenarios.

翻译：本文提出了一种从数据中推断时序逻辑属性的新框架。数据集包含有限时间系统轨迹与对应标签的配对，标签表示轨迹是否展示特定期望行为，例如船舶是否遵循安全航线。我们提出的方法利用基于决策树的技术，通过原始公式推断信号时序逻辑分类器。我们将推断过程形式化为混合整数线性规划优化问题，通过递归生成约束来确定数据分类与树结构。在生成的树上应用最大流算法，将问题转化为全局优化挑战，从而实现了相较于现有方法更高的分类准确率。此外，我们提出了一种利用信号时序逻辑原始公式内在对称性来减少约束数量的技术，这提升了算法的时间性能与可解释性。为评估算法的有效性与分类性能，我们开展了三个案例研究，涵盖二分类、多分类及复杂公式分类场景。