Abstract
Symmetry reduction is an effective approach for dealing with the state explosion problem: when applicable, it enables exponential statespace reduction. Thus, it is appealing to extend the power of symmetry reduction to systems which are “not quite symmetric”. Emerson et al. identified a class of these, called virtually symmetric [9]. In this paper, we study symmetry from the point of view of abstraction, which allows us to present an efficient procedure for identifying full virtual symmetry. We also explore techniques for combining virtual symmetry with symbolic model-checking and report on experiments that illustrate the feasibility of our approach.
Chapter PDF
Similar content being viewed by others
References
Aloul, F., Ramani, A., Markov, I., Sakallah, K.: PBS: A Backtrack Search Pseudo-Boolean Solver. In: SAT 2002, pp. 346–353 (2002)
Barner, S., Grumberg, O.: Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 93–106. Springer, Heidelberg (2002)
Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons for Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131. Springer, Heidelberg (1982)
Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting Symmetry in Temporal Logic Model Checking. FMSD 9(1-2), 77–104 (1996)
Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM TOPLAS 2(19), 253–291 (1997)
Emerson, E., Havlicek, J., Trefler, R.: Virtual Symmetry Reduction. In: LICS 2000, pp. 121–131 (2000)
Emerson, E., Sistla, A.: Symmetry and Model Checking. FMSD 9(1-2), 105–131 (1996)
Emerson, E., Trefler, R.: From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999)
Emerson, E., Wahl, T.: On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 216–230. Springer, Heidelberg (2003)
Ip, C., Dill, D.: Better Verification Through Symmetry. FMSD 9(1-2), 41–75 (1996)
Papadimitriou, C.: On the Complexity of Integer Programming. J. ACM 28(4), 765–768 (1981)
Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1, ∞)-Counter Abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–122. Springer, Heidelberg (2002)
Pugh, W.: The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis. Comm. of the ACM (August 1992)
Wolper, P., Boigelot, B.: An Automata-Theoretic Approach to Presburger Arithmetic Constraints. In: SAS 1995. LNCS, vol. 1785, pp. 21–32 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wei, O., Gurfinkel, A., Chechik, M. (2005). Identification and Counter Abstraction for Full Virtual Symmetry. In: Borrione, D., Paul, W. (eds) Correct Hardware Design and Verification Methods. CHARME 2005. Lecture Notes in Computer Science, vol 3725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560548_22
Download citation
DOI: https://doi.org/10.1007/11560548_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29105-3
Online ISBN: 978-3-540-32030-2
eBook Packages: Computer ScienceComputer Science (R0)