Yixuan Wang, Danyang Li, Matthew Cleaveland, Roberto Tron, Mingyu Cai
Abstract
Signal Temporal Logic (STL) inference provides interpretable formulas for time series classification. For multiclass classification, however, accurate predictions do not necessarily ensure that the inferred formulas are satisfied consistently with the true class. We introduce the positive satisfaction rate and codeword satisfaction rate to quantify satisfaction of required formulas and consistency with the complete class codeword, respectively. We develop a two-stage procedure that first learns discriminative formulas using a margin-based objective and then refines predicate thresholds toward a small positive robustness target while fixing the formula structure and temporal intervals. Satisfaction and ranking penalties discourage violations of required formulas and loss of class separation. The decoding loss is used as a nonconformity score and calibrated separately for each class, providing finite-sample class-conditional coverage under intra-class exchangeability. Experiments on naval, synthetic, and robot manipulation trajectories demonstrate discrepancies between classification accuracy and formula satisfaction. The results further reveal a data-dependent tradeoff between robustness tightness and satisfaction, while class-conditional calibration mitigates undercoverage that can be hidden by pooled calibration.
Class-Conditional Conformal STL Inference
The proposed framework combines multiclass STL inference with explicit specification-satisfaction evaluation and class-conditional uncertainty calibration. Discriminative STL formulas are first learned, after which predicate thresholds are refined toward tighter satisfaction boundaries while limiting losses in satisfaction and class separation. The resulting decoding loss is then calibrated separately for each class to construct prediction sets with finite-sample class-conditional coverage.
Motivation
Multiclass STL inference is typically evaluated by classification accuracy, but accurate predictions do not necessarily imply that trajectories satisfy the specifications associated with their true classes. Moreover, discriminative learning does not explicitly encourage tight formulas, and tightening predicate thresholds may trade off against satisfaction and class separation. Finally, marginal uncertainty calibration can conceal substantial coverage differences across classes. These limitations motivate jointly evaluating specification satisfaction, refinement tightness, and class-conditional predictive uncertainty.
Method
Discriminative Multiclass STL Learning: A set of STL formulas is first learned to distinguish among multiple classes. Their robustness values are combined through a class-dependent decoding loss, and a ranking objective encourages the true class to have a lower decoding loss than competing classes.
Tightness Refinement: After the discriminative model is selected, the formula structure and temporal intervals are fixed, while only predicate thresholds are refined. The refinement moves required positive robustness values toward a small positive target, while satisfaction, ranking, and anchor penalties limit losses in formula satisfaction, class separation, and threshold stability.
Class-Conditional Conformal Calibration: The decoding loss of the selected model is used as the nonconformity score. Calibration is performed separately for each class, producing class-specific thresholds and prediction sets with finite-sample class-conditional coverage under within-class exchangeability.
Experiment
Dataset
Naval (3 classes), Synthetic (7 classes), CALVIN (12 classes)
(a) Naval
(b) Synthetic
(c) CALVIN
Results
(a) Acuracy, satisfaction rates, and mean positive robustness on the test split.
Figure1: Conformal prediction with the refined models, standard against class conditional calibration