Executing complex manipulation in cluttered environments requires satisfying coupled geometric and temporal constraints. Although Spatio-Temporal Logic (SpaTiaL) offers a principled specification framework, its use in gradient-based optimization is limited by non-differentiable geometric operations. Existing differentiable temporal logics focus on the robot's internal state and neglect interactive object-environment relations, while spatial logic approaches that capture such interactions rely on discrete geometry engines that break the computational graph and preclude exact gradient propagation. To overcome this limitation, we propose Differentiable SpaTiaL, a fully tensorized toolbox that constructs smooth, autograd-compatible geometric primitives directly over polygonal sets. To the best of our knowledge, this is the first end-to-end differentiable symbolic spatio-temporal logic toolbox. By analytically deriving differentiable relaxations of key spatial predicates--including signed distance, intersection, containment, and directional relations--we enable an end-to-end differentiable mapping from high-level semantic specifications to low-level geometric configurations, without invoking external discrete solvers. This fully differentiable formulation unlocks two core capabilities: (i) massively parallel trajectory optimization under rigorous spatio-temporal constraints, and (ii) direct learning of spatial logic parameters from demonstrations via backpropagation. Experimental results validate the effectiveness and scalability of the proposed framework.
Figures & tables
Fig. 1 : Overview of Differentiable SpaTiaL . Our framework replaces discrete geometry engines with a fully tensorized architecture, enabling end-to-end trajectory optimization under formal specifications.
Framework / Toolbox
Temporal
Spatial
Differentiable
Batch-native tensorized
Diff-TL (e.g., STLCG [ 12 , 13 ] )
✓
×
✓
✓
SpaTiaL [ 4 ]
✓
✓
×
×
Diff. Collision (e.g., DiffCol [ 21 ] )
×
✓
✓
×
Diff-SpaTiaL (Ours)
✓
✓
✓
✓
TABLE I : Feature comparison of our toolbox against existing formal logic and geometric frameworks.
Fig. 2 : Smooth spatial and temporal operators form a differentiable robustness computation graph.
Fig. 3 : Differentiable penetration depth via Smooth SAT. Exact discrete overlap is relaxed into a smooth, differentiable repulsion field.
Fig. 4 : Differentiable Signed Distance Field (SDF) via boundary sampling. Soft aggregation ensures informative gradients in both colliding and non-colliding states.
Fig. 5 : Geometric interpretation of compositional predicates (left: EnclIn, right: leftOf). Spatial relations are resolved as differentiable algebraic operations over vertex tensors.
Fig. 6 : Qualitative spatio-temporal trajectory optimization using differentiable spatial semantics. From left to right: initial trajectory (violates), iteration 30, final trajectory (satisfies), and robustness analysis.
Fig. 7 : Learning spatial specification parameters from demonstrations via robustness backpropagation. From left to right: oblique, xy, and xz views.
Start → Pick
Pick → Place
Obs
Formula
ε
Obs
Formula
ε
O1
FI1(RightOf)
4.25
O1
GI2(RightOf)
3.31
FI1(Behind)
1.87
FI2(InFrontOf)
3.77
O2
FI1(LeftOf)
5.25
O2
FI2(InFrontOf)
4.73
FI1(Above)
2.55
FI2(Above)
2.52
O3
FI1(LeftOf)
5.83
O3
FI2(Behind)
3.66
TABLE II : Discovered spatio-temporal specification with learned margins; phase 1 ( I1=[0,59] ) and phase 2 ( I2=[60,118] ). All predicates are of the form (arm,Ok) .
Fig. 8 : Geometric accuracy of differentiable predicates. We compare distance, signed distance, penetration, and enclosure robustness against Shapely across randomized convex polygons and transforms.
Fig. 9 : Effect of the smoothing temperature τ and boundary sampling density on signed distance and its gradient.
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
Multi-agent robotic manipulation tasks require coordination among agents to satisfy task-level temporal, logical, and safety constraints. Recently, diffusion policies have been used to perform the task. However, they still suffer from desynchronization, incorrect action ordering, and coordination failures in tasks that require simultaneous or sequential multi-agent interaction. Therefore, LTLDiff is proposed as a framework that combines Finite Linear Temporal Logic (LTLf) specification learning for both the generation of demonstrations and learning via diffusion policies. Each task has a specific LTLf formula that is learned from a set of natural language instructions using a large-scale language model. To enable a fixed-dimensional vector embedding of the learned specification from the language model, LTLf uses an abstract syntax tree representation scheme. This embedding of logic serves as a condition for (i) logic-guided data collection and (ii) diffusion-based policy training, encouraging trajectories that are consistent with the desired ordering and coordination requirements. Experiments on multi-agent LTLDiff manipulation tasks demonstrate improved task success rates compared to the baseline. Together, these contributions demonstrate the effectiveness of LTLDiff for coordinated multi-agent manipulation.
Chuhan Meng, Haiyan Yin
University of Toronto, Toronto, ON, Canada · A*STAR Centre for Frontier AI Research (A*STAR CFAR), Agency for Science, Technology and Research (A*STAR), Singapore
Vision-language-action (VLA) models have achieved great success on general robotic tasks, but still face challenges in fine-grained spatiotemporal manipulation. Typically, existing methods mainly embed spatiotemporal knowledge into visual and action representations, and directly perform a cross-modal mapping for step-level action prediction. However, such spatiotemporal reasoning remains largely implicit, making it difficult to handle multiple sequential behaviors with explicit spatiotemporal boundaries. In this work, we propose ST-π, a structured spatiotemporal VLA model for robotic manipulation. Our model is guided by two key designs: 1) Spatiotemporal VLM. We encode 4D observations and task instructions into latent spaces, and feed them into the LLM to generate a sequence of causally ordered chunk-level action prompts consisting of sub-tasks, spatial grounding and temporal grounding. 2) Spatiotemporal action expert. Conditioned on chunk-level action prompts, we design a structured dual-generator guidance to jointly model spatial dependencies and temporal causality, thus predicting step-level action parameters. Within this structured framework, the VLM explicitly plans global spatiotemporal behavior, and the action expert further refines local spatiotemporal control. In addition, we propose a real-world robotic dataset with structured spatiotemporal annotations for fine-tuning. Extensive experiments have been conducted to demonstrate the effectiveness of our model. Our code link: https://github.com/chuanhaoma/ST-pi.
Chuanhao Ma, Hanyu Zhou, Shihan Peng +3
School of Artificial Intelligence and Automation, Huazhong University of Science and Technology · School of Computing, National University of Singapore · School of Computing, Macquarie University