A Computational Group Theoretic Symmetry Reduction Package for the Spin Model Checker

Abstract. Symmetry reduced model checking is hindered by two problems: how to identify state space symmetry when systems are not fully symmetric, and how to determine equivalence of states during search. We present TopSPIN, a fully automatic symmetry reduction package for the SPIN model checker. TopSPIN uses the GAP computational algebra system to effectively detect state space symmetry from the associated Promela specification, and to choose an efficient symmetry reduction strategy by classifying automorphism groups as a disjoint/wreath product of subgroups. We present encouraging experimental results for a variety of Promela examples.

• Type: Conference
• Year: 2006
• Where: AMAST
• Authors: Alastair F. Donaldson, Alice Miller
• Keywords: AMAST 2006, Software Engineering, State Space Symmetry, Symmetry, Symmetry Reduction