On the constructive orbit problem.(English)Zbl 1205.68220

Summary: Symmetry reduction techniques aim to combat the state-space explosion problem for model checking by restricting search to representative states from equivalence classes with respect to a group of symmetries. The standard approach to representative computation involves converting a state to its minimal image under a permutation group $$G$$, before storing the state. This is known as the Constructive Orbit Problem (COP), and is $$NP$$ hard. It may be possible to solve the COP efficiently if $$G$$ is known to have certain structural properties: in particular if $$G$$ is isomorphic to a full symmetry group, or $$G$$ is a disjoint/wreath product of subgroups. We extend existing results on solving the COP efficiently for fully symmetric groups, and investigate the problem of automatically classifying an arbitrary permutation group as a disjoint/wreath product of subgroups. We also present an approximate COP strategy based on local search, and some computational group-theoretic optimisations to improve the basic approach of solving the COP by symmetry group enumeration. Experimental results using the TopSpin symmetry reduction package, which interfaces with the computational group-theoretic system Gap, illustrate the effectiveness of our techniques.

MSC:

 68Q60 Specification and verification (program logics, model checking, etc.) 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) 68U07 Computer science aspects of computer-aided design 20B25 Finite automorphism groups of algebraic, geometric, or combinatorial structures 20E22 Extensions, wreath products, and other compositions of groups

Software:

Spin-to-Grape; SPIN; TopSpin; GAP; SymmSpin
Full Text:

