Extending Symmetry Reductionby Exploiting System Architecture

摘要

Symmetry reduction is a technique to alleviate state explo-sion in model checking by replacing a model of replicated processes witha bisimilar quotient model. The size of the quotient depends strongly onthe set of applicable symmetries, which in many practical cases allowsonly polynomial reduction. We introduce architectural symmetry, a con-cept that exploits architectural system features to compensate for a lackof symmetry in the system model. We show that the standard symmetryquotient of an architecturally symmetric and well-architected model pre-serves arbitrary Boolean combinations and nestings of reachability prop-erties. This quotient can be exponentially smaller than the model, evenin cases where traditional symmetry reduction is nearly ineffective. Ourtechnique thus extends the benefits of symmetry reduction to systems thatare in fact not symmetric. Finally, we generalize our results to all architec-turally symmetric models, including those that are not well-architected.We illustrate our method through examples and experimental data.