安全层设计基础：STL、CBF、HTN与EKF

本章为三层架构的每一层提供形式化工具基础。工具不是随意选择的——每种工具的数学结构恰好匹配对应层次的约束类型。理解这种对应关系，是理解EICPS架构设计理由的关键。

8.1 信号时序逻辑（STL）：时间约束的形式化语言

8.1.1 STL语法与语义：从直觉到精确定义

信号时序逻辑（Signal Temporal Logic，STL）是时序逻辑（LTL/CTL）向连续信号的扩展。STL公式 $\phi$ 在信号 $\mathbf{x}: \mathbb{R}_{\geq 0} \to \mathbb{R}^n$ 上求值，其核心语法包括：布尔原子命题（如 $h(x) > 0$，“当前处于安全区内”）、时序算子 $\mathbf{G}_{[a,b]}\phi$（“在时间段 $[a,b]$ 内 $\phi$ 始终成立”）、$\mathbf{F}_{[a,b]}\phi$（“在时间段 $[a,b]$ 内 $\phi$ 至少成立一次”）、以及布尔组合（$\phi_1 \wedge \phi_2$，$\phi_1 \vee \phi_2$，$\neg\phi$）。

STL的核心优势在于其鲁棒语义：布尔满足/不满足之外，STL定义了实数值的鲁棒度 $\rho(\phi, \mathbf{x}, t)$，度量信号在时刻 $t$ 满足公式 $\phi$ 的”裕量”。$\rho > 0$ 表示满足，$\rho < 0$ 表示违反，$|\rho|$ 的大小表示满足/违反的程度。这一鲁棒语义使得STL可以作为Spine层的实时监控工具：鲁棒度的正负判断给出满足性，鲁棒度的绝对值给出安全余量的量化估计。

8.1.2 STL规约的设计模式：带电作业场景的典型规约

带电作业场景中的STL规约设计遵循三类模式。安全间距规约：$\phi_{\mathrm{safe}} = \mathbf{G}_{[0,T]}(h_{\mathrm{elec}}(T_{\mathrm{ee}}) \geq d_{\min})$，要求末端执行器在整个执行时间段 $[0,T]$ 内与带电体的距离始终不低于法定最小安全距离 $d_{\min}$（依电压等级为0.6m或更大）。任务完成规约：$\phi_{\mathrm{complete}} = \mathbf{F}_{[0,T_{\max}]}(q_{\mathrm{sem}} \in \mathcal{S}_{\mathrm{goal}})$，要求任务在最大允许时间 $T_{\max}$ 内至少完成一次（到达目标语义状态）。操作质量规约：$\phi_{\mathrm{quality}} = \mathbf{G}_{[t_{\mathrm{ops}}, t_{\mathrm{ops}}+T_{\mathrm{ops}}]}(\dot{T}_{\mathrm{ee}} \leq v_{\max})$，要求在精细操作阶段速度不超过限制。

8.1.3 STL在线监控的计算复杂度

STL在线监控需要在每个监控周期（100ms）内完成对当前信号片段的鲁棒度计算。对于嵌套时序算子的复杂规约，这可能是一个耗时的计算任务。通过两项优化措施，EICPS将STL监控的计算代价控制在100ms预算内：（1）增量计算：利用STL的时序结构，将鲁棒度计算分解为可增量更新的子问题，避免每次重新计算整个信号历史；（2）规约简化：Brain层在下发规约包时，优先使用经过事先简化（合并冗余约束）的规约形式，减少在线计算量。在第10章中，规约包的编译优化将作为形式证据链生成的组成部分被处理。

写作占位 — STL在线监控计算复杂度的定量分析（待实验数据）

8.2 控制障碍函数（CBF）：执行安全的实时保证

8.2.1 CBF理论基础：从不变集到控制律约束

