符号奇偶博弈的生成与求解

我们提出了一种基于符号奇偶博弈的新工具，用于验证进程规范的模态$\mu$演算公式。该工具增强了一种现有方法，即先将问题编码为参数化布尔方程组 (PBES)，然后将 PBES 实例化为奇偶博弈。我们改进了从规范到 PBES 的转换过程，以在 PBES 中保留规范的结构；扩展了 LTSmin 以将 PBES 实例化为符号奇偶博弈；并针对符号奇偶博弈实现了 Zielonka 的递归奇偶博弈求解算法。我们使用多值决策图 (MDDs) 来表示集合和关系，从而使工具能够处理非常大的系统。转移关系根据规范的结构进行划分，从而实现了对 MDDs 的高效操作。我们在模块化规范上进行了两项案例研究，结果表明新方法在时间和内存性能上优于现有的基于 PBES 的工具，并且可能比符号模型检查器 NuSMV 更快（尽管内存效率略低）。