安全约束验证

STL（Signal Temporal Logic，信号时序逻辑） 由 Maler & Nickovic 于 2004 年提出，是 EICPS 安全约束形式化的核心工具。给定执行轨迹，STL 工具可以机械地判断时序约束是否满足，不依赖人工审查。EICPS 将 STL 与滚动时域控制（RHC/MPC）结合，实现接口 A 下行的形式化约束传递和 Spine 层的在线验证。

STL 语义与鲁棒度

STL 约束的核心量是鲁棒度 $\rho$ ——描述系统轨迹距约束边界的裕度：

$\rho > 0$ ：约束满足，值越大安全裕度越高
$\rho = 0$ ：恰好在边界上
$\rho < 0$ ：约束违反

Prj167 典型约束（STL-001）：

\varphi = \square_{[0,T]}\; d(x(t),\, \text{wire}) \geq d_{safe}

含义：在整个作业时间 $[0, T]$ 内，机身与带电导线的距离始终不小于安全距离 $d_{safe}$ （500kV 线路：5.0m）。STL 将这一连续约束形式化为可机械验证的规约——Spine 层每 5 秒重新评估 $\rho$ ，无需人工审查。

接口 A 中的 STL 下发

Brain 层将任务意图打包为 STL 规约包 + ETL 任务图，经接口 A 下发给 Spine：

\text{接口 A 下行载荷} = \{\varphi_i\}_{i=1}^{N} \;\cup\; \text{ETL任务图}

Spine 收到后立即生效，旧规约被覆盖。当 Brain 无响应时，Spine 依靠 ZOH（零阶保持）维持最后一次接收的规约集继续运行。

STL-RHC：滚动时域在线验证

Spine 层以**滚动时域控制（RHC）**在线求解 STL 约束满足问题：

ρ > ρ_warn        → 正常执行，继续当前任务
0 < ρ ≤ ρ_warn   → 预警：上报 Brain，降低运动速度，保守策略
ρ ≤ 0             → 强制 Jump → FAILSAFE 模态，所有运动指令挂起

STL-RHC 持续计算预测时域内的鲁棒度 $\rho$ ，确保系统先于违约采取动作，而非事后响应。

安全谱：STL 约束的谱视角

从结构谱角度理解 STL 约束：Prj167 的安全约束 $d(x, \text{wire}) \geq d_{safe}$ 定义了一个安全势能场 $V_{risk}(x)$ ——距带电体越近，势能越高。STL 鲁棒度 $\rho$ 是当前状态在这个势能场中的”安全裕度”， $\rho = 0$ 意味着状态到达了安全势阱的边缘。

安全谱算子：

\mathcal{X}_{safe} = \text{Spec}(-\Delta_{\mathcal{M}} + V_{risk})

特征值 $\lambda_k^{safe}$ 对应不同安全等级的”能级”：低能级（小 $\lambda_k$ ）对应远离障碍物的宽阔区域（高安全），高能级（大 $\lambda_k$ ）对应狭窄走廊或近障碍物区域（低安全）。

STL-RHC 是安全谱 $\mathcal{X}_{safe}$ 的工程实现——谱特征值编码约束难度， $\rho$ 鲁棒度是当前状态的安全裕度，两者在数学上一脉相承。

STL 与 CBF 的互补关系

STL 验证任务完成性（离线规约 + 在线验证）：Brain 层制定”整个作业过程中始终保持安全距离”的时序约束，Spine 层机械验证是否满足。

CBF 保证执行过程安全（在线、连续）：在每个控制周期（1ms）实时求解 QP，强制状态不越出安全集边界——是比 STL 更快的最后防线。

两者在 Spine 层并行运行：STL-RHC 每 5 秒评估（较慢但全局），CBF 每 1ms 介入（极快但局部）。

→ 实时安全监控（CBF） · 接口协议 A/B