第三部分导言

理论与工程之间，有一道鸿沟不是”将公式翻译成代码”就能跨越的。真正的挑战在于：实时性约束、计算资源的有限性、传感器噪声的不可消除性，这些工程现实会让漂亮的数学在实现中折断。第三部分的任务，是设计一个能让数学理论在工程约束中存活的系统架构。

一个根本性的设计问题

第二部分建立了具身空间的完整数学基础：三流形乘积结构、$\mathrm{SE}(3)$ 的李群几何、规范闭合性给出的 $\mathrm{SEC}=1$、Flow-Jump混合动力学。这是理论层面的完整图谱。

但当我们面对一台真实的机器人，在真实的物理环境中执行真实的任务时，立刻遭遇一个根本性的设计问题：

具身空间中的三个流形，对应的物理过程运行在完全不同的时间尺度上。

Brain层的语义推理——将自然语言任务描述转化为结构化的执行计划——在秒级时间尺度上运行，调用大语言模型或HTN规划器，每次调用耗时数百毫秒到数秒。Spine层的实时安全监控——在线评估STL规约的鲁棒度 $\rho$，触发CBF约束的仲裁——必须在100ms量级内完成，这是不可压缩的物理约束：导线在风荷载下的摆动周期通常为数秒，其中需要完成多次安全检验。Body层的运动控制与状态估计——EKF融合IMU、激光雷达、视觉的多频传感信号——工作在10ms量级的控制周期上。

这三个时间尺度相差两个数量级。如果把它们放在同一个控制循环中处理，要么Brain层的慢速推理让Body层的控制产生无法接受的延迟，要么Body层的高频中断让Brain层的推理永远无法完成。

时间尺度的解耦，是EICPS系统架构设计的第一原则，也是第三部分的核心组织逻辑。

Brain/Spine/Body：解耦而非分离

Brain/Spine/Body三层架构不是简单的功能分层，而是对三个流形动力学时间尺度的工程对应。关键的设计挑战在于：三层必须解耦以保证各自的实时性，但又不能真正分离——因为它们在具身空间中的动力学是耦合的。

这个矛盾的解决，依赖层间接口的精确设计。Brain层向Spine层输出的不是控制指令，而是STL规约——以形式化的时序逻辑公式表达任务约束，而非直接的数值命令。这个接口设计有一个深刻的意义：它将”Brain理解任务的能力”与”Spine保证安全的能力”在功能上分离，同时通过形式化语言保持语义上的精确连接。Spine层不需要”理解”Brain层的规划意图，只需要评估当前行为轨迹是否满足STL规约——这是一个纯粹的形式化判定问题，与任务的语义内容解耦。

Spine层向Body层传递的是经过安全仲裁的控制目标，以及CBF约束参数。Body层的EKF始终独立运行，向上提供状态估计；只有在安全约束被激活时，Spine才干预Body的控制权。这种”正常时自主、异常时仲裁”的接口设计，使得Body层在绝大多数时间内不受上层延迟的影响。

工具选型的理论依据

第8章讨论的四类核心工具——STL、CBF、HTN、EKF——不是因为它们”流行”或”好用”而被选择，而是因为它们分别对应了四类结构性约束的形式化需求，并且这种对应关系是理论上可以严格说明的。

STL（信号时序逻辑） 对应验证可判定性约束。系统行为是否满足时域规约，必须能在有限时间内给出量化判定。STL鲁棒度 $\rho$ 将这一判定的”余量”数值化——$\rho > 0$ 意味着规约被满足且有余量，$\rho < 0$ 意味着违反，$|\rho|$ 提供了距离边界的定量度量。这是其他逻辑系统（如LTL、CTL）所不具备的实时量化特性。

CBF（控制屏障函数） 对应执行安全约束。对安全集 $\mathcal{S} = \{x : h(x) \geq 0\}$ 的前向不变性要求，在数学上等价于在 $\mathrm{SE}(3)$ 测地距离下维持安全间距约束——这正是第4章建立的李群几何所要描述的对象。CBF将连续时间轨迹上的安全条件转化为逐时刻可验证的不等式约束，与QP优化框架的结合使其可实时求解。

HTN（分层任务网络） 对应语义完备性约束的规划侧。当Brain层将自然语言任务分解为可执行的子任务序列时，需要保证分解的完备性（不遗漏）和可达性（每个子任务都有可行的实现方法）。HTN的方法库（method library）结构，为规范闭合域中的词汇覆盖提供了规划层面的镜像：词汇集 $\mathcal{V}^L_{167}$ 中的每个操作类型，都对应HTN方法库中至少一个可执行的方法原语。

EKF（扩展卡尔曼滤波） 对应隐变量流形 $\mathcal{M}_{\mathrm{lat}}$ 上的状态估计问题。在架空线场景中，IMU高频（1000Hz）、激光雷达中频（10Hz）、视觉低频（1-5Hz）的多传感器融合，加上PINN物理先验辅助，使得EKF在强电磁干扰下仍能维持可接受的状态估计精度——这是Body层向Spine层提供可靠安全判定输入的基础。

双流V模型：开发与验证并行

第9章引入的ESTL任务语言，解决了一个在实践中极易被忽视的工程问题：如何保证从自然语言任务描述到STL规约的转换，本身是正确的？

如果这个转换步骤出错，则Spine层所监控的规约与Brain层所理解的任务之间存在语义Gap——系统在Spine层”通过了验证”，却在Brain层的原始意图层面已经偏离。这种错误难以被发现，因为它发生在两个形式化工具的边界处，两侧各自的验证都是正确的。

双流V模型的解决思路是：将自然语言 → HTN计划 → ESTL规约 → STL的转换链，与其对应的测试规约并行运行——每一层的正向转换，都有一条从下至上的验证链反向追溯到原始任务意图。这使得”语言理解正确”与”安全验证通过”成为两个独立可检验的条件，而非一个不透明的整体。

形式证据链：可追溯性的工程实现

第10章的形式证据链设计，是第三部分的收束。它解决的问题是：在一个由多个形式化工具（STL监控器、CBF控制器、HTN规划器、EKF估计器）组成的复杂系统中，每一次具体的任务执行，其安全性是由哪些具体的判定结果支撑的？这些判定结果如何可追溯、可重现、可在事后审计？

形式证据包（Formal Evidence Package）将每次执行的关键判定节点——STL规约的实时鲁棒度值、CBF约束的激活历史、EKF状态估计的置信区间、HTN分解的完备性签名——结构化存储为可审计的记录。这不仅是工程可靠性的需要，也是安全关键系统在监管合规层面的基本要求。

形式证据链的完整性，为第四部分的验证提供了”可观测的输入”：三段验证链（V-SEM–V-SAF）的每一段，都将基于形式证据包中的具体数据得出可重现的结论。

本部分对应 LaTeX 文档的 Part III（第7–10章）。第10章完成系统架构的闭环描述后，第四部分将在同一架构上展开三段核心理论贡献的形式化证明。