文档中心 / 数学讲义

第八讲：STL 信号时序逻辑

STL（Signal Temporal Logic）把时序约束从自然语言变成可计算的数学对象：鲁棒度 ρ\rho 不仅告诉你规约”满足还是违反”，还定量描述”满足/违反了多少”——这正是 EICPS EvidencePack 将安全判定机械化的核心工具。

符号含义
φ\varphiSTL 规约公式
x(t)\mathbf{x}(t)连续时间信号（状态轨迹）
(x,t)⊨φ(\mathbf{x}, t) \models \varphi信号 x\mathbf{x} 在时刻 tt 满足公式 φ\varphi
ρ(φ,x,t)\rho(\varphi, \mathbf{x}, t)鲁棒度（正 = 满足裕量，负 = 违反程度）
G[a,b] φ\mathbf{G}_{[a,b]}\,\varphi全局（Globally）：[a,b][a,b] 内始终满足 φ\varphi
F[a,b] φ\mathbf{F}_{[a,b]}\,\varphi最终（Finally）：[a,b][a,b] 内某时刻满足 φ\varphi
φ1 U[a,b] φ2\varphi_1\,\mathbf{U}_{[a,b]}\,\varphi_2直到（Until）：φ1\varphi_1 持续直到 φ2\varphi_2 在 [a,b][a,b] 内成立

前言：理论发展沿革

1977 年，阿米尔·普努利（Amir Pnueli）将**线性时态逻辑（LTL）**引入程序验证，奠定了形式化规约的基础，并因此获得 1996 年图灵奖。LTL 用 G（全局）、F（最终）、U（直到）描述离散事件系统的时序性质，但无法处理连续时间信号——而真实的物理系统从不离散。

2004 年，Oded Maler 与 Dejan Nickovic 发表了开创性论文 Monitoring Temporal Properties of Continuous Signals，提出 MTL（Metric Temporal Logic）的连续信号扩展——即后来被称为 STL 的框架。STL 保留了 LTL 的算子语法，同时允许公式作用于连续时间信号，并引入了鲁棒度语义：规约满足与否不再是布尔二值，而是一个实数，量化满足裕量或违反深度。

2012 年，Donzé 与 Maler 进一步系统化了鲁棒度语义，开发了 Breach 工具箱，使 STL 从理论走向工程实践。此后，STL 在自动驾驶（Uber ATG、Waymo 测试框架）、航空航天任务规划和机器人运动规划中广泛应用。

在 EICPS 框架中，STL 承担双重角色：接口A将语言指令打包为 STL 规约传入 Brain 层；EvidencePack 的 STL 门在任务结束时计算鲁棒度，给出机械可验证的安全判定。

1 STL 语法

STL 公式在原子谓词 μ:Rn→R\mu: \mathbb{R}^n \to \mathbb{R} 上递归构造：

φ::=⊤∣μ(x)>0∣¬φ∣φ1∧φ2∣G[a,b] φ∣F[a,b] φ∣φ1 U[a,b] φ2\varphi ::= \top \mid \mu(\mathbf{x}) > 0 \mid \neg\varphi \mid \varphi_1 \wedge \varphi_2 \mid \mathbf{G}_{[a,b]}\,\varphi \mid \mathbf{F}_{[a,b]}\,\varphi \mid \varphi_1\,\mathbf{U}_{[a,b]}\,\varphi_2

三个时序算子的直观含义：

  • G[a,b] φ\mathbf{G}_{[a,b]}\,\varphi：在时间区间 [t+a, t+b][t+a,\, t+b] 内，φ\varphi 始终成立
  • F[a,b] φ\mathbf{F}_{[a,b]}\,\varphi：在时间区间 [t+a, t+b][t+a,\, t+b] 内，φ\varphi 至少一次成立
  • φ1 U[a,b] φ2\varphi_1\,\mathbf{U}_{[a,b]}\,\varphi_2：φ1\varphi_1 持续成立，直到 φ2\varphi_2 在 [t+a, t+b][t+a,\, t+b] 内成立

