SparseMax-dSTL: Sound Robustness with Horizon-Independent Gradient Allocation for Temporal Logic Trajectory Optimization

Sai Sandeep Damera; Ryan Matheu; John S. Baras; Calin Belta

eess.SYOct 16, 2026

SparseMax-dSTL: Sound Robustness with Horizon-Independent Gradient Allocation for Temporal Logic Trajectory Optimization

Authors: Sai Sandeep Damera, Ryan Matheu, John S. Baras, Calin Belta

Organizations: The authors are with the University of Maryland, College Park, USA.

Abstract

A gradient-based solver that enforces a Signal Temporal Logic (STL) specification uses a smooth approximation of its quantitative semantics, the robustness. In safety-critical trajectory optimization, this approximation must have two properties. First, it must be sound, that is, nonnegative only on trajectories that satisfy the specification. Second, at each temporal operator, the weight of its gradient on the violating samples must stay bounded away from zero, however long the horizon. The approximations in use, including the log-sum-exp, its sound variant, and the generalized-mean robustness, do not have both. We introduce lower approximations of the minimum and the maximum whose gradients are sparsemax projections, and we prove that the robustness built from them has both. It lies below the exact robustness and is therefore sound, and its error has a bound that is independent of the number of samples and known before optimization. The gradient of each approximation is exactly zero on every sample beyond a data-dependent threshold, so the weight on violating samples a gap beyond the others has a positive lower bound at every horizon. On a planar unicycle and on a seven-joint manipulator beside a person in simulation, the log-sum-exp approximation is positive on a violating trajectory. As the horizon of the manipulator's task grows from 10 to 80 s, the gradient weight of the sound variant on the violating samples falls from 0.22 to 0.04, while that of sparsemax stays at 1. In a constrained trajectory optimization of the unicycle, the constraint on the log-sum-exp robustness returns a violating trajectory, whereas the constraint on the sparsemax robustness returns a trajectory that satisfies the specification with the required margin.

Figures & tables

Fig. 1: (a) Stay out of the zone until the pick on nine samples, three per class (approach, in the zone, waiting), with margins 0.25,

-0.02

, 0.04 from the zone and

-1

, 0.8, 0.8 at the pick,

\varepsilon=0.07

per node. (b) The prefix minimum on the simplex of the class weights (illustrative, not to scale): the values

z

push the centre (equal weights) by

-z/\gamma

, and the nearest point of the simplex gives the sparsemax weights; the LSE weights lie inside, the GMR weights sum to

0.90

(dashed). (c) Values against the exact

\rho

and (d) weight per class at the prefix minimum of (b); GMR of order

(-10,10)

Fig. 2: The until node

\phi\,\mathbf{U}_{I}\,\psi

at sample

t

for a window of four offsets. The outer maximum ranges over the witnesses

j\in I

, and the child of witness

j

is a minimum over

\rho^{\psi}_{t+j}

and the closed prefix

\rho^{\phi}_{t},\ldots,\rho^{\phi}_{t+j}

. Each node is labeled with its error band

b_{m}(\gamma)

of Proposition 1 .

Fig. 3: The minima of sparsemax and of the sound LSE on

k=10

entries at the minimum and

N

entries a gap

\Delta

above it, at equal worst-case error

\varepsilon=0.2

;

N=400

in (a) and (b). (a) Both values lie in the band

[\min z-\varepsilon,\min z]

. (b) Weight on one minimal entry (solid) and on one other entry (dashed), exactly zero for sparsemax once

\Delta\geq\gamma/k

. (c) Weight on the

k

entries against

N

( Theorem 2 ):

W_{Q}=1

at every ratio

\Delta/\varepsilon

shown, since

k\Delta\geq\gamma

there, and each

W_{L}

curve is labeled by its ratio.

	value		weight on $S_{1}$		returned $\rho$
measure	$S_{1}$	$S_{2}$	3 s	130 s	$c=0$	$c=0.2$
exact	$-0.015$	0.300
plain LSE	$+0.024$	0.357	0.68	0.19	$-0.058$	0.146
sound LSE	$-0.076$	0.258	0.68	0.19	0.045	0.218
GMR $(0,1)$	$-0.0001$	1.69	0.043	0.007	$<0.001$	$<0.001$
GMR $(-10,10)$	$-0.009$	0.49	0.71	0.60	$<0.001$	0.141

TABLE I: Planar unicycle at

\varepsilon=0.1

m: values of

\phi

on the fixed trajectories at the 3 s wait, weight on the samples of

S_{1}

inside Red at waits of 3 and 130 s, and exact robustness of the trajectory returned from

S_{1}

at constraint level

c

. Entries shown as

<0.001

lie in

(0,0.001)

Fig. 4: Planar unicycle. (a) The regions and the two fixed trajectories:

S_{1}

cuts into Red and waits beside it,

S_{2}

passes Red at a clearance of 0.3 m. (b) Distance from Red of the trajectories returned at

c=0

under the plain LSE (solid) and the sound LSE (dashed), GMR of order

(-10,10)

, and sparsemax, from the initial trajectory

S_{1}

(dotted).

Panel of Figure 6 — Fig. 5: A violating initial trajectory of the manipulator ( $H=10$ s, exact robustness $-0.05$ ). Top: manipulator, person and zone (green) at five times. Bottom left: exact predicate values; the end effector is inside the zone for 0.3 s and then waits at the pick pose. Bottom right: weight on the samples inside the zone at $\varepsilon=0.2$ , medians over the four trajectories (markers), with the curves of Remark 1 for the LSE and sparsemax and straight lines for GMR.

		weight on		torque gradient through
		the samples inside the zone
