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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Bosnacki, D., Dams, D., Holenderski, L.: Symmetric spin. International Journal on Software Tools for Technology Transfer 4(1), 65–80 (2002)
Butler, G.: Fundamental Algorithms for Permutation Groups. LNCS, vol. 559. Springer, Heidelberg (1991)
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)
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)
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)
Donaldson, A.F., Miller, A.: topspin, http://www.dcs.gla.ac.uk/people/personal/ally/topspin/
Emerson, E.A., Havlicek, J., Trefler, R.J.: Virtual symmetry reduction. In: LICS 2000, pp. 121–131. IEEE Computer Society Press, Los Alamitos (2000)
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)
The Gap Group. GAP–Groups, Algorithms, and Programming, Version 4.4 (2006), http://www.gap-system.org
Holzmann, G.J.: The SPIN model checker: primer and reference manual. Addison-Wesley, Reading (2003)
Ip, C., Dill, D.: Better verification through symmetry. Formal Methods in System Design 9, 41–75 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Donaldson, A.F., Miller, A. (2006). A Computational Group Theoretic Symmetry Reduction Package for the Spin Model Checker. In: Johnson, M., Vene, V. (eds) Algebraic Methodology and Software Technology. AMAST 2006. Lecture Notes in Computer Science, vol 4019. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11784180_29
Download citation
DOI: https://doi.org/10.1007/11784180_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35633-2
Online ISBN: 978-3-540-35636-3
eBook Packages: Computer ScienceComputer Science (R0)