---
kind: concept
slug: signal-temporal-logic
title: Signal temporal logic
summary: >-
  How to write timed rules over real-valued signals and turn them into a controller cost. Robustness degree gives a signed margin, and a smooth encoding makes it solvable inside a nonlinear MPC. One card so far, author-reported, on bipedal push recovery.
tags: [formal-methods, model-predictive-control, robotics, safety]
papers: ["2403.15993"]
related: [model-predictive-control, temporal-logic-runtime-monitoring, control-barrier-function, functional-safety]
status: draft
updated_at: 2026-10-25
---

## Overview

Signal temporal logic (STL) states rules over real-valued signals with time
bounds, such as "within two steps, the state must enter a safe set and stay
inside it". Each atomic predicate has the form μ(y) − c ≥ 0. Predicates are
combined with negation, conjunction, disjunction, and the temporal operators
eventually, always and until [arxiv:2403.15993 §IV-A] [arxiv:2403.15993 eq. 4].

The reason to use STL in a controller is the robustness degree. Instead of a
yes or no answer, it returns a signed number: positive when the rule holds,
and larger when it holds with more room. Negation flips the sign. Conjunction
takes a minimum, disjunction a maximum, eventually a maximum over a window,
and always a minimum over a window [arxiv:2403.15993 tab. 2]
[arxiv:2403.15993 §IV-A]. Maximising that number gives a controller a
graded goal, not just a feasibility check.

Evidence is thin. The one card covers a single robot and reports its results
as author-reported. Treat the encoding choices below as options to test, not
as settled practice [arxiv:2403.15993 §VII] [arxiv:2403.15993 §VIII-C].

## Variants

### Exact mixed-integer encoding

The Boolean structure of the specification is written with binary variables,
so the planner is a mixed-integer program. The authors use this as their
baseline. It finds the global optimum of the robustness objective in their
test, and its solve time grows quickly with the horizon [arxiv:2403.15993
§V-B] [arxiv:2403.15993 tab. 3]. Card: [Robust-Locomotion-by-Logic](/papers/2403.15993).

### Smooth-operator encoding in a nonlinear program

The min and max operators in the robustness are replaced by smooth
approximations, each with a positive constant. The result is a nonlinear
program that a standard NLP solver can handle. In the authors' test it solves
several times faster than the exact encoding, but it reaches a local optimum
with lower robustness [arxiv:2403.15993 §V-B] [arxiv:2403.15993 tab. 3]. Card:
[Robust-Locomotion-by-Logic](/papers/2403.15993).

### Eventually-within-horizon obligations instead of fixed timing

A recovery event, here the apex of the step, is required to occur somewhere
within the horizon, not at a pre-set knot. The paper argues that fixing the
timing makes the motion conservative [arxiv:2403.15993 §V-A]. Its recovery
condition is stated as a liveness property over the horizon
[arxiv:2403.15993 §III-B]. In one ablation case, fixed apex timing fails
where the full method recovers [arxiv:2403.15993 §VIII-F].

## When to use which

| Situation | Use | Why |
|---|---|---|
| Small horizon, global optimum needed for a check | Exact mixed-integer encoding | The authors' test reaches the global robustness optimum [arxiv:2403.15993 tab. 3] |
| Horizon grows, real-time re-planning | Smooth-operator NLP | Mean solve times were 0.04 to 0.12 s at horizons of 2 to 4 steps in the authors' test [arxiv:2403.15993 tab. 3] |
| Accepting a local optimum is a risk | Smooth NLP plus a check on the result | The smooth solution was 0.092 against a global 0.100 [arxiv:2403.15993 tab. 3] |
| Event timing is unknown beyond one step | Eventually-within-horizon obligation | Fixed timing was reported as conservative [arxiv:2403.15993 §V-A] |
| Monitoring a finished trace rather than planning | See [temporal-logic runtime monitoring](/concepts/temporal-logic-runtime-monitoring) | That concept covers checking rules on recorded runs, not optimising them |

The timing data come from one robot, one gait, and the authors' solver setup.
Do not assume the speed-up carries over to other systems or solvers.

## Implementation sketch

The shared core is the same across variants: write the rule, compute its
robustness on the predicted trajectory, and add it to the cost. The smooth
variant replaces each min with a soft minimum. The paper gives the soft
minimum as a log-sum-exp form that under-approximates the minimum for a
positive constant [arxiv:2403.15993 eq. 7] [arxiv:2403.15993 §V-B]. The smooth
maximum is also named in eq. 7, but the card does not state its exact form, so
check the source before copying it.

```pseudocode
# Soft minimum of the robustness terms  [arxiv:2403.15993 §V-B] [eq. 7]
def soft_min(rhos, k1):
    # Under-approximates min(rhos) for k1 > 0  [arxiv:2403.15993 §V-B]
    return -log(sum(exp(-k1 * r) for r in rhos)) / k1

# Robustness of the stability clause, as a cost term  [arxiv:2403.15993 §VI-A]
def stability_robustness(traj, horizon_knots):
    # Eventually over the last step is a max over the window  [arxiv:2403.15993 §V-A]
    inner = [soft_min(predicate_margins(y), k1)
             for y in traj[horizon_knots]]
    return soft_max(inner, k2)

# Objective: effort minus robustness  [arxiv:2403.15993 §VI-A] [eq. 8]
# The weight w on effort is small, favouring the specification  [§VII]
def cost(traj, controls, w):
    # Squared swing-foot velocities over all knots  [arxiv:2403.15993 §VI-A]
    effort = sum(u ** 2 for u in controls)
    return w * effort - stability_robustness(traj, horizon_knots)
```

The constants k1 and k2 are not given in the paper. Choose them and report
the values you use [arxiv:2403.15993 §V-B].

## Contradictions

Within the one paper, two reported figures do not match the rest of the text.

- **Solve-time ratio.** The text says the exact encoding is 5 to 10 times
  slower [arxiv:2403.15993 §VIII-C]. The mean solve times in the table give
  about 7.6 times at N = 2, about 17 times at N = 3, and about 19 times at
  N = 4 [arxiv:2403.15993 tab. 3]. Use the table.
- **Impulse tolerance.** The conclusion claims an 81 % increase in maximum
  impulse tolerance during leg crossing [arxiv:2403.15993 §XI]. The body shows
  the comparison only in a figure without tabulated values
  [arxiv:2403.15993 fig. 15], so the 81 % figure cannot be checked from the text.

## Papers

- [Robust-Locomotion-by-Logic](/papers/2403.15993): STL robustness as the MPC objective for Cassie push recovery, with exact and smooth encodings compared.