LTLDoG: Satisfying Temporally-Extended Symbolic Constraints for Safe Diffusion-based Planning

TL;DR

A data-driven diffusion-based framework that modifies the inference steps of the reverse process given an instruction specified using finite linear temporal logic, and can be trained to generalize to new instructions not observed during training, enabling flexible test-time adaptability.

Abstract

Operating effectively in complex environments while complying with specified constraints is crucial for the safe and successful deployment of robots that interact with and operate around people. In this work, we focus on generating long-horizon trajectories that adhere to novel static and temporally-extended constraints/instructions at test time. We propose a data-driven diffusion-based framework, LTLDoG, that modifies the inference steps of the reverse process given an instruction specified using finite linear temporal logic ($\text{LTL}_f$). LTLDoG leverages a satisfaction value function on $\text{LTL}_f$ and guides the sampling steps using its gradient field. This value function can also be trained to generalize to new instructions not observed during training, enabling flexible test-time adaptability. Experiments in robot navigation and manipulation illustrate that the method is able to generate trajectories that satisfy formulae that specify obstacle avoidance and visitation sequences. Code and supplementary material are available online at https://github.com/clear-nus/ltldog.

Figures (14)

• Figure 1: We present LTLDoG, a diffusion-based planning framework for generating trajectories that comply with specified $\textnormal{LTL}_f$ formulae. In the example above, a robot dog is tasked to arrive at the goal position (A), but first has to visit B and avoid obstacles (crosses).
• Figure 2: Real world environments for quadruped robot navigation.
• Figure 3: Examples of safe planning in Maze2d-Large. There are three unsafe blocks (red squares, labeled $p_L$, $p_M$, $p_R$ from left to right) that need to be avoided during navigation to the goal (shaded circle). The $\textnormal{LTL}_f$ constraint for this task is $\varphi = \Box\xspace\neg(p_L \wedge p_M \wedge p_R)$. (a) Trajectories from Diffuser ignore safety and can violate the specified constraints. (b) SafeDiffuser produces discontinuous trajectories. (c) Our LTLDoG is able to plan trajectories that detours around the obstacles to successfully arrive at the goal.
• Figure 4: Results of safe control in PushT. (a) A robot arm's end effector (circles filled in blue) should manipulate the T block (gray) to a goal pose (green), and avoid entering unsafe regions (hollow circles marked with $pX$), specified by an $\textnormal{LTL}_f$ formula (text in black). In this example, the $\textnormal{LTL}_f$ specifies the end effector should never enter regions $p1$ (purple) and $p3$ (cyan). (b) The actions generated and executed by Diffusion Policy do not satisfy the $\textnormal{LTL}_f$ formula. (c) In contrast, LTLDoG-S guides the diffusion to avoid $p1$ and $p3$, yet still completes the manipulation task.
• Figure 5: Temporal Constraints in Maze2D. (a) Each maze has 6 non-overlapping regions. Agents are requested to visit some of these blocks under different temporally-extended orders. (b) and (c) show generated trajectories under $\varphi=\neg p_3\operatorname{\mathsf{U}}\xspace{}(p_5 \wedge(\neg p_2\operatorname{\mathsf{U}}\xspace{} p_0))$. Our method can satisfy $\neg$ propositions (red zones) before reaching the green regions.