Extending Symmetry Reduction by Exploiting System Architecture

11 years 6 months ago
Extending Symmetry Reduction by Exploiting System Architecture
Abstract. Symmetry reduction is a technique to alleviate state explosion in model checking by replacing a model of replicated processes with a bisimilar quotient model. The size of the quotient depends strongly on the set of applicable symmetries, which in many practical cases allows only polynomial reduction. We introduce architectural symmetry, a concept that exploits architectural system features to compensate for a lack of symmetry in the system model. We show that the standard symmetry quotient of an architecturally symmetric and well-architected model preserves arbitrary Boolean combinations and nestings of reachability properties. This quotient can be exponentially smaller than the model, even in cases where traditional symmetry reduction is nearly ineffective. Our technique thus extends the benefits of symmetry reduction to systems that are in fact not symmetric. Finally, we generalize our results to all architecturally symmetric models, including those that are not well-arch...
Richard J. Trefler, Thomas Wahl
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Authors Richard J. Trefler, Thomas Wahl
Comments (0)