Advertisement

Identification and Counter Abstraction for Full Virtual Symmetry

  • Ou Wei
  • Arie Gurfinkel
  • Marsha Chechik
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

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.

References

  1. 1.
    Aloul, F., Ramani, A., Markov, I., Sakallah, K.: PBS: A Backtrack Search Pseudo-Boolean Solver. In: SAT 2002, pp. 346–353 (2002)Google Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting Symmetry in Temporal Logic Model Checking. FMSD 9(1-2), 77–104 (1996)Google Scholar
  8. 8.
    Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM TOPLAS 2(19), 253–291 (1997)CrossRefGoogle Scholar
  9. 9.
    Emerson, E., Havlicek, J., Trefler, R.: Virtual Symmetry Reduction. In: LICS 2000, pp. 121–131 (2000)Google Scholar
  10. 10.
    Emerson, E., Sistla, A.: Symmetry and Model Checking. FMSD 9(1-2), 105–131 (1996)Google Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Ip, C., Dill, D.: Better Verification Through Symmetry. FMSD 9(1-2), 41–75 (1996)Google Scholar
  14. 14.
    Papadimitriou, C.: On the Complexity of Integer Programming. J. ACM 28(4), 765–768 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    Pugh, W.: The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis. Comm. of the ACM (August 1992)Google Scholar
  17. 17.
    Wolper, P., Boigelot, B.: An Automata-Theoretic Approach to Presburger Arithmetic Constraints. In: SAS 1995. LNCS, vol. 1785, pp. 21–32 (1995)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Ou Wei
    • 1
  • Arie Gurfinkel
    • 1
  • Marsha Chechik
    • 1
  1. 1.Department of Computer ScienceUniversity of Toronto 

Personalised recommendations