工程语言示例：“无人机在任务全程保持距离障碍物 2 m 以上”写作：

G[0,T]  (dobs(x(t))≥2.0)\mathbf{G}_{[0,T]}\;\bigl(d_{obs}(\mathbf{x}(t)) \geq 2.0\bigr)

2 鲁棒度语义

鲁棒度 ρ\rho 递归定义，使得 (x,t)⊨φ⇔ρ(φ,x,t)>0(\mathbf{x},t) \models \varphi \Leftrightarrow \rho(\varphi,\mathbf{x},t) > 0：

ρ(μ>0, x, t)=μ(x(t))\rho(\mu > 0,\, \mathbf{x},\, t) = \mu(\mathbf{x}(t))

ρ(¬φ, x, t)=−ρ(φ, x, t)\rho(\neg\varphi,\, \mathbf{x},\, t) = -\rho(\varphi,\, \mathbf{x},\, t)

ρ(φ1∧φ2, x, t)=min⁡ ⁣(ρ(φ1,x,t),  ρ(φ2,x,t))\rho(\varphi_1 \wedge \varphi_2,\, \mathbf{x},\, t) = \min\!\bigl(\rho(\varphi_1,\mathbf{x},t),\; \rho(\varphi_2,\mathbf{x},t)\bigr)

ρ ⁣(G[a,b] φ, x, t)=min⁡t′∈[t+a, t+b]ρ(φ, x, t′)\rho\!\bigl(\mathbf{G}_{[a,b]}\,\varphi,\, \mathbf{x},\, t\bigr) = \min_{t^{\prime} \in [t+a,\, t+b]} \rho(\varphi,\, \mathbf{x},\, t^{\prime})

ρ ⁣(F[a,b] φ, x, t)=max⁡t′∈[t+a, t+b]ρ(φ, x, t′)\rho\!\bigl(\mathbf{F}_{[a,b]}\,\varphi,\, \mathbf{x},\, t\bigr) = \max_{t^{\prime} \in [t+a,\, t+b]} \rho(\varphi,\, \mathbf{x},\, t^{\prime})

ρ ⁣(φ1 U[a,b] φ2, x, t)=max⁡t′∈[t+a, t+b]min⁡ ⁣(ρ(φ2,x,t′),  min⁡t′′∈[t,t′]ρ(φ1,x,t′′))\rho\!\bigl(\varphi_1\,\mathbf{U}_{[a,b]}\,\varphi_2,\, \mathbf{x},\, t\bigr) = \max_{t^{\prime} \in [t+a,\, t+b]} \min\!\bigl(\rho(\varphi_2,\mathbf{x},t^{\prime}),\; \min_{t^{\prime\prime} \in [t,t^{\prime}]} \rho(\varphi_1,\mathbf{x},t^{\prime\prime})\bigr)

关键性质：ρ\rho 对信号扰动具有Lipschitz 连续性，可用作梯度优化目标（反事实轨迹搜索、对抗测试生成）。

3 STL 监控算法

对有限长度轨迹 x[0,T]\mathbf{x}_{[0,T]}，在线监控使用区间运算和单调队列，时间复杂度 O(N)O(N)：

对 G[a,b]\mathbf{G}_{[a,b]}，维护滑动窗口最小值队列：

ρkG=min⁡j∈[k+a/Δt,  k+b/Δt]ρjatom\rho_k^G = \min_{j \in [k+a/\Delta t,\; k+b/\Delta t]} \rho_j^{\text{atom}}

对 F[a,b]\mathbf{F}_{[a,b]}，维护滑动窗口最大值队列：

ρkF=max⁡j∈[k+a/Δt,  k+b/Δt]ρjatom\rho_k^F = \max_{j \in [k+a/\Delta t,\; k+b/\Delta t]} \rho_j^{\text{atom}}

实时系统中，监控器在每个控制周期更新一次，无需存储完整历史轨迹——满足 EICPS 脊髓层 1 ms 刷新周期的延迟约束。

4 STL 在 EICPS 中的工程化

4.1 接口 A：语言指令 → STL 载荷

