局部 μ-演算的对称性归约
计算机科学中的逻辑
2019-03-26 v1
摘要
由于状态爆炸，对大规模进程网络进行模型检验具有挑战性。在许多情况下，单个进程是同构的，但缺乏足够的全局对称性以简化模型检验。本文考虑局部性质的验证，即那些在进程邻域上定义的性质。在显著推广先前关于不变性的结果的基础上，本文证明了所有局部 μ-演算性质，包括安全性与活性性质，均被邻域对称性保持。因此，只需在一组代表性进程邻域上局部地检验它们。一般而言，局部验证是对全局状态空间上验证的近似；然而，若进程交互是外向的，则证明该关系是精确的。对于许多网络拓扑，即便是那些具有很少全局对称性的拓扑，使用代表进行分析也能显著乃至指数级地降低验证代价。此外，本文证明对于由构建模块模式生成的网络族，邻域对称性易于确定，且整个族上的验证可归约为有限组代表性进程邻域上的验证。
引用
@article{arxiv.1903.10405,
title = {Symmetry Reduction for the Local Mu-Calculus},
author = {Kedar S. Namjoshi and Richard J. Trefler},
journal= {arXiv preprint arXiv:1903.10405},
year = {2019}
}
备注
17 pages