超越依赖图：项重写系统终止性证明与安全协议知识计算研究

### 超越依赖图：项重写系统终止性证明与安全协议知识计算研究 #### 1. 项重写系统终止性证明 在项重写系统（TRS）的研究中，终止性证明是一个重要的问题。相关研究将之前章节描述的技术集成到终止性证明器 TTT2 中。下面将介绍相关的依赖图处理器及其实验结果。 ##### 1.1 依赖图处理器 - **处理器类型**： - **t**：使用根比较来估计依赖图的简单快速近似方法。若规则 α 的右部和规则 β 的左部根符号相同，则从 α 到 β 添加一条弧。 - **e**：使用 DGe(P, R) 估计的依赖图处理器，是 TTT2 和 AProVE 中的默认处理器。 - **c**：基于 DGc(P, R) 的依赖图处理器。 - **r**：定理 16 中的改进依赖图处理器，对于（非）右线性的 P ∪ R 使用 IDGc(P, R)（DGc(P, R)）。 - **\***：t、e、c 和 r 的组合，后三者每个计算有 500 毫秒的时间限制。 ##### 1.2 实验设置 对 Termination Problem Data Base 5.0 版本中全终止类别下满足变量条件（每个重写规则 l → r 中 Var(r) ⊆ Var(l)）的 1331 个 TRS 进行实验。使用配备 Intel Pentium M 处理器（2 GHz CPU 速率，1 GB 系统内存）的工作站，所有实验时间限制为 60 秒。 ##### 1.3 实验结果 | 处理器 | 无可用规则 - 无多项式 | | | | | 有可用规则 - 无多项式 | | | | | | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | | | t | e | c | r | * | t | e | c | r | * | | 移除弧数 | 55 | 68 | 68 | 72 | 73 | 55 | 67 | 68 | 73 | 74 | | SCC 数量 | 4416 | 4529 | 4218 | 3786 | 4161 | 4416 | 4532 | 4179 | 3680 | 4114 | | 规则数量 | 24404 | 22198 | 20519 | 19369 | 21196 | 24404 | 22233 | 20306 | 19033 | 21093 | | 成功次数 | 25 | 60 | 67 | 176 | 183 | 25 | 58 | 67 | 191 | 195 | | 平均时间（毫秒） | 105 | 190 | 411 | 365 | 211 | 133 | 224 | 491 | 434 | 242 | | 超时次数 | 2 | 2 | 60 | 78 | 2 | 2 | 2 | 60 | 81 | 2 | | 处理器 | 无可用规则 - 有多项式 | | | | | 有可用规则 - 有多项式 | | | | | | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | | | t | e | c | r | * | t | e | c | r | * | | 成功次数 | 454 | 494 | 493 | 528 | 548 | 454 | 491 | 492 | 529 | 548 | |