×

zbMATH — the first resource for mathematics

Vector symmetry reduction. (English) Zbl 1335.68134
Miller, Alice (ed.) et al., Proceedings of the 8th international workshop on automated verification of critical systems (AVoCS 2008), Glasgow, UK, September 30 – October 1, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 250, No. 2, 3-18 (2009).
Summary: Symmetry reduction is an effective state-space reduction technique for model checking, and works by restricting search to equivalence class representatives with respect to a group of symmetries for a model. A major problem with symmetry reduction techniques is the time taken to compute the representative of a state, which can be prohibitive. In efficient implementations of symmetry reduction, a symmetry is applied to a state as a sequence of operations which swap component identities. We show that vector processing technology, common to modern computers, can be used to implement a vectorised swap operation, which can be incorporated into the representative computation algorithm to accelerate symmetry reduction. Via a worked example, we present details of this vector symmetry reduction method. We have implemented our techniques in the TopSpin symmetry reduction package for the Spin model checker, and present experimental results showing the speedups obtained via vectorisation for two case-studies running on a PowerPC vector processor.
For the entire collection see [Zbl 1281.68035].
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
Software:
SPIN; SymmSpin; TopSpin
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bosnacki, D.; Dams, D.; Holenderski, L., Symmetric spin, Sttt, 4, 1, 92-106, (2002)
[2] Calder, M.; Miller, A., Generalising feature interactions in email, (), 187-204
[3] Clarke, E.M.; Emerson, E.A.; Jha, S.; Sistla, A.P., Symmetry reductions in model checking, (), 147-158
[4] Clarke, E.M.; Jha, S.; Enders, R.; Filkorn, T., Exploiting symmetry in temporal logic model checking, Formal methods in system design, 9, 1/2, 77-104, (1996)
[5] Clarke, E.; Grumberg, O.; Peled, D., Model checking, (1999), The MIT Press
[6] Donaldson, A.F.; Miller, A., Automatic symmetry detection for model checking using computational group theory, (), 481-496 · Zbl 1120.68414
[7] Donaldson, A.F.; Miller, A., A computational group theoretic symmetry reduction package for the SPIN model checker, (), 374-380
[8] Donaldson, A.F.; Miller, A., Exact and approximate strategies for symmetry reduction in model checking, (), 541-556
[9] A.F. Donaldson and A. Miller. Extending symmetry reduction techniques to a realistic model of computation. Electr. Notes Theor. Comput. Sci., 2007. To appear · Zbl 1335.68135
[10] Emerson, E.A.; Sistla, A.P., Symmetry and model checking, Formal methods in system design, 9, 1/2, 105-131, (1996)
[11] Emerson, E.A.; Trefler, R.J., From asymmetry to full symmetry: new techniques for symmetry reduction in model checking, (), 142-156 · Zbl 0957.68067
[12] Emerson, E.A.; Wahl, T., On combining symmetry reduction and symbolic representation for efficient model checking, (), 216-230 · Zbl 1179.68082
[13] Emerson, E.A.; Wahl, T., Dynamic symmetry reduction, (), 382-396 · Zbl 1087.68587
[14] Freescale Semiconductor. AltiVec, 2008. http://www.freescale.com/altivec/
[15] Herstein, I., Topics in algebra, (1975), John Wiley & Sons · Zbl 1230.00004
[16] Hofstee, H.P., Power efficient processor architecture and the cell processor, (), 258-262
[17] Holzmann, G.J., The SPIN model checker: primer and reference manual, (2003), Addison-Wesley
[18] Holzmann, G.J.; Bosnacki, D., The design of a multicore extension of the SPIN model checker, IEEE trans. software eng., 33, 10, 659-674, (2007)
[19] Ip, C.N.; Dill, D.L., Better verification through symmetry, Formal methods in system design, 9, 1/2, 41-75, (1996)
[20] Kernighan, B.W.; Ritchie, D., The C programming language, (1988), Prentice Hall
[21] Miller, A.; Donaldson, A.F.; Calder, M., Symmetry in temporal logic model checking, ACM comput. surv., 38, 3, (2006), Article 8
[22] Rangarajan, M.; Dajani-Brown, S.; Schloegel, K.; Cofer, D.D., Analysis of distributed spin applied to industrial-scale models, (), 267-285 · Zbl 1125.68373
[23] Sistla, A.P.; Gyuris, V.; Emerson, E.A., SMC: a symmetry-based model checker for verification of safety and liveness properties, ACM trans. softw. eng. methodol., 9, 2, 133-166, (2000)
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.