Efficient Reduction Techniques for Systems with Many Components

We present an improved approach to verifying systems involving many copies of a few kinds of components. Replication of this type occurs frequently in practice and is regarded a major source of state explosion during temporal logic model checking. Our solution makes use of symmetry reduction through counter abstraction. The efficiency of this approach directly depends on the size of the components' local state space, which is exponential in the number of local variables. We show how program analysis can significantly reduce the local state space and can help towards a succinct BDD representation of the system. Our reduction techniques synergistically combine into efficient symbolic verification, as documented by promising experimental results.