References:

 [1] Alur, R., Henzinger, T.A.: Reactive modules. Form. Methods Syst. Des. 15(1), 7–48 (1999) [2] Bosnacki, D., Dams, D., Holenderski, L.: Symmetric spin. Softw. Tools Technol. Trans. 4(1), 92–106 (2002) · Zbl 02178179 [3] Butler, G.: Fundamental algorithms for permutation groups. In: Lecture Notes in Computer Science, vol. 559. Springer, New York (1991) · Zbl 0785.20001 [4] Calder, M., Miller, A.: Generalising feature interactions in email. In: Amyot, D., Logrippo, L. (eds.) Feature Interactions in Telecommunications and Software Systems VII, 11–13 June 2003, Ottawa, Canada, pp. 187–204. IOS, Amsterdam (2003) [5] Cameron, P.: Permutation Groups. Cambridge University Press, Cambridge (1999) · Zbl 0922.20003 [6] Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) Computer Aided Verification, 10th International Conference, CAV ’98, Vancouver, BC, Canada, 28 June–2 July 1998, Proceedings. Lecture Notes in Computer Science, vol. 1427, pp. 147–158. Springer, New York (1998) [7] Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1/2), 77–104 (1996) · Zbl 05475431 [8] Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT, Cambridge (1999) [9] Darga, P.T., Liffiton, M.H., Sakallah, K.A., Markov, I.L.: Exploiting structure in symmetry detection for CNF. In: Malik, S., Fix, L., Kahng, A.B. (eds.) Proceedings of the 41th Design Automation Conference, DAC 2004, San Diego, CA, USA, 7–11 June 2004, pp. 530–534. ACM, New York (2004) [10] Donaldson, A.F.: Automatic techniques for detecting and exploiting symmetry in model checking. Ph.D. thesis, Department of Computing Science, University of Glasgow (2007) [11] Donaldson, A.F., Miller, A.: Automatic symmetry detection for model checking using computational group theory. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, 18–22 July 2005, Proceedings. Lecture Notes in Computer Science, vol. 3582, pp. 481–496. Springer, New York (2005) · Zbl 1120.68414 [12] Donaldson, A.F., Miller, A.: A computational group theoretic symmetry reduction package for the SPIN model checker. In: Johnson, M., Vene, V. (eds.) Algebraic Methodology and Software Technology, 11th International Conference, AMAST 2006, Kuressaare, Estonia, 5–8 July 2006, Proceedings. Lecture Notes in Computer Science, vol. 4019, pp. 374–380. Springer, New York (2006) [13] Donaldson, A.F., Miller, A.: Exact and approximate strategies for symmetry reduction in model checking. In: Misra, J., Nipkow, T. (eds.) FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, 21–27 August 2006, Proceedings. Lecture Notes in Computer Science, vol. 4085, pp. 541–556. Springer, New York (2006) [14] Donaldson, A.F., Miller, A.: Extending symmetry reduction techniques to a realistic model of computation. Electr. Notes Theor. Comput. Sci. 185, 63–76 (2007) [15] Donaldson, A.F., Miller, A., Calder, M.: SPIN-to-GRAPE: a tool for analysing symmetry in Promela models. Electr. Notes Theor. Comput. Sci. 139(1), 3–23 (2005) [16] Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Form. Methods Syst. Des. 9(1/2), 105–131 (1996) · Zbl 05475432 [17] Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, 4–8 April 2005, Proceedings. Lecture Notes in Computer Science, vol. 3440, pp. 382–396. Springer, New York (2005) · Zbl 1087.68587 [18] The GAP Group: GAP–groups, algorithms, and programming, version 4.4. http://www.gap-system.org/ (2006) [19] Gent, I.P., Harvey, W., Kelsey, T.: Groups and constraints: symmetry breaking during search. In: Hentenryck, P.V. (ed.) Principles and Practice of Constraint Programming - CP 2002, 8th International Conference, CP 2002, Ithaca, NY, USA, 9–13 September 2002, Proceedings. Lecture Notes in Computer Science, vol. 2470, pp. 415–430. Springer, New York (2002) [20] Goldberg, K., Newman, M., Haynsworth, E.: Combinatorial analysis. In: Abramowitz, M., Stegun, I. (eds.) Handbook of Mathematical Functions: With Formulas, Graphs and Mathematical Tables. Dover, New York (1972) [21] Herstein, I.: Topics in Algebra. Wiley, New York (1975) · Zbl 1230.00004 [22] Holt, D.F., Eick, B., O’Brien, E.A.: Handbook of Computational Group Theory. Chapman & Hall/CRC, London (2005) · Zbl 1091.20001 [23] Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison Wesley, Reading (2004) [24] Ip, C.N., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1/2), 41–75 (1996) · Zbl 05475430 [25] Jefferson, C., Kelsey, T., Linton, S., Petrie, K.: GAPLex: generalized static symmetry breaking. In: Benhamou, F., Jussien, N., O’Sullivan, B. (eds.) Trends in Constraint Programming, chap. 9, pp. 191–205. ISTE, Eugene (2007) [26] Jha, S.: Symmetry and induction in model checking. Ph.D. thesis, School of Computer Science, Carnegie Mellon University (1996) [27] Kirkpatrick, K., Gelatt, C., Vecchi, M.: Optimization by simulated annealing. Science 220, 671–680 (1983) · Zbl 1225.90162 [28] Kovács, L.G.: Wreath decompositions of finite permutation groups. Bull. Aust. Math. Soc. 40(2), 255–279 (1989) · Zbl 0679.20003 [29] Kwiatkowska, M.Z., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, 17–20 August 2006, Proceedings. Lecture Notes in Computer Science, vol. 4144, pp. 234–248. Springer, New York (2006) · Zbl 1188.68194 [30] Linton, S.: Finding the smallest image of a set. In: Gutierrez, J. (ed.) Symbolic and Algebraic Computation, International Symposium ISSAC 2004, Santander, Spain, 4–7 July 2004, Proceedings, pp. 229–234. ACM, New York (2004) · Zbl 1134.05302 [31] McMillan, K.: Symbolic Model Checking. Kluwer, Deventer (1993) · Zbl 0784.68004 [32] Meldrum, J.D.P.: Wreath products of groups and semigroups. In: Pitman Monographs and Surveys in Pure and Applied Mathematics, vol. 74. Longman, New York (1995) · Zbl 0833.20001 [33] Miller, A., Donaldson, A.F., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3) (2006), Article 8 [34] Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981) · Zbl 0474.68031 [35] Rose, J.S.: A Course in Group Theory. Dover, New York (1994) · Zbl 0818.11001 [36] Russel, S., Norvig, P.: Artificial Intelligence, A Modern Approach. Prentice Hall, Englewood Cliffs (1995) · Zbl 0835.68093 [37] 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.