From asymmetry to full symmetry: New techniques for symmetry reduction in model checking

Abstract

It is often the case that systems are “nearly symmetric”; they exhibit symmetry in a part of their description but are, nevertheless, globally asymmetric. We formalize several notions of near symmetry and show how to obtain the benefits of symmetry reduction when applied to asymmetric systems which are nearly symmetric. We show that for some nearly symmetric systems it is possible to perform symmetry reduction and obtain a bisimilar (up to permutation) symmetry reduced system. Using a more general notion of “sub-symmetry” we show how to generate a reduced structure that is simulated (up to permutation) by the original asymmetric program. In the symbolic model checking paradigm, representing the symmetry reduced quotient structure entails representing the BDD for the orbit relation. Unfortunately, for many important symmetry groups, including the full symmetry group, this BDD is provably always intractably large, of size exponential in the number of bits in the state space. In contrast, under the assumption of full symmetry, we show that it is possible to reduce a textual program description of a symmetric system to a textual program description of the symmetry reduced system. This obviates the need for building the BDD representation of the orbit relation on the program states under the symmetry group. We establish that the BDD representing the reduced program is provably small, essentially polynomial in the number of bits in the state space of the original program.