Stream-based robotics Task and Motion Planning (TAMP) integrates discrete symbolic planning with dynamically generated continuous geometric parameters, such as poses, grasps, and trajectories. However, stream-based planners typically reason only about goal reachability, whereas long-horizon tasks also demand adherence to temporal specifications, such as safety-critical ordering, invariance, and liveness constraints. No methods currently exist to enforce such temporal constraints for stream-based solvers because streams generate an expanding geometric object set via iterative stream refinement loops during planning, rendering existing temporal-logic compilation techniques incompatible. We therefore present Synchronous Action Monitoring with Token Destruction (SAM-TD), a compilation method that enforces arbitrary Linear Temporal Logic over finite traces (LTLf) specifications in stream-based TAMP. SAM-TD translates arbitrary LTLf constraints into automata and embeds regressed automaton guards into action schemas, which are pre-specified before planning begins. By doing so, SAM-TD can handle objects generated by streams during planning, thus circumventing the need to enumerate a fixed object set or modify the underlying planner. During search, SAM-TD synchronously updates automaton states and uses a validity token shared across all automata to prune constraint-violating branches. We show that SAM-TD supports dynamically generated stream objects from iterative stream refinements during plan search. Experimental results provide the first ever demonstration of stream-based TAMP under LTLf constraints in three robotics PDDLStream environments. Furthermore, on standard discrete PDDL benchmarks, SAM-TD is competitive with state-of-the-art temporal-constraint compilation methods.
Figures & tables
Figure 1: Illustrative example with two LTL f constraints: φsafety keeps the white and red blocks out of the marked danger region (red wireframe), and φordering forbids moving the red block until the white block is placed. The planning problem requires the robot to move both of the blocks from the black tray to the green tray on the other side of the table. The unconstrained plan (red) is symbolically valid but carries the blocks straight through the danger region (red trace) and moves them in the incorrect sequence. With SAM-TD compiling both constraints into the PDDLStream task, an unmodified planner returns a plan (green) whose sampled trajectory routes around the region (green trace) while respecting the ordering.
Figure 2: SAM-TD pipeline. Left: Inputs are an unmodified PDDLStream problem Π and DFA monitors for each LTL f constraint. Inside SAM-TD: (1) Each transition guard gjkℓ constrains the post-action state, γ(s,a)⊨gjkℓ , and is regressed through every lifted action schema into the equivalent pre-action condition: s⊨Rega(gjkℓ) (§ 3.3 ). (2) The regressed transitions are added to action schemas as conditional effects that advance the monitor in lockstep with the action (§ 3.4 ) during plan search. (3) Transitions into a sink delete a Valid token: the compiled state of a two-state violation monitor tracking all DFAs at once (§ 3.5 ). The compiled goal requires the Valid token and all DFAs in accepting states. Right: The compiled problem Π′ is solved by an unmodified planner with hFF . Since no action re-adds Valid , any state that loses it sets hFF=∞ , so violating branches (red) are pruned before geometric sampling is spent on them. The returned plan π satisfies all constraints.
Figure 3: SAM-TD median end-to-end (left) and median compilation (center) time in stream-based TAMP under adversarial and arbitrary constraint scaling (Experiment 1 and Experiment 2). Runtime breakdown (right) shows per-component medians as stacked areas. Fast Downward translation, not the SAM-TD compilation itself, dominates cost of end-to-end compilation and planning.
Figure 4: Encoding ablation on the Experiment 2 prefixes: median planning time for SAM-TD and SAM-PB, with timeouts capped at the per-environment budget (dashed). Capped points are right-censored. The ZoneSort SAM-PB arm has one accepted repeat; it exhausts memory at k=15 before any Fast Downward invocation, and later prefixes were not run (shaded).
max constraints k
Compiler
Solved
Openst. (24/29)
Rovers (30/56)
Storage (128/128)
t∩ (s)
SAM-TD (ours)
30/30
24/29
30/56
128/128
1.88
BM06
30/30
24/29
30/56
128/128
2.71
TB15
15/30
4/4
4/8
4/64
9.55
TCORE
30/30
24/29
30/56
128/128
2.16
LiftedTCORE
22/30
24/29
30/56
1/1
6.77
Table 1: Published PDDL3 scaling over six tasks and five levels of constraint prefixes per task. Domain entries report the max verified k for the two tasks in order: Openstacks p61/p75, Rovers p60/p90, and Storage p19/p24. t∩ is the geometric-mean compiler-plus-planner time on the instances solved by all seven methods. Complete outcomes, pairwise runtimes, and representation sizes are in supplementary material.
Appendix figures & tables3 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 5: Published PDDL3 trajectory-constraint scaling on the six classical tasks of §4.2 (two per domain), with medians taken over the tasks available at each exact k . Top row: temporal compilation time. Bottom row: total compile-plus-search time, on logarithmic axes. After a method’s first failure, its curve is held at the 180-second budget and marked with crosses (right-censored); those flat segments are not measured runtimes.
Environment
ID
LTL f formula
Interpretation
Tabletop
G1
G(¬InDanger(w))
White block always avoids the encoded danger route.
G2
G(¬InDanger(r))
Red block always avoids the encoded danger route.
G3
G(¬InDanger(b))
Blue block always avoids the encoded danger route.
G4
G(¬InDanger(g))
Green block always avoids the encoded danger route.
U1
¬Moved(r)UPlaced(w)
Place white before moving red.
U2
¬Moved(b)UPlaced(w)
Place white before moving blue.
Appendix
Table 2: Experiment 1 constraint catalogs for all three environments ( G : safety, U : precedence, F : completion). Tabletop abbreviates white_block , red_block , blue_block , and green_block by w,r,b,g ; Kitchen abbreviates the cup, spoon, cream cup, sugar cup, stirrer, and block by c,s,cr,cs,t,b . The six ZoneSort safety formulas cover b1,…,b6 , and its nine precedence formulas form the complete bipartite graph {b1,b2,b3}→{b4,b5,b6} .
Table 3: Five frozen prefix orders per environment. Entries are read from left to right: a run at level k jointly enforces the first k constraints. The seed values are stable pool labels, not run-time shuffle instructions.
We present a fast numerical method for safe continuous-time motion planning under Temporal Logic (TL) specifications. The method generates smooth continuous trajectories that remain collision-free while robustly satisfying temporal and logical task requirements. A central component of our method is the formulation of nonconvex safety and logic constraints as unions of convex sets where associated discrete decisions are encoded in a joint feasibility graph. This graph representation allows Euclidean projection onto the feasible set and proximal robustness maximization to be reformulated as shortest- and widest-path problems, respectively. Building on this structure, we develop a nonconvex splitting method based on the Alternating Direction Method of Multipliers (ADMM), which decouples smooth spatio-temporal trajectory optimization from nonsmooth discrete constraint handling within the optimization. The resulting algorithm exhibits reliable convergence across benchmarks and scales to large-scale motion-planning problems, providing a 4.7x average speedup over the state of the art on discrete and continuous-time logic problems.
Lukas Pries, Joris Verhagen, Jon Arrizabalaga +3
Department of Aerospace and Geodesy, TU Munich, Germany · Division of Robotics, Perception, and Learning, KTH Royal Institute of Technology, Stockholm, Sweden · Department of Aeronautics and Astronautics, MIT, Cambridge, MA, USA
As robots move from controlled environments into real-world settings, it becomes increasingly crucial to ensure that they perform as expected. A key step toward that goal is a rigorous specification of the desired robot behavior, capturing intricate temporal, spatial, and logical requirements. Complementing this, plan and control synthesis methods are needed to fulfill these specifications with provable guarantees. This manuscript presents temporal logics - particularly linear and signal temporal logic - as expressive specification languages for robot behavior over time. We then discuss principles of formal synthesis, from discrete graph- and game-based approaches to sampling-based motion planning, trajectory optimization, and control-certificate-based synthesis. Finally, we outline challenges in deploying formal synthesis in real-world robotics, emphasizing the interplay between modeling fidelity, computational tractability, and the types of rigorous guarantees that can be achieved.
This paper investigates continuous-time motion planning under Signal Temporal Logic (STL) specifications. The goal is to generate smooth robot trajectories that satisfy high-level logical and timing requirements while respecting low-level motion constraints. To this end, we propose an efficient framework that combines timed-automata reasoning with graphs of convex sets (GCS). An STL specification is first represented by a timed automaton, which is then coupled with a convex decomposition of the configuration space to form a joint transition system encoding both task progress and region occupancy. Based on this joint transition system, the STL motion-planning problem is reformulated as a shortest-path problem over a GCS, whose solution induces a smooth Bézier-spline trajectory satisfying the STL specification, smoothness requirements, and velocity bounds. We establish the soundness of the proposed formulation and analyze its computational complexity, showing that, once the timed automaton and convex decomposition are fixed, the convex relaxation scales polynomially with the configuration-space dimension and the Bézier degree. We further develop a compact timed-automaton construction for an expressive STL fragment using dedicated templates and Boolean composition. Numerical experiments on low-dimensional benchmarks, a 3-D quadrotor, a 30-DoF humanoid, and a hardware experiment on a UR-3 robot arm demonstrate that the proposed method efficiently solves complex STL motion-planning problems and produces smooth executable trajectories.
Yu Chen, Ancheng Hou, Mingyang Feng +2
School of Automation & Intelligent Sensing, Shanghai Jiao Tong University, Shanghai 200240, China · Institute of Artificial Intelligence, Xiamen University, Xiamen, China