STLCG++: A Masking Approach for Differentiable Signal Temporal Logic Specification
Parv Kapoor, Kazuki Mizuta, Eunsuk Kang, Karen Leung
AI summary
Problem
Existing methods for evaluating and differentiating Signal Temporal Logic (STL) robustness rely on sequential recurrent computations, which become inefficient and slow for long time sequences, hindering their use in real-time robotics and gradient-based optimization.
Approach
Inspired by transformer attention mechanisms, the method unrolls time-series signals into multi-dimensional arrays and applies binary masks to compute robustness traces simultaneously across all timesteps, enabling full parallelization and GPU acceleration.
Key results
- Parallelized STL robustness evaluation and backpropagation via masking
- First differentiation of STL time interval bounds using smoothing
- Significant computational speed-ups over recurrent STLCG baselines
- Open-source JAX and PyTorch libraries validated on three robotics use cases
Why it matters
It enables efficient, gradient-based optimization of long-horizon spatio-temporal robotic behaviors, making formal STL specifications practical for real-time control, planning, and deep learning workflows.
Abstract
Signal Temporal Logic (STL) offers a concise yet expressive framework for specifying and reasoning about spatio- temporal behaviors of robotic systems. Attractively, STL admits the notion of robustness, the degree to which an input signal satisfies or violates an STL specification, thus providing a nuanced evaluation of system performance. In particular, the differentiability of STL robustness enables direct integration to robotic workflows that rely on gradient-based optimization, such as trajectory optimization and deep learning. However, existing approaches to evaluating and differentiating STL robustness rely on recurrent computations, which become inefficient with longer sequences, limiting their use in time-sensitive applications. In this paper, we present STLCG++, a masking-based approach that parallelizes STL robustness evaluation and backpropagation across timesteps, achieving significant speed-ups compared to a recurrent approach. We also introduce a smoothing technique to enable the differentiation of time interval bounds, thereby expanding STL’s applicability in gradient-based optimization tasks involving spatial and temporal variables. Finally, we demon- strate STLCG++’s benefits through three robotics use cases and provide JAX and PyTorch libraries for seamless integration into modern robotics workflows. Project website with demo and code: https://uw-ctrl.github.io/stlcg/.