ScanSTL: Parallel Robustness Evaluation for Signal Temporal Logic

Abstract

Repeated evaluation and differentiation of Signal Temporal Logic (STL) robustness can become a computational bottleneck in robot planning and control. Sequential temporal recurrences limit parallelism, while dense masking increases memory requirements. We propose ScanSTL, which combines associative temporal aggregation with parallel scans and ordered block reductions. Eventually and Always use range extrema, while inclusive strong Until composes compact segment representations. A common range engine handles bounded and shifted intervals, including the guards required before delayed Until witnesses. Each exact temporal operator computes complete robustness traces with linear work and storage and logarithmic parallel depth on uniformly sampled finite signals. An open source JAX implementation supports automatic differentiation, batching, and compilation.

We compare ScanSTL with STLCG and STLCG++ using CPU and GPU operator benchmarks and nine composed specifications. Across these nine specifications at 512 samples, ScanSTL achieves geometric mean speedups of 243× for forward evaluation and 104× for gradient computation over STLCG++ in JAX on the CPU. On an RTX 5090 GPU, ScanSTL evaluates unbounded Until over more than two million samples with median times below 0.1 ms for forward evaluation and 0.25 ms for gradient computation. Simulated escort and patrol experiments with a robot dog further demonstrate faster repair of violating plans and greater solver capacity in model predictive control.

How does ScanSTL work?

STLCG evaluates temporal recurrences sequentially. STLCG++ exposes parallelism through dense masks. ScanSTL combines compact segment representations through associative scans and ordered range reductions, reusing computations across temporal windows. The same range engine supports Eventually, Always, and inclusive strong Until, including bounded intervals and the guards before delayed Until witnesses.

Choose a method, then press play to see how it works.

The animations illustrate the computation. Their playback speed does not represent measured runtime.

Scaling to longer traces

We compare forward evaluation and gradient computation on CPU and GPU. ScanSTL is faster at every shared CPU test point. On GPU, dense masking remains competitive for short unary traces, while ScanSTL offers a clear advantage for Until and supports much longer traces.

Unbounded operators [0, ∞]

Unbounded Eventually, Always, and Until runtime versus trace length. CPU results occupy the top row and GPU results the bottom row. ScanSTL continues to longer traces while maintaining low evaluation cost.

Bounded operators [5, 15]

CPU and GPU scaling for bounded Eventually, Always, and Until with the interval from 5 to 15 samples.

Shifted unbounded operators [5, ∞]

CPU and GPU scaling for shifted unbounded operators with a lower bound of 5 samples.

The gains persist in composed specifications

Across nine formulas and five horizons, ScanSTL is faster than both JAX baselines in forward evaluation and gradient computation at every tested combination. At 512 samples, its geometric mean speedups over STLCG++ are 243× forward and 104× for gradients on CPU. The formulas include nested operators, bounded Until, response requirements, and multiple clauses.

Results for all nine formulas

Forward and gradient CPU runtimes for nine composed STL formulas, comparing ScanSTL with STLCG and STLCG++ in JAX.

Escort and patrol with a robot dog

A simulated robot dog, modeled as a unicycle, escorts a person to a safe area, visits patrol locations A and B, and returns to its dock. The person can cross the robot exclusion region, while the robot must stay outside it. Model predictive control repeatedly updates the plan as the person moves.

Execution, local MPC objective, and verified margin

Representative robot dog execution, changing local MPC objective, and a positive exact margin for safety and escort proximity through the Until witness.

BibTeX

@article{alcan2026scanstl,
          author  = {Gokhan Alcan},
          title   = {ScanSTL: Parallel Robustness Evaluation for Signal Temporal Logic}, 
          journal = {arXiv preprint arXiv:2610.07346},
          year    = {2026}
}

Acknowledgment

This work was supported by the Research Council of Finland Project under Grant 370881 and by the NVIDIA Academic Grant Program through the provision of RTX PRO 6000 Blackwell Max-Q GPUs.

References

STLCG. K. Leung, N. Aréchiga and M. Pavone, “Backpropagation Through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods,” The International Journal of Robotics Research, 42(6), 356–370, 2023.
STLCG++. P. Kapoor, K. Mizuta, E. Kang and K. Leung, “STLCG++: A Masking Approach for Differentiable Signal Temporal Logic Specification,” IEEE Robotics and Automation Letters, 10(9), 9240–9247, 2025.