Source-linked AI summary
ScanSTL: Parallel Robustness Evaluation for Signal Temporal Logic
Gokhan Alcan
TL;DR
Repeated STL robustness and gradient evaluation can bottleneck robot planning and control when temporal recurrences limit parallelism or dense masks consume substantial storage. ScanSTL uses associative scans and ordered range reductions for exact temporal evaluation. Benchmarks and simulated robot tasks report computational gains, faster verified plan repair, and greater MPC solver capacity.
Problem
Repeated evaluation of complete STL robustness traces and gradients is costly for planning and control, while recurrent dependencies and dense masks constrain temporal evaluation.
Source: §I · p. 1Method
ScanSTL combines associative scans and ordered range reductions to compute exact robustness traces, with a JAX implementation supporting automatic differentiation.
Source: §I · pp. 1–2, §VI · p. 8Results
Benchmarks show substantial computational gains, particularly for Until and composed specifications, while simulated robot tasks show faster verified plan repair and greater MPC solver capacity.
Source: §VI · p. 8Takeaways & Limitations
The reported computational gains accompany faster verified plan repair and greater solver capacity in simulated escort-and-patrol planning and MPC.
Source: §VI · p. 8Smooth Until remains a quadratic reference, with O(T^2) work and storage for the unbounded path.
Source: E. Smooth Robustness · p. 5
Abstract
from arXiv · showhide
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 times for forward evaluation and 104 times 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.
I. INTRODUCTION
STL robustness supports trajectory verification and optimization, but repeated evaluation of complete traces and gradients is costly when temporal operators are sequential or memory-intensive. ScanSTL combines associative scans and ordered reductions to compute exact traces with linear work and storage and logarithmic parallel depth.
I. INTRODUCTION
- Repeated specification and gradient evaluations make complete robustness traces a computational cost in trajectory optimization and control.STL robustness values indicate satisfaction or violation and provide a margin; optimizer iterations evaluate the specification and its gradient, while nested operators need values at multiple starting times.Source: §I · p. 1
- ScanSTL combines associative aggregation, scans, and ordered reductions to compute exact complete traces without full-horizon sequential recurrences or dense temporal masks.Eventually and Always use range extrema, while inclusive strong Until composes compact segment representations; each temporal operator has linear work and storage and logarithmic parallel depth.Source: §I · pp. 1–2
A. Control Using STL Robustness
- STLCG supports differentiable robustness optimization, while STLCG++ [8] exposes temporal parallelism using masks; ScanSTL addresses their recurrence-versus-storage tradeoff.The introduction describes prior control formulations and robustness objectives as complementary to ScanSTL’s focus on repeated robustness and gradient evaluation.Source: §I · p. 1, A. Control Using STL Robustness · p. 2
B. Exact Monitoring and Associative Algorithms
- Prior monitoring work includes associative Since/Until algorithms [9], while ScanSTL combines associative methods with parallel scans and ordered block reductions.The cited online monitor achieves linear total work for a fixed formula but does not develop input derivatives or logarithmic parallel depth across time.Source: B. Exact Monitoring and Associative… · p. 2
C. Differentiable and Parallel STL Evaluation
Differentiable STL evaluators trade temporal parallelism against intermediate storage, while exact finite-horizon semantics require complete traces at every starting time. The problem formulation seeks efficient, parallel computation that preserves those semantics and remains compatible with automatic differentiation.
C. Differentiable and Parallel STL Evaluation
- STLCG uses recurrent updates with limited temporal parallelism, whereas STLCG++ [8] parallelizes through masks whose storage grows quadratically for unary operators and cubically for Until.ScanSTL is positioned as combining associative scans and ordered range reductions for linear work and storage with logarithmic parallel depth, while retaining JAX automatic differentiation.Source: C. Differentiable and Parallel STL… · p. 2
III. PROBLEM FORMULATION
- STL is evaluated on uniformly sampled finite signals, with robustness traces indexed by every possible starting time.Robustness is positive for satisfaction, negative for violation, and its absolute value measures the margin; temporal intervals may be bounded or unbounded.Source: §III · p. 2
- Strong Until requires a valid witness for the second formula and the first formula to hold from the start through that witness.The inclusive prefix includes the witness time and, for delayed intervals, also includes offsets before the witness becomes eligible; no valid witness yields −∞.Source: §III · p. 3
- The task is to compute exact complete traces for a formula and its subformulas at every time index, preserving finite-horizon truncation and empty-window identities.A satisfactory method should use low work and memory, expose parallelism with depth substantially below T, avoid storage-intensive intermediates, and support automatic differentiation.Source: §III · p. 3
IV. PROPOSED METHOD: SCANSTL
ScanSTL reorganizes exact STL semantics so each subformula returns a complete robustness trace. For unbounded Eventually and Always, associative suffix scans replace sequential backward recurrences.
IV. PROPOSED METHOD: SCANSTL
- ScanSTL evaluates formulas recursively over their syntax trees, with each subformula returning a length-T trace; Boolean operators remain pointwise.The method develops bounded ranges and strong Until from the same associative viewpoint used for unbounded unary operators.Source: §IV · p. 3
A. Unbounded Eventually and Always
- O(T) work and O(log T) parallel depth suffice to compute complete unbounded Eventually and Always traces through reverse-time associative scans.The scans exploit associativity of max and min rather than following the corresponding recurrences sequentially; shifted unbounded intervals read the suffix traces at t + a.Source: A. Unbounded Eventually and Always · p. 3
B. Bounded Range Reductions
Bounded temporal ranges are computed as fixed-width queries over identity-padded signals. Ordered block prefixes and suffixes let a shared reduction engine handle extrema and order-sensitive operators.
B. Bounded Range Reductions
- For finite bounds, ScanSTL defines the query width as w = b̄ − a + 1, where b̄ is the largest offset that can be valid at t = 0.When a exceeds b̄ all windows are empty and return their identity; otherwise identity padding converts the ranges into fixed-width queries.Source: B. Bounded Range Reductions · p. 3
- O(T + b̄) work and storage and O(log w) parallel depth compute bounded ranges using within-block prefixes and suffixes.A window crossing a block boundary combines the first block’s suffix with the next block’s prefix, covering its elements exactly once and preserving operand order.Source: B. Bounded Range Reductions · pp. 3–4
C. Strong Until as Max–Min Pair Composition
Strong Until is not a pointwise range maximum: each witness also depends on the survival prefix of φ1. ScanSTL represents the recurrence with associative max–min pair composition, enabling a complete unbounded Until trace through a suffix scan.
C. Strong Until as Max–Min Pair Composition
- Each strong-Until witness depends on φ1 holding through the witness time, so Until is not a pointwise range maximum.The survival prefix is part of each candidate witness.Source: C. Strong Until as Max–Min Pair… · p. 4
- The unbounded recurrence is expressed as a max–min affine map whose pair composition is associative and keeps earlier segments on the left.The operation is not commutative, so scans and range queries must preserve temporal order.Source: C. Strong Until as Max–Min Pair… · p. 4
- One associative suffix scan computes the complete unbounded Until trace with O(T) work and O(log T) depth.The composed pair’s second coordinate gives the strong-Until robustness for the survival prefix beginning at the queried time.Source: C. Strong Until as Max–Min Pair… · p. 4
D. Bounded and Shifted Until
Delayed Until witnesses require a prefix guard for φ1 before the admissible witness range. Ordered pair reductions and that guard produce complete shifted and bounded Until traces.
D. Bounded and Shifted Until
- A delayed first admissible witness requires φ1 to hold before pair composition begins.The prefix guard enforces φ1 before the first allowed witness, while the pair range enforces it from offset a through each witness.Source: D. Bounded and Shifted Until · p. 4
- For [a, ∞], a pair suffix scan plus a prefix-guard range minimum yields the complete shifted Until trace with O(T) work and O(log T) parallel depth.Out-of-horizon pairs use the pair identity.Source: D. Bounded and Shifted Until · p. 4
- For finite [a, b], ordered block reduction and the prefix guard yield the complete bounded Until trace with O(T + b̄) work and O(log(b̄ + 1)) parallel depth.The depth accounts for both the witness range and the guard.Source: D. Bounded and Shifted Until · p. 4
- Table I summarizes exact operator classifications, algebraic objects, evaluation strategies, and full-trace complexities.Source: Table I · p. 5
E. Smooth Robustness
ScanSTL provides smooth unary trace reductions separately from its exact formula evaluator. Smooth Until is a reference surrogate because the exact pair composition does not remain associative under smoothing.
E. Smooth Robustness
- The smooth maximum upper-bounds the exact maximum by at most log(n)/β and converges to it as β → ∞.Smooth minimum is defined by sign duality from smooth maximum.Source: E. Smooth Robustness · p. 5
- Smooth Eventually uses an associative reduction and the shared block engine for bounded windows, while smooth Always follows by sign duality.The aligned-window branch is needed because the smooth reduction is not idempotent.Source: E. Smooth Robustness · p. 5
- Replacing exact minima and maxima with smooth surrogates breaks associativity of the exact pair composition, so Smooth Until is provided only as a reference surrogate.It is not presented as an associative fast path.Source: E. Smooth Robustness · p. 5
- The bounded Smooth Until reference path uses O(T(b̄ + 1)) work and storage, while the unbounded path uses O(T^2).Finite padding substitutes for identities only when padded contributions are negligible; extreme predicate values or temperatures can violate this assumption.Source: E. Smooth Robustness · p. 5
V. EXPERIMENTS
The experiments are organized around scaling, performance on composed specifications, and effects on plan repair and MPC solver capacity.
V. EXPERIMENTS
- The experiments ask how robustness evaluation and differentiation scale with trace length on CPUs and GPUs.Source: §V · p. 5
- A second question tests whether the gains persist across composed specifications.Source: §V · p. 5
- The experiments also test whether faster evaluation reduces time to a verified satisfying plan and increases MPC solver capacity.Source: §V · p. 5
A. Compared Methods and Protocol
The protocol measures complete robustness traces and gradients on CPU and GPU; operator benchmarks show ScanSTL’s advantage varies with operator, interval, and device.
A. Compared Methods and Protocol
- The protocol reports synchronized medians after two warmups, excludes compilation unless stated, and differentiates ρ[0] with respect to inputs.Operator tests use a Ryzen 9 9950X3D and RTX 5090; forward evaluation returns complete traces.Source: A. Compared Methods and Protocol · p. 5
B. Operator Scaling (Q1)
- At T = 256, ScanSTL’s Until speedups over STLCG++ are 2869× forward and 13,694× for gradients on CPU, and 19.7× and 108× on GPU.The comparison focuses on the largest shared tested trace length for Until.Source: B. Operator Scaling (Q1) · p. 5
- At T = 221 on GPU, unbounded Until takes 0.0953 ms forward and 0.2442 ms for gradients; shifted Until takes 0.1303 and 0.3854 ms, respectively.These are the longest tested GPU horizons reported for these operators.Source: B. Operator Scaling (Q1) · p. 5
- On CPU, ScanSTL leads both baselines for unbounded operators at all shared lengths; on GPU, masking is faster for Eventually and Always at T = 128 and 512.At T = 2048, ScanSTL gains 1.19–1.20× forward, with gradients near parity for Eventually and 1.41× faster for Always. Fig. 2 separates unbounded and bounded intervals by row and CPU/GPU by paired rows.Source: B. Operator Scaling (Q1) · p. 5, Figure 2 · p. 6
- Bounded unary forward speedups at T = 2048 are 185–201× on CPU and 1.73–2.06× on GPU; bounded Until at T = 512 gains 160×/1528× on CPU and 2.42×/2.17× on GPU for forward/gradients.The narrow window reduces masking cost and narrows the GPU gap relative to unbounded Until.Source: B. Operator Scaling (Q1) · p. 6
C. Composed Formulas (Q2)
Across nine composed formulas, ScanSTL outpaces both baselines in forward evaluation and gradient computation, with gains that grow as traces lengthen. Escort-and-patrol experiments also report faster plan repair and longer MPC prediction horizons within the nominal solver budget.
C. Composed Formulas (Q2)
- The nine-formula suite tests nesting, bounded Until, response requirements, and multiple clauses across T = 32, 64, 128, 256, and 512.Table III identifies depth as maximum temporal nesting.Source: Table III · p. 6, C. Composed Formulas (Q2) · p. 6
- At T = 512, φ8 takes 0.0267 ms in ScanSTL, versus 182.6 ms in STLCG++ and 108.7 ms in STLCG; φ8 nests bounded Until inside Always.The deeply nested unary formulas φ4 and φ5 have smaller forward speedups over STLCG, 4.42–4.64×; operators and intervals matter alongside nesting depth.Source: C. Composed Formulas (Q2) · p. 6
- At T = 512, ScanSTL’s geometric mean speedups over STLCG++ are 243× for forward evaluation and 104× for gradients across nine formulas.It is faster than both baselines for all nine formulas at each of five tested horizons in both measures.Source: C. Composed Formulas (Q2) · p. 6, Figure 3 · p. 7
D. Escort-and-Patrol Planning and MPC (Q3)
- For plan repair, ScanSTL’s mean time rises from 5.33 to 6.76 ms as T grows from 200 to 500, while STLCG rises from 529 ms to 11.07 s.STLCG++ takes 462 ms at T = 200; compilation exceeds 120 s at T = 300, so T = 500 is not attempted.Source: Table IV · p. 7, D. Escort-and-Patrol Planning and MPC… · p. 7
- The simulated robot dog must escort a person, visit A and B within time windows, return to its dock, and stay within arena and exclusion-region constraints.Planning uses a known person trajectory, while MPC predicts it during execution.Source: D. Escort-and-Patrol Planning and MPC… · p. 7
- Within the nominal 100 ms solver budget, ScanSTL supports a 24 s prediction horizon, compared with 6 s for STLCG++ and 3 s for STLCG.Across tested lookaheads, ScanSTL’s median solver time rises from 1.40 to 24.4 ms.Source: Figure 4 · p. 7, D. Escort-and-Patrol Planning and MPC… · p. 7
- For the escort Until at T = 300, ScanSTL uses prefix and suffix scans over three blocks of 211 pairs, followed by 300 pair compositions.Each scan output contains 633 pairs, or 10.1 kB in float64.Source: D. Escort-and-Patrol Planning and MPC… · p. 7
- The H = 30 execution satisfies the complete mission with robustness +0.091, including a minimum positive safety and proximity margin of +0.091 m.The reported witnesses certify visits to A at 18.8 s, B at 21.4 s, and the dock at 25.6 s; Fig. 5 depicts the execution and margins.Source: D. Escort-and-Patrol Planning and MPC… · pp. 7–8, Figure 5 · p. 8
VI. CONCLUSION
ScanSTL computes complete robustness traces for Eventually, Always, and inclusive strong Until with linear work and storage and logarithmic parallel depth per operator. Benchmarks show computational gains, particularly for Until and composed specifications, while simulated robot experiments show faster plan repair and greater MPC solver capacity.
VI. CONCLUSION
- ScanSTL computes complete robustness traces for Eventually, Always, and inclusive strong Until with linear work and storage and logarithmic parallel depth per operator.Its JAX implementation supports automatic differentiation for optimization and control.Source: §VI · p. 8
- Benchmarks show computational gains, particularly for Until and composed specifications, while simulated robot experiments show faster verified plan repair and greater MPC solver capacity.Smooth Until remains a separate quadratic reference.Source: §VI · p. 8
- Efficient smooth Until evaluation and controllers that use computational savings to improve task satisfaction under enforced deadlines remain future work.Smooth Until remains a separate quadratic reference.Source: §VI · p. 8