Dynamic Symmetry Reduction

9 years 1 months ago
Dynamic Symmetry Reduction
Abstract. 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 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.
E. Allen Emerson, Thomas Wahl
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Authors E. Allen Emerson, Thomas Wahl
Comments (0)