控制障碍函数（Control Barrier Function，CBF）是一种系统化工具，将安全集的前向不变性转化为控制输入的线性约束。对连续时间控制系统 $\dot{x} = f(x) + g(x)u$，若存在连续可微函数 $h: \mathcal{X} \to \mathbb{R}$ 满足：$\mathcal{S} = \{x \in \mathcal{X} : h(x) \geq 0\}$（安全集由 $h$ 的超水平集定义），且存在 $\mathcal{K}$ 类函数 $\alpha$ 使得 $\sup_{u \in \mathcal{U}} [\nabla h(x) \cdot f(x) + \nabla h(x) \cdot g(x) u] \geq -\alpha(h(x))$，则 $h$ 是 $\mathcal{S}$ 的CBF，且在满足 CBF 条件 $\dot{h}(x, u) + \alpha(h(x)) \geq 0$ 的控制律下，$\mathcal{S}$ 是前向不变的。

这意味着安全性保证不依赖于特定的控制律，而是作为一个约束嵌入控制律设计中：任何满足CBF条件的控制输入都是安全的，给控制器设计留下了最大的自由度（第9章利用这一自由度优化任务性能）。

从理论谱系看，CBF 并非孤立发明，而是两条独立发展的理论河流汇合的产物。第一条河流来自计算机科学的程序逻辑与模型检验传统（Floyd–Hoare 逻辑、Pnueli 的时序逻辑、Clarke–Emerson–Sifakis 的模型检验），它回答”如何精确描述并机械验证系统性质”，但只能处理有限状态系统；第二条河流来自控制理论的稳定性传统——Lyapunov（1892）用能量函数证明”好事持续发生”，而 Nagumo（1942）给出了”坏事永远不发生”的几何刻画：集合 $\mathcal{S} = \{x : h(x) \geq 0\}$ 在动力学 $\dot{x} = f(x)$ 下正向不变，当且仅当边界上向量场不指向集合外部（$h(x)=0 \Rightarrow \nabla h(x) \cdot f(x) \geq 0$）。Nagumo 定理此后数十年停留在分析层面——只能判断给定集合是否不变，无法在存在控制输入时主动维持不变性。上一段给出的 CBF 定义正是 Ames 等人（2017）对 Nagumo 条件的控制论推广：引入 $\mathcal{K}$ 类函数 $\alpha$ 允许 $h$ 在集合内部适度下降，并将条件转化为对控制输入 $u$ 的线性约束，从而使前向不变性成为可以在线优化维持的性质。第一条河流贡献了规约语言（STL 即其连续信号扩展，见§8.1），第二条河流贡献了执行机制（CBF），两者在本章的工具组合中重新汇合——这一历史脉络的完整梳理见知识库 Q-28。

8.2.2 SE(3)框架下的CBF正确形式

经典CBF理论假设欧氏状态空间，直接应用于 $\mathrm{SE}(3)$ 上的位姿控制存在根本性错误（欧氏近似）。在 $\mathrm{SE}(3)$ 框架下，CBF条件需要用李导数（Lie derivative）重新表达（第4章§4.5.2已给出公式）：

$\mathcal{L}_f h(T) + \alpha(h(T)) \geq 0$

其中 $\mathcal{L}_f h(T) = \langle \mathrm{grad}_{\mathrm{SE}(3)} h(T), f(T, u) \rangle_{\mathfrak{se}(3)}$ 使用 $\mathfrak{se}(3)$ 内积而非欧氏内积。这一区别在高曲率位姿区域（如大角度旋转时）会产生可量化的安全裕量误差，是安全关键系统中不可忽视的系统性偏差。

8.2.3 CBF约束的QP实现：实时安全过滤器

在每个Body控制时步（10ms），CBF约束通过以下二次规划（QP）实现安全过滤：

$u^* = \arg\min_{u} \|u - u_{\mathrm{nom}}\|^2 \quad \text{s.t.} \quad \mathcal{L}_f h(T) + \mathcal{L}_g h(T) u + \alpha(h(T)) \geq 0$

