STeP: Signal Temporal Logic for Precise Specifications for Action Generation with Vision Language Models

Figure 1: A single language instruction can encode temporal ("within 5 to 8 seconds") and spatial ("8cm left of the pink mug" and "avoiding the stove") requirements simultaneously. The framework decomposes the instruction into STL-annotated subtasks, where each stage carries relevant constraints as formal specifications guiding execution and monitoring.

1. Abstract

Vision-language-action (VLA) models have shown impressive generalization, but often lack interpretability and can struggle to follow precise natural language instructions that encode spatial, temporal, and logical requirements. We propose a hierarchical framework that uses Signal Temporal Logic (STL) as a shared representation connecting high-level language understanding with low-level robot execution. A high-level policy leverages a VLM to decompose language instructions into high-level subtasks, generate STL specifications for each subtask, and choose a low-level policy for executing each subtask. The STL specifications translate language-derived intent into precise constraints, and the low-level policy selection determines whether those constraints are enforced directly through STL-guided model-predictive control or monitored during execution of a learned policy for perceptually complex, or contact-rich behaviors. By integrating STL into plan validation, low-level policy, subtask monitoring, and replanning, our framework enables language-derived plans to be checked, optimized, and revised at runtime using a common formal structure.

2. Background & Motivation

Precise language-conditioned robot planning requires more than completing coarse semantic goals—many instructions impose spatial, temporal, and logical requirements (placing at specified metric offset, maneuvering within timing window, avoiding regions). VLA models perform well but don't inherently expose mechanisms for representing, monitoring, or enforcing such constraints during execution.

Recent dual-system VLA architectures separate behavior into slow deliberative System 2 (vision-language reasoning) and fast System 1 (low-level action generation). But this separation alone doesn't specify how precise spatial, temporal, and logical requirements should be represented or enforced during execution.

STeP argues System 2 should not only plan but also formalize these requirements into a representation System 1 can monitor and enforce. Using STL as this formal interface—STL provides a compact language for encoding spatial, temporal, and logical constraints, with quantitative robustness semantics providing a continuous measure of specification satisfaction, allowing progress evaluation, violation detection, and trajectory optimization.

3. Core Method

Figure 2: Overview of STeP. System 2 uses language instruction, observation, skill library, and history log to decompose task into subtasks and compile each into STL specification. System 1 executes active subtask while STL monitoring tracks progress and detects failures. Upon completion or violation, history log provides recall context for System 2 to update plan while grounded in original task specification.

3.1 System 2: Language-to-STL Task Planning

System 2 acts as high-level task planner and formalizer. Given language instruction, current observation, skill and predicate libraries, and recall context (prior observations/states/STL robustness values/previous plan), System 2 queries a VLM to produce structured task specification—subtask sequence, each with skill name, grounded parameters, optional constraints, and natural language description.

Figure 3a: Constructing a VLM prompt from language instruction, observation, and system Skill Library.

Before execution, static task-spec checks ensure: output matches JSON schema, each skill present in library, parameters have correct types, referenced objects/regions exist in current scene, each constraint supported by selected skill. Failed specs sent back to VLM with error message.

Checked specification passed to deterministic STL compiler, mapping skill templates and grounded parameters to STL formulas over predefined predicate library, inserting relevant local/global constraints (safety, timing windows), and converting seconds to controller timesteps.

Figure 3b: Task specification showing each subtask the VLM produces and how it's compiled into a series of STL formulas.

3.2 System 1: STL-Guided Execution and Monitoring

System 1 handles low-level action generation. For each subtask, selects either STL-guided MPC controller or predefined learned policy. MPC used for subtasks expressible through explicit geometric/temporal/safety constraints; learned policies for behaviors difficult to model analytically or requiring more expressive perceptual control.

During execution, STL monitor evaluates robustness of active subtask formula. If robustness drops below threshold, System 1 triggers recall to System 2 with current execution context, allowing plan repair/revision while grounded in original task specification.

Figure 3c: Simplified history log entry showing how STL robustness is integral to task monitoring and failure detection.

3.3 MPC Controller

MPC prescribes a dynamics model, optimizing action sequence over finite horizon at each timestep, executing first action and replanning. Given STL specification, controller optimizes:

$$\min_{a_{0:H}} \; -\rho^{\beta}_{\phi}(\hat{s}_{0:H})$$

where $\hat{s}$ is the predicted signal trajectory for evaluating STL robustness $\rho^{\beta}_{\phi}$. Robustness uses softmax smooth approximation of max/min operators for gradient-based optimization:

$$\mathrm{smoothmax}_{\beta}(x_1,\ldots,x_n) = \frac{\sum_{i} x_i e^{\beta x_i}}{\sum_{i} e^{\beta x_i}}$$

where $\beta$ controls approximation sharpness. Since dynamics model predicts future states but not observations, future signals computed using predicted states and current observation.