measure	value	10 s	80 s	10 s	80 s
exact	$-0.050$
plain LSE	$+0.023$	0.216	0.036	3.62	0.67
sound LSE	$-0.177$	0.216	0.036	3.62	0.67
GMR $(0,1)$	$-0.0006$	0.024	0.0024	0.40	0.039

TABLE II: The until conjunct on the violating initial trajectories of the manipulator at

\varepsilon=0.2

, medians over the four trajectories: value at

H=10

s, sum of the leaf weights on the samples inside the zone, and norm of the part of the torque gradient that passes through those samples.

measure	$\rho_{0}$	10 s	20 s	40 s	$\rho_{100}$	effort
		first satisfying update			after 100 updates, 40 s
plain LSE	$-0.05$	6	6	6 [5,7]	0.001 ( $-0.006$ )	0.61
	$-0.10$	$7^{1}$	$7^{2}$	7 [7,23]	$-0.0005$ ( $-0.15$ )	0.50
sound LSE	$-0.05$	4.5	10	17 [14,22]	0.097 (0.06)	0.94
	$-0.10$	6	11	19.5 [13,25]	0.083 (0.04)	0.94
GMR $(0,1)$	$-0.05$	3	$5^{1}$	$5^{1}$ [5,6]	0.003 ( $-0.02$ )	0.33

TABLE III: Optimization on the torques from the violating initial trajectories, the same 16 locations for every measure,

c=0

, 100 updates: median first update with a nonnegative exact robustness at 10, 20, and 40 s, with quartiles at 40 s; at 40 s, the median and smallest exact robustness after 100 updates and the median effort relative to the initial trajectory,

E_{100}/E_{0}

. A superscript counts the locations that never satisfied, left out of the median.

STL Motion Planning

See all 19 papers

Mar 6, 2026

STL-SVPIO: Signal Temporal Logic guided Stein Variational Path Integral Optimization

Signal Temporal Logic (STL) enables formal specification of complex spatiotemporal constraints for robotic task planning. However, synthesizing long-horizon continuous control trajectories from complex STL specifications is fundamentally challenging due to the nested structure of STL robustness objectives. Existing solver-based methods, such as Mixed-Integer Linear Programming (MILP), suffer from exponential scaling, whereas sampling methods, such as Model-Predictive Path Integral control (MPPI), struggle with sparse, long-horizon costs. We introduce Signal Temporal Logic guided Stein Variational Path Integral Optimization (STL-SVPIO), which reframes STL as a globally informative, differentiable reward-shaping mechanism. By leveraging Stein Variational Gradient Descent and differentiable physics engines, STL-SVPIO transports a mutually repulsive swarm of control particles toward high robustness regions. Our method transforms sparse logical satisfaction into tractable variational inference, mitigating the severe local minima traps of standard gradient-based methods. We demonstrate that STL-SVPIO significantly outperforms existing methods in both robustness and efficiency for traditional STL tasks. Moreover, it solves complex long-horizon tasks, including multi-agent coordination with synchronization and queuing while baselines either fail to discover feasible solutions, or become computationally intractable. Finally, we use STL-SVPIO in agile robotic motion planning tasks with nonlinear dynamics, such as 7-DoF manipulation and half cheetah back flips to show the generalizability of our algorithm.

Hongrui Zheng, Zirui Zang, Ahmad Amine +2

Department of Electrical and Systems Engineering, University of Pennsylvania, Philadelphia, PA, USA. · Mechanical Engineering and Mechanics Department, Lehigh University, Bethlehem, PA, USA.

STL Motion Planning Trajectory Optimization Robot Task Planning Motion Planning

Ask PDF

Jun 17, 2026

pdSTL: Probabilistic Differentiable Signal Temporal Logic for Stochastic Systems

Autonomous robots operating in uncertain environments must satisfy complex temporal and safety specifications despite stochastic dynamics and sensing noise. While Signal Temporal Logic (STL) offers robustness measures for gradient-based optimization, existing extensions either lack differentiability or ignore belief-space uncertainty. We introduce pdSTL (probabilistic differentiable Signal Temporal Logic), a framework that unifies probabilistic semantics with differentiable robustness over belief trajectories. pdSTL employs interval-valued probabilistic semantics to compute conservative satisfaction bounds, propagated compositionally through the STL syntax tree. We formulate the temporal robustness evaluation as a recurrent, LSTM-style unfolding of STL operators, enabling linear-time, differentiable monitoring suitable for end-to-end trajectory optimization. We validate pdSTL on simulated obstacle avoidance, lane-change maneuvers, and real-world Crazyflie quadcopter flight experiments under aerodynamic disturbances. Results demonstrate that pdSTL achieves efficient optimization with formal probabilistic guarantees, significantly outperforming deterministic differentiable STL in maintaining safety margins under real-world uncertainty.

Bennett Dogbey, Hemanth Manjunatha

Dept. of Mechanical and Aerospace Engineering, Oklahoma State University, Stillwater, OK USA

Signal Temporal Logic Safe Robot Navigation

Ask PDF

Oct 5, 2026

ScanSTL: Parallel Robustness Evaluation for Signal Temporal Logic

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.

Gokhan Alcan

Automation Technology and Mechanical Engineering, Tampere University, 33100 Tampere, Finland

Signal Temporal Logic STL Planning

Ask PDF

Abstract

STL Motion Planning

Explore similar work

STL-SVPIO: Signal Temporal Logic guided Stein Variational Path Integral Optimization

pdSTL: Probabilistic Differentiable Signal Temporal Logic for Stochastic Systems

ScanSTL: Parallel Robustness Evaluation for Signal Temporal Logic