Symmetry Reduction for B by Permutation Flooding

Symmetry reduction is an established method for limiting the amount of states that have to be checked during exhaustive model checking. The idea is to only verify a single representative of every class of symmetric states. However, computing this representative can be nontrivial, especially for a language such as B with its involved data structures and operations. In this paper, we propose an alternate approach, called permutation flooding. It works by computing permutations of newly encountered states, and adding them to the state space. This turns out to be relatively unproblematic for B’s data structures and we have implemented the algorithm inside the ProB model checker. Empirical results confirm that this approach is effective in practice; speedups exceed an order of magnitude in some cases. The paper also contains correctness results of permutation flooding, which should also be applicable for classical symmetry reduction in B.

• Type: Conference
• Year: 2007
• Where: B
• Authors: Michael Leuschel, Michael J. Butler, Corinna Spermann, Edd Turner
• Keywords: B 2007, Data Structures, Exhaustive Model Checking, Software Engineering, Symmetry Reduction