graph TB
    LANG[Natural Language Instruction] --> S2[System 2: VLM Planner]
    OBS[Current Observation] --> S2
    SKILL[Skill Library + Predicates] --> S2
    HIST[History Log] --> S2
    S2 -->|subtasks + STL specs| COMPILE[Deterministic STL Compiler]
    COMPILE --> CHECK[Static Task Spec Checks]
    CHECK -->|pass| S1[System 1: Execution]
    CHECK -->|fail + error| S2
    S1 -->|STL constraints| MPC[STL-Guided MPC]
    S1 -->|contact-rich| LEARN[Learned Policy]
    MPC --> MONITOR[STL Robustness Monitor]
    LEARN --> MONITOR
    MONITOR -->|robustness < threshold| S2
    MONITOR -->|satisfied| NEXT[Next Subtask]
    NEXT --> S1

4. Key Experiments

4.1 RQ1: Precise Language Following

Figure 4: Real World Results of STeP vs VLM-MPC-Cost. Success rates grouped by constraint type. Embedding STL improves success across the board, especially on temporal constraints.

Evaluated on UR3e robot across 9 tabletop manipulation tasks grouped by primary constraint type (logical, spatial, logical+spatial, temporal). STeP achieves higher safe success rates across all task categories, with largest gains on temporal constraints. Baseline VLM-MPC-Cost removes STL components—System 2 outputs direct MPC cost function with failure threshold, history log records MPC costs instead of STL robustness traces.

Table 1: Real-world success rates by constraint type. STeP improves across all, with largest gains on temporal constraints.

4.2 RQ2: Learned Policy/Motion Planning Switching

Trained ResNet-based BC policy (30 demonstrations) to pick cube from chest, placing obstacle on approach path at test time. STL monitor tracks whether arm maintains safe distance from obstacle. When robustness drops below threshold, subtask reassigned from learned policy to MPC with obstacle avoidance cost. MPC reaches pre-grasp region, learned policy resumes for contact-rich grasp.

Table 2: Learned policy/MPC switching results. STL robustness provides a practical switching signal between learned policy and MPC.

Without switching, BC policy collides in 28/30 trials; MPC alone succeeds at avoidance but fails at grasp in 24/30. The switching mechanism makes both complementary—STL robustness provides the practical switching signal.

4.3 RQ3: Few-Shot Replanning

Evaluates whether STL violation traces enable more targeted plan corrections than informal failure feedback. Task: stack three cubes, failures most often during third placement—robot approaches existing stack too low and knocks it over. 16/20 first attempts fail.

Table 3: Few-shot replanning results. STL violation traces (violated constraint, robustness margin, violation timestep) enable more structured feedback than scalar MPC cost for more targeted recovery.

STL monitor records violated constraint (Safe End-Effector), its robustness margin, and violation timestep, returning to System 2 with updated scene snapshot of displaced cubes. On next attempt, VLM uses this structured feedback to increase approach height and update placement target. Baseline often overcorrects approach height or regenerates full plan rather than adjusting specific failed parameter.

5.

状态-观测映射到潜在空间

$$ z_{t}=\psi(s_{t},o_{t})\in\mathcal{Z} $$

可微最大值近似

$$ \max(\mathbf{x})\approx\frac{\sum_{i=1}^{n}x_{i}\exp(\beta x_{i})}{\sum_{i=1}^{n}\exp(\beta x_{i})} $$

鲁棒性裕度

$$ \rho(z_{t},\mu_{j,c})=\mu_{j}(z_{t})-c $$

Limitations & Future Work

• Only MPC optimizes STL directly (author-stated): Only MPC-based skills directly optimize actions w.r.t. STL specification. Learned policies monitored by STL robustness but don't yet use specification as inference-time control signal.
• Linear subtask sequence (author-stated): High-level plan represented as subtask sequence, limiting branching or cyclic behaviors compared to full automaton.
• Simple components (author-stated): MPC solver, grasp-pose selection, and real-world execution loop deliberately simple, struggling in cluttered environments.
• Incomplete VLM specs (author-stated): VLM can still produce incomplete or incorrect task specifications, especially when fine spatial details are missing from scene description.

6. Conclusion

STeP is a hierarchical framework using Signal Temporal Logic as a shared representation between language-based task reasoning and low-level robot execution. Instead of treating language instructions as informal prompts to a policy, STeP converts spatial, temporal, and logical requirements into STL specifications that can be validated before execution, optimized through MPC, monitored during execution, and reused during replanning. The framework combines STL-guided MPC for constraint-sensitive subtasks with learned policies for contact-rich behaviors, while using STL robustness to detect failures and provide structured feedback. Across various real-world manipulator tasks, results show this formal interface improves constraint satisfaction, supports switching between execution modes, and enables more targeted recovery after intermediate failures. These findings indicate language-conditioned robots can benefit from an explicit specification layer between high-level VLM reasoning and low-level control, rather than relying on a single learned policy to implicitly satisfy all task requirements.