其中 $u_{\mathrm{nom}}$ 是Body层的名义控制输入（来自任务导向的控制律），$u^*$ 是在保持距 $u_{\mathrm{nom}}$ 最近的前提下满足CBF约束的安全控制输入。当 $u_{\mathrm{nom}}$ 本身满足CBF约束时，$u^* = u_{\mathrm{nom}}$（CBF不干预）；当 $u_{\mathrm{nom}}$ 违反CBF约束时，$u^*$ 是最小修正后的安全替代。这种设计保证了CBF的”最小侵入性”——仅在必要时介入控制。

8.3 HTN规划：任务分解的层级结构

8.3.1 HTN的基本形式化：方法与算子

层级任务网络（Hierarchical Task Network，HTN）规划以任务（Task）为基本单位，分为两类：复合任务（compound task）需要通过”方法”（method）分解为子任务序列，原始任务（primitive task，又称算子operator）可以直接执行。方法定义了一组前置条件（precondition）和分解方案（subtask sequence）：当前状态满足前置条件时，复合任务可以通过该方法分解为对应的子任务序列。HTN规划器从初始任务出发，递归应用方法，直到所有任务都分解为原始任务，生成一个可直接执行的动作序列。

在EICPS中，原始任务对应Spine层能够监控的最小执行单元（有对应STL规约的子任务）；复合任务对应Brain层的高层任务分解逻辑（来自LLM的规划输出）。

8.3.2 HTN与LLM的集成策略

大语言模型（LLM）在HTN框架中的角色是方法生成器：给定高层任务描述，LLM根据领域知识生成备选分解方案，由HTN规划器验证其合法性（前置条件是否在当前状态下满足）并选取可执行方案。这种”LLM生成 + 符号验证”的集成策略，既利用了LLM丰富的领域知识，又通过HTN的形式化结构过滤了不合法的分解方案。

V-PLN验证（第12章）的核心工作就是量化这一过滤机制的有效性：LLM生成的分解方案中，有多大比例能通过HTN合法性验证？不通过验证的方案（对应LLM幻觉）能否在执行前被可靠识别？

8.3.3 HTN库的构建与维护

EICPS的HTN方法库来自两个来源：规程文档解析（将带电作业技术规程DL/T 966—2005中的操作步骤解析为HTN方法）和专家经验编码（由领域专家将实操经验提炼为HTN方法的前置条件和效果描述）。方法库的质量直接决定了Brain层的规划能力：方法库中没有对应方法的任务，HTN规划器无法处理。这是规范闭合性假设在架构设计中的具体体现——V-167词汇集对应的不仅是语义空间的覆盖，更是HTN方法库的完备性。

8.4 扩展卡尔曼滤波（EKF）：状态估计的概率框架

8.4.1 EKF的基本流程与 SE(3) 适配

扩展卡尔曼滤波的基本流程——预测（predict）和更新（update）——在EICPS的Body层中被适配到 $\mathrm{SE}(3)$ 状态空间上。预测步：基于运动学模型（控制输入 $u \in \mathfrak{se}(3)$）预测下一时刻状态 $\hat{T}^- = \hat{T} \cdot \exp(\xi^\wedge \Delta t)$，协方差矩阵通过雅可比矩阵（在 $\mathfrak{se}(3)$ 中线性化）传播。更新步：将传感器测量值（视觉里程计位姿、IMU角速度积分）与预测值做对比，计算残差（在 $\mathfrak{se}(3)$ 中）并用卡尔曼增益加权校正。

SE(3)适配的关键是在李代数 $\mathfrak{se}(3)$（线性空间）中执行所有线性代数运算，通过指数/对数映射在 $\mathrm{SE}(3)$ 和 $\mathfrak{se}(3)$ 之间转换，避免了直接在非线性流形上进行线性操作的错误。

8.4.2 多传感器融合策略

带电作业场景中，Body层融合三类传感器数据：视觉里程计（相机图像序列，提供位姿估计，精度高但在遮挡或低纹理环境下可能退化）、IMU（惯性测量单元，提供高频角速度和加速度，短期精度高但积分漂移明显）、关节编码器（提供关节角度，通过正运动学映射到末端执行器位姿，精度高但依赖机械标定质量）。EKF的多传感器融合通过不同传感器的测量噪声协方差矩阵进行加权，在每个传感器可用时将其纳入更新步，在传感器失效时自动降级到剩余可用传感器的组合。

