Symmetry Reduced Model Checking for B
Symmetry Reduced Model Checking for B
复制标题
B 的对称性简化模型检查
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
M. Butler
中科院分区：
文献类型：
--
作者：
E. Turner;M. Leuschel;Corinna Spermann;M. Butler
对称性约简是一种可以帮助缓解模型检测中状态空间爆炸问题的技术。这个想法是只验证来自每一类(轨道)对称状态的状态子集。本文提出了一种B机对称约简模型检验的框架，该框架从每个轨道验证一个唯一的代表。对称是由延迟集诱导的；延迟集是B语言的关键组成部分。这与需要在语言中引入特殊数据类型以表示对称性的策略不同。图同构程序的扩展版本NAUTY被用来检测对称性，对称性约简包已经被集成到PROB模型检查器中。给出了相关的算法，实验结果表明该方法是有效的，有时可以实现指数加速。
Symmetry reduction is a technique that can help alleviate the problem of state space explosion in model checking. The idea is to verify only a subset of states from each class (orbit) of symmetric states. This paper presents a framework for symmetry reduced model checking of B machines, which verifies a unique representative from each orbit. Symmetries are induced by the deferred set; a key component of the B language. This contrasts with strategies that require the introduction of a special data type into a language, to indicate symmetry. An extended version of the graph isomorphism program, nauty, is used to detect symmetries, and the symmetry reduction package has been integrated into the PROB model checker. Relevant algorithms are presented, and experimental results illustrate the effectiveness of the method, where exponential speedups are sometimes possible.