图变换系统的验证与多合并三元图语法工具支持

# 图变换系统的验证与多合并三元图语法工具支持 ## 1. 归纳不变检查结果分析 ### 1.1 验证问题复杂度与算法结果 通过一系列案例对验证问题的复杂度和算法结果进行了评估，部分结果如下表所示： | Example | Check | Complexity time (s) | result | time (s) | result | time (s) | result | time (s) | result | time (s) | result | | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | | MT - Simple - Semantics subproblem | 4 | 20 | true | <1 | true | <1 | true | <1 | true | <1 | true | | MT - Complex - TGG subproblem | 4 | <1 | true | <1 | true | <1 | true | <1 | true | <1 | true | | Car Platooning subproblem | 258 | <1 | true | <1 | true | <1 | true | <1 | true | <1 | true | | MT - Simple - TGG subproblem | 2778 | 220 | true | 1,5 | false negatives | 1 | false negatives | 1,5 | true | 1 | true | 从表中可以看出，不同的案例在验证时间和结果上存在差异。部分子问题验证时间较短且结果为真，而有些则出现了超时、内存不足或假阴性等情况。 ### 1.2 高级蕴含检查的影响 归纳不变检查器在不使用高级蕴含检查时，会对某些子问题产生假阴性结果。而使用带有高级蕴含检查的变体时，这些假阴性结果不会出现。这表明高级蕴含检查在提高准确性方面具有重要作用，对于案例研究具有实际意义。 ### 1.3 部分负应用条件的作用 复杂模型变换案例研究无法通过没有部分负应用条件的归纳不变检查器变体进行验证，这些尝试在经过两天多的计算后仍无结果而被中止。相反，采用部分负应用条件时，最长案例的验证时间为 100 分钟，这在处理更复杂案例时，可扩展性有了显著提高。额外使用高级蕴含检查不仅消除了假阴性，在一个案例中还将验证时间减半，对性能有明显的提升。 ## 2. 相关工具对比 ### 2.1 SeekSat/ProCon 工具 SeekSat/ProCon 工具比当前方法更通用，原则上能够处理案例研究。但该工具的可扩展性有限，因此仍需要针对特定类型问题进行优化的工具，以应对更复杂的案例研究。 ### 2.2 其他自动化方法 其他处理无限状态空间图变换系统的自动化方法，如采用基于形状分析汇总的抽象模型检查方法、采用邻域抽象的模型检查方法、Uncover 工具、Augur 工具和 RAVEN 工具等，都无法用于需要无限制负应用条件的案例研