8.4.3 状态估计不确定性对安全判定的影响

Spine层的CBF安全判定依赖Body层的状态估计 $\hat{T}$，但状态估计存在不确定性（协方差矩阵 $P$）。当状态估计不确定性较大时（$P$ 的迹较大），CBF条件 $h(\hat{T}) \geq 0$ 可能在真实状态下被违反。EICPS通过鲁棒CBF处理这一问题：将CBF条件修改为 $h(\hat{T}) \geq \epsilon(P)$，其中 $\epsilon(P)$ 是基于估计不确定性自适应设定的安全裕量，当不确定性增大时自动增加安全距离要求。这在形式上是一种保守化处理，以降低任务效率为代价保证安全性——这种权衡在安全关键应用中是必要且合理的。

写作占位 — EKF状态估计精度的实测数据（与SLAM方法的比较）

8.5 四种工具的协同与选型依据综述

8.5.1 工具-层次-约束的三维对应关系

四种工具的选型不是任意的，每种工具恰好对应一类约束类型和一个架构层次：STL捕获时序约束（任务必须在时间窗口内按序完成），分配给Spine层的监控职责；CBF捕获不变性约束（安全集的前向不变性），分配给Spine-Body接口的实时仲裁；HTN捕获层级组合约束（复杂任务的合法分解结构），分配给Brain层的规划职责；EKF捕获不确定性约束（噪声环境下的状态估计），分配给Body层的感知职责。这种对应关系使得每个工具在其适用的约束类型上发挥最大效用，而不是用一种工具强行覆盖所有约束（单一工具方案的常见失效模式）。

8.5.2 工具间的信息流与依赖关系

四种工具之间存在单向信息流：EKF提供状态估计 $\hat{T}$，CBF利用 $\hat{T}$ 实时计算安全约束，STL利用 $\hat{T}$ 的历史轨迹评估规约满足性，HTN利用STL反馈的任务进度状态更新规划树。这种单向流避免了工具间的循环依赖（可能引发死锁或不一致），同时保证了信息从最原始的传感器数据（EKF入口）流向最抽象的任务决策（HTN出口）的完整路径。形式证据链的生成正是沿着这条信息流方向记录每一步的输入输出，在第10章中具体展开。

8.5.3 工具选型的理论充分性与实践必要性

“为什么不用其他工具替代”是架构设计决策中需要正面回答的问题。为什么用STL而非LTL：LTL在布尔信号上定义，无法提供连续的鲁棒度量，而带电作业的安全余量（距离带电体的距离）是连续量，需要定量监控而非仅仅布尔判断。为什么用CBF而非MPC：模型预测控制（MPC）能提供更强的最优性保证，但其计算复杂度（解多步预测优化问题）在10ms控制周期内难以保证实时性；CBF的QP求解在凸约束下有解析解或近似解，计算复杂度可控。为什么用HTN而非PDDL：标准PDDL规划器在大规模任务空间中的搜索开销过高；HTN通过层级结构剪枝搜索空间，与LLM生成的结构化分解方案自然结合。

上述逐项论证之外，这套工具组合还有一个整体性的学术背书：STL 与 CBF 构成的形式化安全链，正是 Fan（范楚楚，MIT）在《Formal Methods for Safe Autonomy》（ACM Books, 2023）中系统化的 Safe Autonomy 研究纲领的核心工具。该纲领的中心命题——自主系统应在形式化约束下运行，用数学证明而非测试统计建立行为边界——与本书的形式化自主目标同构。两者是上下游关系：Safe Autonomy 提供工具并证明其数学性质（前向不变性、鲁棒度语义），本书回答这些工具在一个具有三类异质状态空间的具身系统中应放在哪一层、以什么频率运行、通过什么接口交互。该纲领同时提供了本书架构论证的一个关键支点：自主度越高，对形式化保证的需求越强——遥操作模式下操作员承担实时安全判断，转向 Human-on-the-Loop 自主操作后，这一职责必须由形式化机制接替，形式化验证由此从可选项变为不可缺失项。

