Signal Temporal Logic

Definition

Signal Temporal Logic (STL) is a spatiotemporal logic for specifying time-dependent
requirements on the trajectories of a dynamical system, introduced by Maler & Nickovic (cited in
akella2024risk as maler2004monitoring). An STL specification
$\varphi$ is built recursively from atomic predicates by Boolean operators ($\neg$, $\wedge$, and
their derived $\vee$, $\Rightarrow$) and timed temporal operators (until $U_I$, and the derived
eventually $F_I$ and always $G_I$) over a time interval $I$. Beyond a Boolean
satisfied/violated verdict, STL admits a quantitative (robust) semantics ${\rho }^{\varphi }$ that scores
how strongly a signal satisfies (positive) or violates (negative) $\varphi$ — this real-valued
margin is what makes STL useful for risk-aware verification: the robustness becomes a random
variable whose tail (e.g. VaR / CVaR) measures how badly a controller can fail. STL is a formal
specification language and is regime-agnostic — it constrains the signal, not the plant, so it
applies equally to a free-flying or free-floating manipulator once its state trajectory is defined.

Key Equations

Symbols per notation.md. STL specifications here are interpreted over a state
signal $\mathbf{x}:{\mathbb{R}}_{\ge 0}\to {\mathbb{R}}^n$; the symbols below ($\varphi$, $\mu$, $b$,
${\rho }^{\varphi }$, $U_I$, $F_I$, $G_I$) are STL-specific and are not in notation.md.
Caution — local override: here $\varphi$ is the STL specification formula, not the canonical
helix-latitude scalar $\varphi$ of notation.md (guidance scalars: $\varphi ={\varphi }_0+w_{\varphi }u$); disambiguate
by context. Likewise $\mathbf{x}$ here is a generic state signal, not a tracking error.

Syntax (atomic predicate from a real-valued function $b$, then the grammar):

$$\mu (\mathbf{x}(t))=\{\begin{array}{ll}1& b(\mathbf{x}(t))\ge 0\\ 0& \text{otherwise}\end{array}\varphi ::=\top \mid \mu \mid \neg {\varphi }^{\prime }\mid {\varphi }^{\prime }\wedge {\varphi }^{\prime \prime }\mid {\varphi }^{\prime }{U}_I{\varphi }^{\prime \prime }$$

Robust (quantitative) semantics — the recursion that yields the satisfaction margin ${\rho }^{\varphi }$:

$${\rho }^{\mu }(\mathbf{x},t)=\mathrm{Dist}(\mathbf{x}(t),O^{\mu }),{\rho }^{\neg {\varphi }^{\prime }}=-{\rho }^{{\varphi }^{\prime }},{\rho }^{{\varphi }^{\prime }\wedge {\varphi }^{\prime \prime }}=\min ({\rho }^{{\varphi }^{\prime }},{\rho }^{{\varphi }^{\prime \prime }}),$$ $${\rho }^{{\varphi }^{\prime }{U}_I{\varphi }^{\prime \prime }}(\mathbf{x},t)=\underset{t^{\prime \prime }\in t\oplus I}{\sup }\min ({\rho }^{{\varphi }^{\prime \prime }}(\mathbf{x},t^{\prime \prime }),\underset{t^{\prime }\in (t,t^{\prime \prime })}{\inf }{\rho }^{{\varphi }^{\prime }}(\mathbf{x},t^{\prime })),$$

where $O^{\mu }=\{x\in {\mathbb{R}}^n\mid b(x)\ge 0\}$ and $\mathrm{Dist}$ is the signed distance to that set.
Perturbation characterization (as stated in the source): $(\mathbf{x},t)\models \varphi$ iff every
signal ${\mathbf{x}}^{\ast }$ with ${\sup }_t\Vert \mathbf{x}(t)-{\mathbf{x}}^{\ast }(t)\Vert <|{\rho }^{\varphi }(\mathbf{x},t)|$
also satisfies $\varphi$ — i.e. $|{\rho }^{\varphi }|$ is exactly the $\sup$-norm perturbation radius that
preserves the verdict.

Source Support

• akella2024risk — risk-aware planning/control/verification survey;
  presents STL syntax and both the Boolean and robust semantics (sidebars sb:stl_syntax,
  sb:stl_robustness), and motivates using the robustness ${\rho }^{\varphi }$ as the random variable whose
  tail risk (VaR/CVaR) discriminates a “safe” controller from an unsafe one even at equal violation
  probability. The originating STL reference maler2004monitoring is cited there but not in our corpus.

Related Topics

• responsibility_sensitive_safety — both encode safety as a
  formal, checkable specification; RSS gives explicit safe-distance rules, STL gives a temporal-logic
  grammar plus a quantitative margin.
• chance_constraints — a probabilistic-satisfaction view; the STL
  robustness random variable ${\rho }^{\varphi }$ lets a chance constraint $\mathrm{Pr}[{\rho }^{\varphi }\ge 0]\ge 1-\beta$ be
  stated and (via tail measures) sharpened.
• conditional_value_at_risk — the tail risk measure the source
  applies to the robustness ${\rho }^{\varphi }$; ${\mathrm{CVaR}}_{\beta }({\rho }^{\varphi })$ distinguishes controllers
  with equal failure probability but different worst-case severity.
• motion_planning_under_uncertainty — STL robustness can
  serve as the cost/constraint a risk-aware planner optimizes against under stochastic disturbances.

Open Questions

• The source’s verification pipeline samples trajectories of a generic closed-loop system; what is
  the right predicate set $\{\mu \}$ to encode our inspection task (keep-out zones, standoff, pointing
  / versine pointing error, coverage timing) as an STL $\varphi$ for a free-flying
  manipulator?
• STL robustness is a $\sup$-norm margin over a scalar signal; how should it be defined over an
  $\mathrm{SE}(3)$ end-effector pose so the margin respects the rotation metric rather than a raw
  vector difference?
• The survey notes that decomposing a large system-level specification into separately verifiable
  component specs (and the satisfiability of a given $\varphi$) is open — how does this partition for a
  coupled base+arm system where component behaviors are dynamically coupled?