On combining symmetry reduction and symbolic representation for efficient model checking

Abstract

BDDs allow succinct symbolic representation of digital circuits. Symmetry reduction factors out redundancy inherent in the regular organization of many systems. Both are successful techniques for combating state space explosion. It would be desirable to combine them into symbolic symmetry reduction. Unfortunately, the straight-forward approach to symmetry reduction requires the orbit relation, whose symbolic representation as a BDD is in general of exponential size. We investigate the use of generic representatives as a means of overcoming this problem for fully symmetric systems: instead of first representing the system as a BDD and then applying symmetry reduction, we translate the given program text into a symmetry-reduced version. The result can then be encoded using a BDD. We demonstrate that this method is superior not only to the traditional orbit-relation based symmetry reduction, but also to the approach using multiple representatives. © Springer-Verlag Berlin Heidelberg 2003.