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.
Figures & tables
Fig. 1: From demonstrations to runtime temporal composition. Our method learns motor behaviors and their semantic outcomes from offline demonstrations, then uses an LTL automaton at deployment to compose them into new instructions. Top: representative failures of baselines when executing semantic manipulation objectives. Bottom: representative executions of our method for LTL specifications that were not present in the data.
Fig. 2: Learning semantic outcome predictions from demonstrations. Left: an unconditioned multimodal action-chunking policy learns the motor behaviors present in the demonstration data. Middle: the same demonstrations supervise the semantic predictor by pairing each executed action chunk with the next distinct semantic label reached later in the trajectory. Right: at inference time, the predictor maps a proposed action chunk to a distribution over possible future semantic outcomes, allowing the controller to estimate what that behavior is likely to accomplish even before the corresponding proposition becomes true. Curves and probabilities are illustrative.
Fig. 3: Full overview of the runtime temporal-composition controller. The figure walks through one action-selection step for an example with atomic propositions AP={A,B,C} , K=3 candidate action chunks, and an LTL automaton whose accepting state is indicated by a double circle. Left: the behavior policy proposes three candidate action chunks, and gψ maps each candidate to a semantic prediction ℓ^k+ , whose entries give the predicted probabilities that the individual atomic propositions hold in the next distinct semantic label. From each ℓ^k+ , we construct a factorized distribution over complete Boolean labels σ∈Σ=2AP . Center: each possible label σ induces a transition from the current automaton state, producing a distribution over next automaton states that is scored by progress toward acceptance using Uϕ . In the illustrated example, the second candidate receives the highest score. Right: the controller selects this candidate for execution and can optionally refine it using robustness for an additional runtime safety constraint. After the selected chunk is executed, the observed semantic label updates the automaton state qt , the policy proposes new candidates, and the process repeats in closed loop.
Fig. 4: 2D navigation environment and semantic vocabulary. The point agent is trained from single-goal demonstrations to reach four colored regions. Each region induces one atomic proposition through the distance-based predicates shown on the right; the same predicates are used by all methods.
Fig. 5: Composition from primitive demonstrations. Top: executed LTL satisfaction for increasingly long prefixes of the sequence blue → yellow → green → red → blue, together with representative four-goal rollouts. Bottom: success on three structurally different specifications using the same trained models: ϕ1=(¬gUr)∧(¬gUb)∧F(g∧F(y∧F(r∧F(b∧F(y∧Fg))))) , ϕ2=S(r,y,g,b,r,y,g,b)∨S(g,b,y,r,g,b,y,r) , ϕ3=GFr∧GFb∧GFg∧GFy . Here, r,b,g,y denote contact with the corresponding colored regions, and S(p1,…,pm)=F(p1∧XF(p2∧⋯∧XFpm)) denotes strict ordered visitation. Recurrence is evaluated over two completed rounds.
Fig. 6: CALVIN manipulation environment and semantic vocabulary. The robot interacts with a switch, button, drawer, and sliding door. The right panel lists the atomic propositions and simulator-state predicates used to label these behaviors throughout the experiments.
Fig. 7: Semantic guidance and temporal composition in CALVIN. Top: success on seven individual semantic goals. Hatched background bars show the success rate of generated state trajectories for LTLDoG and TeLoGraF. Bottom: full LTL satisfaction (%) on six composite instructions and three runtime safety constraints. Parentheses report results without safety refinement; N/A denotes configurations not evaluated. The same trained behavior policy and semantic predictor are reused across all specifications; safety rows additionally activate the optional robustness refinement. Each tested method–task pair uses 50 executed rollouts.
Fig. 8: Effect of optional safety refinement. Example executions with and without refinement for region, orientation, and gripper constraints. Joint task-and-constraint success increases from 42%, 0%, and 0% without refinement to 98%, 82%, and 98%, respectively.
Fig. 9: Physical execution of runtime temporal instructions. For STL-GPC, the robustness predicates are rbox_grabbed=g , rpour_left=−θ−90∘ , and rpour_right=θ−90∘ , where θ is the wrist angle and g=1 for a closed gripper, −1 otherwise. Success rates for five runtime instructions: ϕ1=F(box_grabbed∧Fpour_left) ; ϕ2=F(box_grabbed∧Fpour_right) ; ϕ3=ϕ1∧G¬unsafe ; ϕ4=ϕ1∧(uprightUnear_bowl) ; ϕ5=F(box_grabbed∧GF(pour_left∧Fpour_right)) . Each condition in ϕ1 – ϕ4 uses N=20 real-robot trials; our method achieves 100% success on ϕ5 over N=5 trials (evaluated for three full cycles).
Many robotic tasks are temporally extended and demand precise specifications of subgoals, constraints, and their temporal ordering. Yet human operators typically communicate such tasks in natural language, which is inherently ambiguous, underspecified, and context dependent. Translating human instructions into formal task specifications, such as Linear Temporal Logic (LTL), is therefore essential for verifiable and safe robotic execution. Existing LLM-based translators attempt to bridge this gap through open-ended reasoning or post-hoc constraint enforcement, but the former may violate domain constraints, whereas the latter can disrupt the reasoning needed for novel instructions. This paper proposes Self-Constrained Reasoning (SCR), a framework that mitigates this trade-off by internalizing structural knowledge into the model's decision-making process rather than imposing it as an external filter. By combining a structural constraint representation with a hierarchical decision-making formulation, SCR guides reasoning within a formally grounded space while preserving adaptability to unseen instructions. Experiments show that SCR improves both domain-constraint satisfaction and generalization, providing an effective and interpretable approach for translating human intent into verifiable specifications for robotic execution.
Haofei Hou, Fanxu Meng, Shunyi Zhao +4
School of Advanced Manufacturing and Robotics, Peking University, Beijing 100871, China. · School of Integrated Circuits, Peking University, Beijing 100871, China.
Diffusion policies enable multimodal robot behavior but offer limited ability to choose among behavior modes at inference time, even though such control is desirable in human-robot settings. Prior solutions to this lack of control have utilized Signal Temporal Logic (STL) to express human intentions and provide corresponding guidance for diffusion policy inference. However, these approaches can only guide diffusion policies that jointly generate future actions and states, increasing both complexity and runtime. We propose a novel guidance method for action-only diffusion policies that uses a separate learned world model to enable differentiable evaluation of STL robustness, with its gradient then injected into the diffusion process. This steers behavior toward constraint satisfaction without retraining, improving constraint adherence while preserving task performance. On the Can Transport task from Robomimic, our method maintains 100% task success while reducing constraint violations from over 80% for baseline methods to 4%. We also discuss extensions toward improved robustness and more complex constraints.
Moritz Zoellner, Anastasios Manganaris, Rohan Paleja
Department of Computer Science, Purdue University West Lafayette, IN, USA
In this work we study offline reinforcement learning (RL) under temporally extended task constraints expressed in Linear Temporal Logic over finite traces (LTLf). Recently, transformer-based approaches such as Trajectory Transformers and Decision Transformers have been adopted to address RL as a sequence modeling problem. However, these methods optimize purely for reward and do not account for high-level temporal requirements. Here, we introduce a neurosymbolic framework that injects LTLf background knowledge into such transformer-based RL policies. Our approach compiles LTLf formulas into deterministic finite automata (DFAs) and integrates them into the learning process through a differentiable representation and a logic-based loss function. In particular, we derive differentiable satisfaction signals from DFA progression and use them as a regularization term during training. The resulting method is architecture-agnostic across different models. We evaluate the proposed framework on navigation environments with specification suites covering combinations of safety and reachability temporal properties. Experimental results show that incorporating background knowledge not only improves constraint satisfaction, but also maintains competitive return compared to vanilla baselines.
Ashkan Ansarifard, Matteo Mancanelli, Elena Umili +1
Sapienza University of Rome · University of Rome La Sapienza, Rome, Italy