Exact and Approximate Strategies for Symmetry Reduction in Model Checking
Exact and Approximate Strategies for Symmetry Reduction in Model Checking
复制标题
模型检查中对称性约简的精确和近似策略
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Alice Miller
中科院分区：
文献类型：
--
作者：
Alastair F. Donaldson;Alice Miller
对称性约简技术可以帮助解决模型检验的状态空间爆炸问题，但受到搜索过程中确定状态等价性的困难问题的限制。因此，现有的对称性约简软件包只能利用系统组件之间的完全对称性，因为在这种特殊情况下，检查状态的等效性是简单的。我们提出了一个框架的对称性减少与任意组的结构对称性。通过推广现有的技术，有效地利用对称性，并引入一个近似的策略，用于快速，准确的策略是不可用的群体，我们的方法允许显着的状态空间减少最小的时间开销。我们展示了如何计算群论技术可以用来分析对称群的结构，以便可以选择一个适当的对称性约简策略，我们描述了一个对称性约简包的SPIN模型检查器的接口与计算代数系统GAP。各种Promela模型上的实验结果说明了我们的方法的有效性。
Symmetry reduction techniques can help to combat the state space explosion problem for model checking, but are restricted by the hard problem of determining equivalence of states during search. Consequently, existing symmetry reduction packages can only exploit full symmetry between system components, as checking the equivalence of states is straightforward in this special case. We present a framework for symmetry reduction with an arbitrary group of structural symmetries. By generalising existing techniques for efficiently exploiting symmetry, and introducing an approximate strategy for use with groups for which fast, exact strategies are not available, our approach allows for significant state-space reduction with minimal time overhead. We show how computational group theoretic techniques can be used to analyse the structure of a symmetry group so that an appropriate symmetry reduction strategy can be chosen, and we describe a symmetry reduction package for the SPIN model checker which interfaces with the computational algebra system GAP. Experimental results on a variety of Promela models illustrate the effectiveness of our methods.