技术摘要：用于验证 CNC 程序物理碰撞的分离逻辑

1. 问题陈述

传统的计算机数控（CNC）加工安全验证严重依赖几何仿真和扫掠体积分析。虽然这些方法在识别明显的 G 代码错误方面行之有效，但它们存在根本性的局限：

• 缺乏符号证明：它们提供的是概率性置信度，而非确定性的、符号化的安全证明。
• 计算成本：它们需要重复的测试周期，特别是在规范或 G 代码发生变化时。
• 不确定性处理：它们难以在不导致计算成本过高的情况下，严格处理连续运动学变量、非确定性的快速定位路径以及机械变异性（例如伺服滞后）。
• 可扩展性：现有方法往往无法高效扩展到复杂的多轴环境（例如 5 轴双转台配置）和协作多刀具系统。

该论文提出，CNC 加工中的物理碰撞可以被重新定义为受管资源模型内的逻辑矛盾，从而为随机仿真提供一种确定性的替代方案。

2. 方法论

所提出的框架引入了一种解析器 - 证明器握手架构，将连续物理运动学与离散形式逻辑解耦。该方法将物理 CNC 工作空间概念化为一个空间堆（Spatial Heap），将物理占用视为一种受管的逻辑资源。

2.1 架构解耦

该系统通过两个领域之间的严格边界运行：

1. 解析器（连续域）：充当一个虚拟机，消耗原始 G 代码、刀具几何形状和安全裕度。它将连续运动学变量（浮点坐标、进给率）和物理不确定性耗尽到离散整数域（$Z^3$）中。它利用闵可夫斯基和（Minkowski sums）将刀具体积按用户定义的安全裕度（$\epsilon$）进行扩展，并采用Bresenham 3D 算法为线性插值（G01）生成离散体素路径，为快速定位（G00）生成边界框。
2. SL 证明器（离散域）：严格在解析器发出的离散空间集上运行。它充当内存管理器，针对**空间堆（$h$）评估分离逻辑（SL）**三元组。证明器不查询变量存储；它仅验证空间不相交性。

2.2 空间堆模型

物理工作空间被映射为一个有限偏函数 $h: Z^3 \rightharpoonup \{Tool, Environment, Stock, Empty\}$。

• 空间数据竞争：物理碰撞被重新定义为“空间数据竞争”，当两个不同的物理资源（例如刀具和环境）试图同时声称拥有同一个离散内存地址时发生。
• 分离合取（$*$）：核心逻辑算子断言子公式在内存的不相交部分上成立。如果 $R(C_1, \theta_1) * R(C_2, \theta_2)$ 被评估，则仅当 $C_1 \cap C_2 = \emptyset$ 时才是可满足的。非空交集使逻辑不可满足，从而确定性地发出故障信号。

2.3 验证流程

验证过程遵循单向流水线：

1. 输入：原始 G 代码、刀具掩膜几何形状、安全裕度（$\epsilon$）和分辨率因子。
2. 离散化：解析器将输入转换为离散空间集（$V_{start}, V_{final}, V_{path}$）。
3. 逻辑推理：证明器评估分离逻辑三元组 $\{ \Sigma_0 \} \text{CSL} \{ \Sigma_{final} \}$。
   • 前置条件（$\Sigma_0$）：断言刀具、环境、毛坯和空空间的初始不相交所有权。
   • 命令（CSL）：将离散运动（例如 G00、G01）表示为堆变异。
   • 后置条件（$\Sigma_{final}$）：断言在刀具位移和材料去除后的更新所有权。

2.4 并发与多轴扩展

• 并发分离逻辑（CSL）：对于多刀具或协作环境，空间堆被划分为线程本地子堆（$h_{local}$）和共享堆（$h_{shared}$）。物理交接通过临界区（with Res do C）作为形式所有权转移进行验证，确保互斥而无需动态锁。
• 多轴运动学：该框架通过将切削刀具和可旋转工件视为两个并发、相互可变的空间线程，扩展到 5 轴操作。解析器预先计算毛坯的旋转扫掠体积（使用旋转矩阵）和刀具的线性扫掠体积，并将两者作为离散集呈现给证明器。这将复杂的三角运动学从证明引擎中抽象出来。

3. 主要贡献

• 碰撞的形式化重定义：该论文建立了物理占用与逻辑内存所有权之间的形式对应关系，将物理碰撞重新定义为逻辑上的“空间数据竞争”。
• 解析器 - 证明器握手：一种新颖的架构边界，将连续不确定性耗尽到离散整数域，使证明器能够在分离逻辑的可处理片段内运行，同时避免了一般指针算术的复杂性。
• 几何安全裕度的集成：该方法集成闵可夫斯基和，直接在离散逻辑中提供形式安全裕度（$\epsilon$），以考虑现实世界的机械不确定性。
• 对高级运动学的可扩展性：该框架原生支持多轴（例如 5 轴）和并发多刀具环境，通过将工件建模为动态可变的空间资源，并利用并发分离逻辑进行共享工作空间验证。

4. 结果与验证

该论文通过以下方式展示了该方法：

• 确定性验证：该系统通过证明分离逻辑三元组的可满足性，成功验证了安全轨迹。
• 碰撞检测：在一个涉及快速进给到夹具的案例研究中，该系统检测到一个“空间数据竞争”（声称的内存的非空交集），并在物理执行之前确定性地转换到故障状态。
• 并发与交接：该框架验证了双刀具在不相交空间中的并行执行以及共享资源的安全顺序交接，证明了分离合取强制实现了互斥。
• 多轴验证：该方法通过将复杂的旋转运动学简化为离散体素集，成功验证了 5 轴操作，证明了刀具和毛坯路径不与环境或彼此相交。

5. 意义与主张

该论文声称，这种方法为传统的几何仿真提供了一种确定性替代方案，提供安全性的符号证明而非概率性置信度。作为仿真的补充，该框架旨在：

• 减少迭代测试：最小化 G 代码或规范变更时所需的测试周期数量。
• 实现自主制造：为自主、少碰撞制造系统提供数学基础。
• 解耦复杂性：将连续运动学的计算负担与逻辑证明分离，使形式验证对于复杂的工业应用变得可处理。

作者将这项工作定位为并非所有仿真的替代品，而是一个严格且可扩展的层，确保在状态转换发生之前满足安全先决条件，这反映了其他领域（如增材制造）中使用的机械化语义。未来的工作 noted 将探索“错误分离逻辑”以隔离遗留错误，并集成到嵌入式控制器中进行实时应用。