[DRAFT] Signal Temporal Logic for Verifiable Robot Actions

The Problem With "Just Follow the Instruction"

Vision-language-action (VLA) models turn natural language into robot motion, but "pick up the red block, then place it gently on the shelf without knocking over the vase" hides constraints a raw policy has no way to check: an ordering constraint (pick before place), a qualitative one (gently), and a safety one (don't touch the vase, ever, not just at the end). A policy that only optimizes for reaching a goal state can satisfy the letter of the instruction while violating all three along the way.

Signal Temporal Logic (STL) gives a formal language for exactly this class of constraint — properties over continuous signals and time — plus a numeric measure of how well or badly a trajectory satisfies them. A recent paper, [STeP: Signal Temporal Logic for Precise VLA Action Generation](https://arxiv.org/abs/2607.18580v1) (2026-07-20), uses this to bridge VLM-produced instructions and robot execution: instructions are decomposed into STL specifications, which then drive runtime verification and replanning instead of just conditioning a policy end-to-end.

STL in Brief

STL formulas are built over predicates on a real-valued signal $\mathbf{s}(t)$ (e.g. end-effector position, gripper aperture, distance to an obstacle). A predicate $\mu$ is a comparison like $f(\mathbf{s}(t)) \geq 0$. Formulas combine predicates with Boolean connectives and timed temporal operators:

• $\mathbf{G}_{[a,b]}\varphi$ — globally: $\varphi$ holds at every instant in $[a,b]$.
• $\mathbf{F}_{[a,b]}\varphi$ — finally: $\varphi$ holds at some instant in $[a,b]$.
• $\varphi_1\,\mathbf{U}_{[a,b]}\,\varphi_2$ — until: $\varphi_1$ holds until $\varphi_2$ becomes true within $[a,b]$.

The vase constraint above is a global safety property; "place gently" is a bound on velocity at the moment of contact; "pick before place" is an until. All three are expressible, all three are checkable against a recorded or predicted trajectory.

Robustness, Not Just True/False

The feature that makes STL useful for control (rather than just for offline verification) is quantitative robustness semantics $\rho(\varphi, \mathbf{s}, t)$: a real number whose sign matches Boolean satisfaction, and whose magnitude is a margin.

$\rho \geq 0$ means the property holds, and $\rho$'s value is how much slack there is — a trajectory that clears an obstacle by 2 cm and one that clears it by 20 cm are both "safe," but only the robustness value tells you which one to trust under noise. This is what makes STL specs usable as a cost signal for replanning rather than only a pass/fail gate: a planner can locally search for trajectories that increase $\rho$ near-zero regions instead of restarting from scratch on any violation.

Worked Example: Pick, Then Place Gently, Never Near the Vase

Take the instruction from the introduction. Let $d_v(t)$ be the distance from the end-effector to the vase, $g(t) \in {0,1}$ be gripper-closed state, and $v_z(t)$ be vertical velocity at contact. A reasonable STL encoding over horizon $[0, T]$:

Each conjunct is independently checkable, and their $\min$-combined robustness gives a single scalar the planner can monitor online. If $\rho$ dips toward zero near the vase term specifically, the replanner knows which sub-constraint is under threat — something a monolithic learned reward can't localize.

def robustness_conjunction(rhos: list[float]) -> float:
    """STL AND: robustness of a conjunction is the min of the conjuncts."""
    return min(rhos)

def globally_min(signal_at_t: list[float]) -> float:
    """STL G[a,b]: robustness is the min robustness over the window."""
    return min(signal_at_t)

Why This Matters for VLA Robustness

Most VLA robustness work targets the perception-to-action mapping: better vision backbones, more training data, longer context. STL-based approaches attack a different failure mode — the policy can be locally competent and still produce a globally wrong trajectory because nothing checked the temporal structure of the task. Compiling language into STL specs (rather than just embeddings) also makes the constraint inspectable: you can read $\varphi$, disagree with how the VLM decomposed the instruction, and fix the spec directly, instead of debugging a black-box reward.

The tradeoff is upfront: STL decomposition depends on the language-to-spec translation being correct, and predicates like "gently" require someone (a human or a learned mapping) to pick concrete thresholds like $v_{\max}$. Formalization doesn't remove the ambiguity in natural language — it just moves the ambiguity to a place where it's checkable.