When Automata Meet Streams: Temporal Logic Compilation for Stream-Based Robotics Task and Motion Planning

Sayem Nazmuz Zaman; Cyrus Neary

cs.ROAug 19, 2026

When Automata Meet Streams: Temporal Logic Compilation for Stream-Based Robotics Task and Motion Planning

Authors: Sayem Nazmuz Zaman, Cyrus Neary

Organizations: Department of Electrical and Computer Engineering University of British Columbia Vancouver, BC, Canada

Abstract

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 ( $\textrm{LTL}_f$ ) specifications in stream-based TAMP. SAM-TD translates arbitrary $\textrm{LTL}_f$ 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 $\textrm{LTL}_f$ 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: $\varphi_{\text{safety}}$ keeps the white and red blocks out of the marked danger region (red wireframe), and $\varphi_{\text{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 $\Pi$ and DFA monitors for each LTL f constraint. Inside SAM-TD: (1) Each transition guard $g^{k\ell}_{j}$ constrains the post-action state, $\gamma(s,a)\vDash g^{k\ell}_{j}$ , and is regressed through every lifted action schema into the equivalent pre-action condition: $s\vDash\mathrm{Reg}_{a}(g^{k\ell}_{j})$ (§ 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 $\Pi^{\prime}$ is solved by an unmodified planner with $h^{\text{FF}}$ . Since no action re-adds Valid , any state that loses it sets $h^{\text{FF}}=\infty$ , so violating branches (red) are pruned before geometric sampling is spent on them. The returned plan $\pi$ 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).

Compiler	Solved	Openst. (24/29)	Rovers (30/56)	Storage (128/128)	$t_{\cap}$ (s)
		max constraints $k$
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_{\cap}

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	$G_{1}$	$\mathsf{G}\bigl(\neg\mathit{InDanger}(w)\bigr)$	White block always avoids the encoded danger route.
	$G_{2}$	$\mathsf{G}\bigl(\neg\mathit{InDanger}(r)\bigr)$	Red block always avoids the encoded danger route.
	$G_{3}$	$\mathsf{G}\bigl(\neg\mathit{InDanger}(b)\bigr)$	Blue block always avoids the encoded danger route.
	$G_{4}$	$\mathsf{G}\bigl(\neg\mathit{InDanger}(g)\bigr)$	Green block always avoids the encoded danger route.
	$U_{1}$	$\neg\mathit{Moved}(r)\ \mathsf{U}\ \mathit{Placed}(w)$	Place white before moving red.
	$U_{2}$	$\neg\mathit{Moved}(b)\ \mathsf{U}\ \mathit{Placed}(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,c_{r},c_{s},t,b

. The six ZoneSort safety formulas cover

b_{1},\ldots,b_{6}

, and its nine precedence formulas form the complete bipartite graph

\{b_{1},b_{2},b_{3}\}\rightarrow\{b_{4},b_{5},b_{6}\}

Environment	Seed	Ordered constraints
Tabletop	11	$F_{1}$ , $G_{1}$ , $U_{4}$ , $G_{4}$ , $U_{1}$ , $G_{3}$ , $U_{3}$ , $G_{2}$ , $U_{2}$
	17	$G_{2}$ , $U_{4}$ , $F_{1}$ , $G_{4}$ , $U_{3}$ , $G_{3}$ , $U_{2}$ , $G_{1}$ , $U_{1}$
	23	$G_{2}$ , $U_{1}$ , $G_{4}$ , $U_{3}$ , $F_{1}$ , $G_{1}$ , $U_{2}$ , $G_{3}$ , $U_{4}$
	31	$G_{4}$ , $U_{4}$ , $G_{3}$ , $U_{2}$ , $G_{1}$ , $U_{3}$ , $F_{1}$ , $G_{2}$ , $U_{1}$
	47	$G_{4}$ , $U_{4}$ , $G_{1}$ , $U_{2}$ , $G_{2}$ , $U_{1}$ , $G_{3}$ , $U_{3}$ , $F_{1}$
Kitchen	11	$F_{1}$ , $U_{1}$ , $U_{2}$ , $G_{1}$ , $U_{3}$ , $U_{4}$ , $G_{2}$

Appendix

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.

Motion Planning

Motion planning finds safe, feasible paths and trajectories for robots and vehicles amid geometric, dynamic, and task constraints.

See all 392 papers

Fast and Robust Temporal Logic Planning via ADMM-based Trajectory Optimization
Sep 19, 2026Lukas Pries, Joris Verhagen, Jon Arrizabalaga +3STL Motion Planning Safe Motion Planning
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
Temporal logics and formal synthesis for robot planning and control
Jun 19, 2026Jana Tumova, Joris Verhagen, Matti VahsRobotics Signal Temporal Logic
KTH Royal Institute of Technology
Signal Temporal Logic Motion Planning via Graphs of Convex Sets
May 22, 2026Yu Chen, Ancheng Hou, Mingyang Feng +2Constrained Motion Planning Trajectory Generation
School of Automation & Intelligent Sensing, Shanghai Jiao Tong University, Shanghai 200240, China · Institute of Artificial Intelligence, Xiamen University, Xiamen, China

Sep 19, 2026J/K move · Enter open · S save

Fast and Robust Temporal Logic Planning via ADMM-based Trajectory Optimization

Lukas Pries, Joris Verhagen, Jon Arrizabalaga, Jana Tumova+2

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

STL Motion Planning Safe Motion Planning Motion Planning Trajectory Optimization

Open paper AskPDF arXiv

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.

Abstract

Motion Planning

Explore similar work

Fast and Robust Temporal Logic Planning via ADMM-based Trajectory Optimization

Temporal logics and formal synthesis for robot planning and control

Signal Temporal Logic Motion Planning via Graphs of Convex Sets