×

zbMATH — the first resource for mathematics

A lazy approach to symmetry reduction. (English) Zbl 1214.68225
Summary: Symmetry reduction is a technique to counter state explosion for systems with regular structure. It relies on idealistic assumptions about indistinguishable components, which in practice may only be similar. In this article, we present a flexible, lazy approach to symmetry-reducing a structure without any prior knowledge about its global symmetry. Instead of a-priori checking for compliance with symmetry conditions, each encountered state is annotated on the fly with information about how symmetry is violated along the path leading to it. The method naturally favors “very symmetric” systems: more similarity among the components leads to greater compression. A notion of subsumption is used to prune the annotated search space during exploration. Previous solutions to the approximate symmetry reduction problem are restricted to specific types of asymmetry, such as up to bisimilarity, or incur a large overhead, either during preprocessing of the structure or during the verification run. In contrast, the strength of our method is its balance between ease of implementation and algorithmic flexibility. We include analytic and experimental results that witness its efficiency.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
CUDD; SPIN; TopSpin; Uppaal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Anand S, Pasareanu C, Visser W (2006) Symbolic execution with abstract subsumption checking. In: Model checking of software (SPIN)
[2] Canfield R (1998) The size of the largest antichain in the partition lattice. J Comb Theory Ser A 83(2): 188–201 · Zbl 0908.05008 · doi:10.1006/jcta.1998.2871
[3] Clarke E, Enders R, Filkorn T, Jha S (1996) Exploiting symmetry in temporal logic model checking. Formal Methods Syst Des (FMSD) 9(1–2): 77–104 · Zbl 05475431 · doi:10.1007/BF00625969
[4] Donaldson A, Miller A (2005) Automatic symmetry detection for model checking using computational group theory. In: Formal methods (FM) · Zbl 1120.68414
[5] Donaldson A, Miller A (2006) Exact and approximate strategies for symmetry reduction in model checking. In: Formal methods (FM) · Zbl 1161.68564
[6] Emerson A, Havlicek J, Trefler R (2000) Virtual symmetry reduction. In: Logic in computer science (LICS)
[7] Emerson A, Sistla P (1996) Symmetry and model checking. Formal Methods Syst Des (FMSD) 9(1–2): 105–131 · Zbl 05475432 · doi:10.1007/BF00625970
[8] Emerson A, Trefler R (1999) From asymmetry to full symmetry: new techniques for symmetry reduction in model checking. In: Correct hardware design and verification methods (CHARME) · Zbl 0957.68067
[9] Emerson A, Wahl T (2003) On combining symmetry reduction and symbolic representation for efficient model checking. In: Correct hardware design and verification methods (CHARME) · Zbl 1179.68082
[10] Hendriks M, Behrmann G, Larsen KG, Niebert P, Vaandrager F (2003) Adding symmetry reduction to Uppaal. In: Formal modelling and analysis of timed systems (FORMATS) · Zbl 1099.68657
[11] Henzinger T, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Principles of programming languages (POPL) · Zbl 1323.68374
[12] Holzmann G (1997) The model checker spin. Trans Softw Eng (TOSE) 23(5): 279–295 · Zbl 05113845 · doi:10.1109/32.588521
[13] Ip N, Dill D (1999) Verifying systems with replicated components in Mur. Formal Methods Syst Des (FMSD) 14(3): 273–310 · doi:10.1023/A:1008723125149
[14] Sistla P, Godefroid P (2004) Symmetry and reduced symmetry in model checking. Trans Program Lang Syst (TOPLAS) 26(4): 702–734 · Zbl 05459337 · doi:10.1145/1011508.1011511
[15] Somenzi F (2001) The CU decision diagram package, release 2.3.1. University of Colorado at Boulder. http://vlsi.colorado.edu/\(\sim\)fabio/CUDD/
[16] Wahl T (2007) Adaptive symmetry reduction. In: Computer-aided verification (CAV) · Zbl 1135.68484
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.