Dynamic Symmetry Reduction
Dynamic Symmetry Reduction
复制标题
动态对称性降低
DOI：
10.1007/978-3-540-31980-1_25
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
T. Wahl
中科院分区：
文献类型：
--
作者：
E. Allen Emerson;T. Wahl
对称约简是解决时态逻辑模型检测中状态爆炸问题的一种方法。它的使用与符号表示遭受了禁止大BDD的轨道关系。一个建议的解决方案是预先计算从状态到可能的多个对称等价类的代表的映射。在本文中，我们提出了一个更有效的方法，确定代表动态不动点迭代。我们的方案保持了代表的唯一性。使用轨道关系的另一种替代方法是反抽象。该方法对全对称的特殊情况是有效的，提供了一种有益的程序结构。相比之下，我们的解决方案也适用于不完全对称的系统，以及转换为计数器是不可行的系统。我们支持这些说法与实验结果。
Symmetry reduction is a technique to combat the state explosion problem in temporal logic model checking. Its use with symbolic representation has suffered from the prohibitively large BDD for the orbit relation. One suggested solution is to pre-compute a mapping from states to possibly multiple representatives of symmetry equivalence classes. In this paper, we propose a more efficient method that determines representatives dynamically during fixpoint iterations. Our scheme preserves the uniqueness of representatives. Another alternative to using the orbit relation is counter abstraction. It proved efficient for the special case of full symmetry, provided a conducive program structure. In contrast, our solution applies also to systems with less than full symmetry, and to systems where a translation into counters is not feasible. We support these claims with experimental results.