pdSTL: Probabilistic Differentiable Signal Temporal Logic for Stochastic Systems
For autonomous robots operating under uncertainty, pdSTL provides a novel method to optimize trajectories with probabilistic safety guarantees, addressing a key bottleneck in safe robot learning.
pdSTL introduces a differentiable, probabilistic signal temporal logic framework for stochastic systems, enabling end-to-end trajectory optimization with formal safety guarantees. It outperforms deterministic STL in maintaining safety margins under real-world uncertainty, as demonstrated in simulated and real-world quadcopter experiments.
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.