Conformalized Signal Temporal Logic Inference under Covariate Shift

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.

Signal Temporal Logic (STL) is an expressive formal language for specifying spatio-temporal requirements over real-valued, real-time signals. It has been widely used for the verification and synthesis of autonomous systems and cyber-physical systems. In practice, however, users often express their requirements in natural language rather than in structured STL formulas, making natural-language-to-STL translation a critical yet challenging task. Manual specification requires temporal-logic expertise and cannot scale, while prompting commercial LLM APIs incurs substantial token costs and may expose sensitive system requirements to third-party services, raising privacy concerns for industrial deployment. To address these challenges, we present ReasonSTL, a tool-augmented framework that adapts local open-source language models for natural-language-to-STL generation. ReasonSTL decomposes the translation process into explicit reasoning, deterministic tool calls, and structured formula construction. We further introduce process-rewarded training to supervise both tool-use trajectories and final formulas, together with STL-Bench, a bilingual, computation-aware benchmark grounded in real-world signals. Experiments show that a 4B model trained with ReasonSTL achieves state-of-the-art performance in both automatic metrics and human evaluations, demonstrating that ReasonSTL provides a transparent, low-cost, and privacy-preserving alternative for formal specification drafting.

Signal Temporal Logic (STL) offers verifiable task specifications and is crucial for safety-critical control. Yet STL planning remains challenging: exact optimization-based methods are often too slow, and learning-based methods struggle to generalize across varying environments. We propose a zero-shot STL planning solver for variable-map environments that generates feasible trajectories without retraining. By integrating a map-conditioned Transformer architecture with a lightweight heuristic, our approach effectively handles complex disjunctive (OR) subformulas. Furthermore, we leverage Transitive Reinforcement Learning (TRL) to ensure consistent temporal grounding and logical coherence across decomposed sub-tasks. Experiments on dynamic semantic maps with diverse obstacle layouts demonstrate consistent gains, highlighting the framework's superior zero-shot generalization to changing environments and broad STL coverage.