8.6 形式化可处理性：工具适用的边界与硬件设计的反推

8.6.1 三个可处理性条件

本章介绍的工具并非无条件可用。对一个动力系统应用 CBF 与 STL 形式化验证，系统必须同时满足三个条件。条件一（有限维状态表示）：存在 $n < \infty$ 使系统完整状态可表示为 $x \in \mathbb{R}^n$，且 $n$ 在设计时已知。条件二（解析动力学）：存在连续可微且具闭合形式的 $f$ 使 $\dot{x} = f(x, u)$，保证 CBF 的李导数可解析计算而非依赖数值积分。条件三（实时可解性）：CBF-QP 可在控制周期内完成求解，这要求 $n$ 不能过大、$h$ 的形式不能过于复杂。三个条件分别对应 CBF 机制的三个环节——状态表示、约束构造、在线优化——任何一环失效，形式化安全保证即整体失效。

8.6.2 反例：连续接触方案的结构性失败

Prj167 的原始作业设计（机械臂持续施力于导线，模仿人工作业的连续接触模式）为三个条件提供了一个完整的反例。架空导线是三维连续体，其完整状态是向量值函数 $\mathbf{w}(\cdot, t) \in [L^2([0,L])]^4$（竖向、水平、纵向位移与扭转角四个分量，各自满足偏微分方程）——这是无穷维 Hilbert 空间中的元素。机械臂（有限维 ODE）与导线（无穷维 PDE）力学耦合后，合并状态空间不再有任何有限维表示，条件一失效；$\partial h / \partial \mathbf{w}$ 成为无穷维空间上的 Fréchet 导数，无有限维闭合形式，条件二失效；STL 规约信号依赖 PDE 数值解且含连续区间上的最小化搜索，无法在控制周期内评估，条件三失效。

需要强调的是失败的性质：三重障碍源自同一根因（连续体与有限维系统的耦合）但相互独立，且均为数学前提不成立——更换处理器、更快的 QP 求解器或模态截断近似都不能恢复形式化保证（截断丢弃的高阶模态恰好会被接触力激励，其能量未被纳入安全证明，误差界不可控）。这是结构性失败而非工程能力不足，其详细论证见知识库 Q-24。

8.6.3 从验证约束反推硬件：分离式设计

结构性失败的诊断直接给出了硬件设计的推导路径：既然三个条件是形式化验证的必要前提，硬件方案必须使每个作业阶段都满足它们。由此逆向反推出分离式设计——作业分解为定位锁紧与工具独立操作两个阶段：锁紧阶段机器人刚性固定于导线，接触力由锁紧机构承受，机械臂状态回到 $q \in \mathbb{R}^6$ 的有限维 ODE；作业阶段末端工具在空间中独立运动，动力学为标准操作臂方程，CBF-QP 可在控制周期内求解；阶段间的切换由 Flow-Jump 框架（第6章）作为离散跳变统一处理，不引入新的连续耦合。

这一推导颠倒了常见的设计次序：不是先有工程方案再寻找理论解释，而是由形式化验证的代数前提决定什么样的硬件设计是被允许的。分离式设计因此不是可以在后续迭代中”优化掉”的工程选项，而是当前场景下形式化安全保证的必要前提；任何替代方案（例如某种软接触持续操作）在采纳前必须先证明其满足全部三个条件。本书将这一”从验证约束反推机械结构”的路径视为 EICPS 方法论的组成部分；其成立范围的限定与”唯一性”表述的证明地位，在第15章§15.5 中作为已知局限明确讨论。

本章建立了四种核心工具的理论基础。第9章进入具体实现——分层控制的实现细节与ESTL任务语言的设计。

参考文献

写作占位 — 本章参考文献列表（随正文写作逐步完善）