参数化系统分析中的对称性与完备性及程序的更好下近似方法

### 参数化系统分析中的对称性与完备性及程序的更好下近似方法 #### 1. 简单BDS系统 简单的BDS（Bounded Data System）系统中，所有全局变量类型为T0，局部变量由类型为T1 → T0的数组表示。这种简单情况很重要，例如它能描述图1中的互斥协议以及许多多线程程序，这些程序中线程操作的数据结构与线程数量无关。 对于简单BDS系统，小模型边界非常小： - 单量化断言（∀i : θ(i)）需要2个进程。 - 双量化断言（∀i, j : i < j : θ(i, j)）需要3个进程。 #### 2. 实验情况 该方法已在TLV中实现，在一些示例上取得了成功。初步结果如下表所示： | 程序 | 不变式类型 | 时间(秒) | 边界 | BDD大小θ(1) 或 θ(1, 2) | 最大BDD | | ---- | ---- | ---- | ---- | ---- | ---- | | mutex | 2 - ∀ | 0.01 | 4 | 9 | 1327 | | mutex+ | 1 - ∀ | 0.01 | 3 | 8 | 1007 | | szymanski | 2 - ∀ | 0.03 | 4 | 18 | 9956 | | token - ring | 2 - ∀ | 0.01 | 4 | 177 | 18341 | 实现会生成形状为（∀i : θ(i)）和（∀i, j : i ≠ j : θ(i, j)）的量化归纳断言，分别记为1 - ∀和2 - ∀。分裂不变式计算的完备性，特别是能计算出最强断言这一特性很有用。如果为大小为K的实例计算出的最强分裂不变式θ∗K未通过充分性测试，那么不存在其他θ′使得（∀i : θ′(i)）对所有N都是归纳的。 也可以对偶化理论来计算“最佳”存在不变式，即形式为（∃i : θ(i)）的断言，其中θ是使断言具有归纳性且蕴含正确性属性的最弱公式。 部分较难证明的属性需要通用和存在属性组合的归纳断言。IIV工具使用启发式方法（可能失败）来构建通用和存在断言的布尔组合，但目前不清楚是否存在完整且高效的方法来构建此类混合不变式，当前实现无法自动证明这些属性。还可以用辅助程序变量替换（Skolem化）存在量化，将其转化为纯通用量化，以便使用分裂不变式方法处理，但这需要猜测辅助变量的定义，目前还没有系统的引入此类变量的程序。 #### 3. 相关工作 参数化验证和组合分析有大量相关工作： - **参数化验证**：某些类别的参数化验证问题是可判定的，基于时态属性的小模型定理。通用的参数化验证方法包括过程摘要和基于自动机理论的加速方法等，早期工作未考虑完备性，截断结果以及与归纳不变性的联系是新的贡献。 - **组合推理**：并发的组合推理可追溯到O