参数化布尔方程系统到奇偶博弈的高效实例化
计算机科学中的逻辑
2012-10-25 v1 计算机科学与博弈论
摘要
参数化布尔方程系统（PBESs）是带有数据变量的布尔不动点方程序列，用于例如验证带有数据的进程代数规范的模态 -演算公式。求解 PBES 通常通过将其实例化为奇偶博弈（Parity Game）然后求解该博弈来完成。现有的实用博弈求解器虽然存在，但实例化步骤是瓶颈所在。我们通过两个步骤改进了实例化过程。首先，我们将 PBES 转换为参数化奇偶博弈（PPG），这是一种每个方程均为合取或析取的 PBES。随后，我们利用 LTSmin 生成博弈图，LTSmin 提供转移缓存、高效的状态存储以及分布式和符号化的状态空间生成功能。为此，我们为 LTSmin 定义了一个语言模块，包含将带参数的变量编码为状态向量、分组转移关系以及指示状态向量部分与转移组之间依赖关系的依赖矩阵。针对一些大型案例研究的基准测试表明，该方法显著加快了实例化速度并大幅降低了内存使用量。
引用
@article{arxiv.1210.6414,
title = {Efficient Instantiation of Parameterised Boolean Equation Systems to Parity Games},
author = {Gijs Kant and Jaco van de Pol},
journal= {arXiv preprint arXiv:1210.6414},
year = {2012}
}
备注
In Proceedings GRAPHITE 2012, arXiv:1210.6118