Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Learning Optimal Signal Temporal Logic Decision Trees for Classification: A Max-Flow MILP Formulation

Kaier Liang, Gustavo A. Cardona, Disha Kamale, Cristian-Ioan Vasile

TL;DR

The paper tackles the challenge of extracting interpretable temporal properties from labeled time-series by learning STL-based decision trees. It introduces a max-flow encoded MILP framework that jointly infers tree structure and PSTL primitives, with robustness- and flow-based constraints ensuring correct classification and interpretable formulae. Key contributions include a global optimization approach that reduces primitive redundancy, a flow-based formulation with complexity control via a regularization parameter, and demonstration on naval surveillance, trace datasets, and second-level STL primitives. The results show high classification accuracy and interpretable STL rules, highlighting the method's potential for scalable, interpretable temporal behavior analysis in real-world settings.

Abstract

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.

Learning Optimal Signal Temporal Logic Decision Trees for Classification: A Max-Flow MILP Formulation

TL;DR

The paper tackles the challenge of extracting interpretable temporal properties from labeled time-series by learning STL-based decision trees. It introduces a max-flow encoded MILP framework that jointly infers tree structure and PSTL primitives, with robustness- and flow-based constraints ensuring correct classification and interpretable formulae. Key contributions include a global optimization approach that reduces primitive redundancy, a flow-based formulation with complexity control via a regularization parameter, and demonstration on naval surveillance, trace datasets, and second-level STL primitives. The results show high classification accuracy and interpretable STL rules, highlighting the method's potential for scalable, interpretable temporal behavior analysis in real-world settings.

Abstract

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.
Paper Structure (18 sections, 2 theorems, 24 equations, 7 figures)

This paper contains 18 sections, 2 theorems, 24 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Preliminaries and Notation
  3. Signal Temporal Logic
  4. Problem Formulation
  5. Solution
  6. Flow constraints
  7. Node function constraints
  8. STL satisfaction constraints
  9. Robustness calculation
  10. Soundness constraints
  11. MILP formulation
  12. Problem simplification
  13. STL formula summary
  14. Case Studies
  15. Naval Surveillance
  16. ...and 3 more sections

Key Result

Theorem 1

Let $s$ be a signal and $\phi$ an STL formula. It holds $\rho(s, \phi, k) > 0 \Rightarrow (s, k) \models \phi$ for satisfaction and $\rho(s, \phi, k) < 0 \Rightarrow (s, k) \nmodels \phi$ for violation.

Figures (7)

  • Figure 1: Max flow classification tree.
  • Figure 2: Naval Surveillance Dataset
  • Figure 3:
  • Figure 4:
  • Figure 6: Performance comparison (a) Run time (b) Correct classification rate.
  • ...and 2 more figures

Theorems & Definitions (6)

  • Theorem 1: Soundness donze2010
  • Definition 1: Classification Tree
  • Definition 2: PSTL primitives
  • Proposition 1
  • proof
  • proof