Advertisement

A Computational Group Theoretic Symmetry Reduction Package for the Spin Model Checker

  • Alastair F. Donaldson
  • Alice Miller
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4019)

Abstract

Symmetry reduced model checking is hindered by two problems: how to identify state space symmetry when systems are not fully symmetric, and how to determine equivalence of states during search. We present TopSpin, a fully automatic symmetry reduction package for the Spin model checker. TopSpin uses the Gap computational algebra system to effectively detect state space symmetry from the associated Promela specification, and to choose an efficient symmetry reduction strategy by classifying automorphism groups as a disjoint/wreath product of subgroups. We present encouraging experimental results for a variety of Promela examples.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bosnacki, D.: A light-weight algorithm for model checking with symmetry reduction and weak fairness. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 89–103. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. 2.
    Bosnacki, D., Dams, D., Holenderski, L.: Symmetric spin. International Journal on Software Tools for Technology Transfer 4(1), 65–80 (2002)CrossRefGoogle Scholar
  3. 3.
    Butler, G.: Fundamental Algorithms for Permutation Groups. LNCS, vol. 559. Springer, Heidelberg (1991)zbMATHGoogle Scholar
  4. 4.
    Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 147–158. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  5. 5.
    Darga, P.T., Liffiton, M.H., Sakallah, K.A., Markov, I.L.: Exploiting structure in symmetry detection for CNF. In: DAC 2004, pp. 530–534. ACM Press, New York (2004)CrossRefGoogle Scholar
  6. 6.
    Donaldson, A.F., Miller, A.: Automatic symmetry detection for model checking using computational group theory. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 418–496. Springer, Heidelberg (2005)Google Scholar
  7. 7.
    Donaldson, A.F., Miller, A.: topspin, http://www.dcs.gla.ac.uk/people/personal/ally/topspin/
  8. 8.
    Emerson, E.A., Havlicek, J., Trefler, R.J.: Virtual symmetry reduction. In: LICS 2000, pp. 121–131. IEEE Computer Society Press, Los Alamitos (2000)Google Scholar
  9. 9.
    Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 382–396. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  10. 10.
    The Gap Group. GAP–Groups, Algorithms, and Programming, Version 4.4 (2006), http://www.gap-system.org
  11. 11.
    Holzmann, G.J.: The SPIN model checker: primer and reference manual. Addison-Wesley, Reading (2003)Google Scholar
  12. 12.
    Ip, C., Dill, D.: Better verification through symmetry. Formal Methods in System Design 9, 41–75 (1996)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Alastair F. Donaldson
    • 1
  • Alice Miller
    • 1
  1. 1.Department of Computing ScienceUniversity of GlasgowGlasgowScotland

Personalised recommendations