Brain 层的任务输入经接口 A 语义-动力学桥处理后，以 STL 公式的形式打包进 ActionPlan：

Proposal: "巡检区间 [0°, 45°] 内保持对线夹的视线"
   ↓  LLM + 参数提取
ActionPlan.stl_spec: G[0,T]( angle_to_clamp ∈ [0,45] ∧ line_of_sight = True )
ActionPlan.tolerance: ρ_min = 0.05   # 最小安全裕量（弧度）

STL 规约随 ActionPlan 下发给脊髓层，作为执行期间的约束边界。

4.2 EvidencePack：STL 门判定

执行完成后，脊髓层将实际轨迹 x[0,T]\mathbf{x}_{[0,T]} 送入 STL 监控器，输出鲁棒度 ρ∗\rho^*：

ρ∗=ρ(φspec, xactual, 0)\rho^* = \rho(\varphi_{\text{spec}},\, \mathbf{x}_{\text{actual}},\, 0)

EvidencePack 包含完整的判定记录：

EvidencePack={Proposal,  ActionPlan,  xactual,  φspec,  ρ∗,  verdict}\text{EvidencePack} = \{\text{Proposal},\; \text{ActionPlan},\; \mathbf{x}_{\text{actual}},\; \varphi_{\text{spec}},\; \rho^*,\; \text{verdict}\}

verdict={PASSρ∗>ρmin⁡WARN0<ρ∗≤ρmin⁡FAILρ∗≤0\text{verdict} = \begin{cases} \texttt{PASS} & \rho^* > \rho_{\min} \\ \texttt{WARN} & 0 < \rho^* \leq \rho_{\min} \\ \texttt{FAIL} & \rho^* \leq 0 \end{cases}

FAIL 时触发 Flow-Jump 的 Jump，回退到安全模式；WARN 时上报 Brain 层请求重规划。

4.3 安全属性的层次组合

复杂任务的安全属性通过逻辑合取（∧\wedge）组合，鲁棒度取最小值，使得系统对最弱约束最敏感：

φtask=φcollision∧φworkspace∧φpayload\varphi_{\text{task}} = \varphi_{\text{collision}} \wedge \varphi_{\text{workspace}} \wedge \varphi_{\text{payload}}

ρtask∗=min⁡(ρcollision∗,  ρworkspace∗,  ρpayload∗)\rho^*_{\text{task}} = \min(\rho^*_{\text{collision}},\; \rho^*_{\text{workspace}},\; \rho^*_{\text{payload}})

这确保任何一个分项违反都能被整体判定捕获，而不会被其他满足项掩盖。

5 与其他模块的数学联系

相关模块联系方式
CBF（第九讲）CBF 保证 h(x)≥0h(\mathbf{x}) \geq 0 的不变性；STL 用 G[0,T](h>0)\mathbf{G}_{[0,T]}(h > 0) 在事后验证该不变性是否整个轨迹成立
Flow-Jump（第三讲）STL 鲁棒度 ρ≤0\rho \leq 0 是 Jump 集 DD 的判定条件之一
EKF（第十一讲）EKF 输出状态估计 x^\hat{\mathbf{x}}，STL 监控器对估计轨迹 x^[0,T]\hat{\mathbf{x}}_{[0,T]} 计算鲁棒度
HTN（第十讲）每个 HTN 原始任务对应一条 STL 规约，任务成功的形式化条件就是 ρ>0\rho > 0

Notebook

Open In Colab

本讲配套 Colab Notebook 包含：①STL 语法树可视化；②鲁棒度曲线实时计算；③模拟 EvidencePack 判定流程；④对抗轨迹生成（最小化 ρ\rho 的梯度下降）。

延伸阅读

  • Maler, O. & Nickovic, D. (2004). Monitoring Temporal Properties of Continuous Signals. FORMATS.
  • Donzé, A. & Maler, O. (2010). Robust Satisfaction of Temporal Logic over Real-Valued Signals. FORMATS.
  • Lindemann, L. & Dimarogonas, D.V. (2019). Control Barrier Functions for Signal Temporal Logic Tasks. IEEE L-CSS.