Composing Learned Robot Behaviors with Temporal Logic at Runtime

Purdue University

Purdue University

Abstract

Executing Linear Temporal Logic (LTL) instructions with learned robot policies faces two practical challenges: demonstrations may cover individual behaviors without containing the temporal compositions requested at deployment, and semantic success predicates often provide little useful motor guidance through quantitative robustness. We address these challenges by separating behavior learning from temporal composition. From the same offline demonstrations, we train an unconditioned multimodal diffusion policy and a semantic predictor that estimates which semantic outcomes are likely to follow a proposed action sequence. These predictions provide a learned guidance signal without requiring hand-designed robustness measures for semantic task objectives. At deployment, an LTL automaton tracks instruction progress and scores the policy's proposed actions according to their predicted semantic outcomes. Neither learned component receives the specification during training, allowing demonstrated behaviors to be reused in longer, previously unseen temporal compositions without retraining. For additional runtime safety constraints with informative continuous margins, an optional robustness-based controller locally refines the selected actions. Experiments in a navigation environment, CALVIN manipulation, and on a real robot demonstrate reliable execution of complex temporal instructions and additional safety constraints, with substantial improvements over temporal-logic baselines.

Experimental Results

1

Navigation

Navigation base diffusion policy rollouts

The demonstration data includes movements to any of the four regions.

Liveness Constraints

Complex Instructions

Liveness Constraints

LTL: F(b ∧ X F(y ∧ X F(g ∧ X F(r ∧ X F b))))

"Touch the blue region, then the yellow, green, and red regions, then blue again."

Complex Instructions

LTL: G avoid_region ∧ F((F r ∧ F b)∧ F[F(y ∧ F(b ∧ F(g ∧ F y)))∨ F(g ∧ F(b ∧ F(y ∧ F g)))])

"Visit r and b, follow y→b→g→y or g→b→y→g, and always avoid the marked regions."

2

CALVIN

Base diffusion policy in CALVIN

The demonstrations cover arbitrary interactions with the tabletop scene.

Cyclic Repetition

Safety Constraints

Cyclic Repetition

LTL: G F(drawer+ ∧ X F(switch+ ∧ X F(drawer− ∧ X F switch−)))

"Repeatedly flip the switch and open or close the drawer."

Safety Constraints

LTL: F switch− ∧ G tilt20°

"Turn off the switch while keeping the gripper tilted near 20 degrees."

3

Real World

Real-world base policy

The demonstrations cover how to pick up the Cheez-Its, pour them into either bowl, and put them down again.

Behavior Selection

Cyclic Repetition

Behavior Selection

LTL: F(pourR ∧ X F(pourL ∧ X F pourR))

"Pour the Cheez-Its into the right bowl, then the left bowl, then the right bowl again."

Cyclic Repetition

LTL: G F(grab ∧ X F(pourR ∧ X F(pourL ∧ X F put_down)))

"Repeatedly pick up the box, pour into the right bowl, then the left bowl, and put it down."

LTL notation:
F = eventually; G = always; X = next. Learn more about LTL
Navigation:
b, y, g, r = blue, yellow, green, red; avoid_region = stay outside the marked regions.
CALVIN:
switch+/switch− = on/off; drawer+/drawer− = open/closed; tilt20° = gripper tilt near 20°.
Real World:
pourR/pourL = pour right/left; grab = pick up the box; put_down = put it down.