Abstract
Symmetry reduction is a well-known approach for alleviating the state explosion problem in model checking. Automatically identifying symmetries in concurrent systems, however, is computationally expensive. We propose a symbolic framework for capturing symmetry patterns in parameterised systems (i.e. an infinite family of finite-state systems): two regular word transducers to represent, respectively, parameterised systems and symmetry patterns. The framework subsumes various types of “symmetry relations” ranging from weaker notions (e.g. simulation preorders) to the strongest notion (i.e. isomorphisms). Our framework enjoys two algorithmic properties: (1) symmetry verification: given a transducer, we can automatically check whether it is a symmetry pattern of a given system, and (2) symmetry synthesis: we can automatically generate a symmetry pattern for a given system in the form of a transducer. Furthermore, our symbolic language allows additional constraints that the symmetry patterns need to satisfy to be easily incorporated in the verification/synthesis. We show how these properties can help identify symmetry patterns in examples like dining philosopher protocols, self-stabilising protocols, and prioritised resource-allocator protocol. In some cases (e.g. Gries’s coffee can problem), our technique automatically synthesises a safety-preserving finite approximant, which can then be verified for safety solely using a finite-state model checker.
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
Similar content being viewed by others
Notes
- 1.
- 2.
Note that all occurrences of \(\#\) are in the end of words.
- 3.
Note that this is for the special case of homomorphisms. Simulation counterexamples are more complicated than case 3 when considering simulations relations that are not total functions.
References
Abdulla, P.A.: Regular model checking. STTT 14(2), 109–118 (2012)
Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158–174. Springer, Heidelberg (2010)
Abdulla, P.A., Jonsson, B., Nilsson, M., d’Orso, J., Saksena, M.: Regular model checking for LTL(MSO). STTT 14(2), 223–241 (2012)
Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35–48. Springer, Heidelberg (2004)
Arenas, M., Barceló, P., Libkin, L.: Regular languages of nested words: fixed points, automata, and synchronization. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 888–900. Springer, Heidelberg (2007)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. JSAT 7(2–3), 56–59 (2010)
Blumensath, A.: Automatic structures. Master’s thesis, RWTH Aachen (1999)
Blumensath, A., Grädel, E.: Finite presentations of infinite structures: Automata and interpretations. Theor. Comput. Syst. 37(6), 641–674 (2004)
Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy - January 23–25, 2013, pp. 457–468 (2013)
Cameron, P.J.: Permutation Groups. London Mathematical Society Student Texts. Cambridge University Press, Cambridge (1999)
Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9(1/2), 77–104 (1996)
Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Proceedings 1991 IEEE International Conference on Computer Design: VLSI in Computer and Processors, ICCD 1992, Cambridge, MA, USA, October 11–14, 1992, pp. 522–525 (1992)
Donaldson, A.F.: Automatic Techniques for Detecting and Exploiting Symmetry in Model Checking. Ph.D. thesis, University of Glasgow (2007)
Donaldson, A.F., Miller, A.: Automatic symmetry detection for model checking using computational group theory. In: FM, pp. 631–631 (2005)
Donaldson, A.F., Miller, A.: Automatic symmetry detection for promela. J. Autom. Reasoning 41, 251–293 (2008)
Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: Proceedings of the 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17–20, 2000, Automated Deduction - CADE-17, pp. 236–254 (2000)
Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL, 85–94, (1995)
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods Syst. Des. 9(1/2), 105–131 (1996)
Gries, D.: The Science of Programming. Springer-Verlag (1981)
Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63–67 (1990)
Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods Syst. Des. 9, 41–75 (1996)
Israeli, A., Jalfon, M.: Token management schemes and random walks yield self-stabilizing mutual exclusion. In: PODC, pp. 119–131 (1990)
Jaghoori, M.M., Sirjani, M., Mousavi, M.R., Khamespanah, E., Movaghar, A.: Symmetry and partial order reduction techniques in model checking rebeca. Acta Inf. 47, 33–66 (2010)
Jaghoori, M.M., Sirjani, M., Mousavi, M.R.R., Movaghar, A.: Efficient symmetry reduction for an actor-based model. In: Chakraborty, G. (ed.) ICDCIT 2005. LNCS, vol. 3816, pp. 494–507. Springer, Heidelberg (2005)
Lehmann, D., Rabin, M.: On the advantage of free choice: A symmetric and fully distributed solution to the dining philosophers problem (extended abstract). In: Proceedings 8th Annual ACM Symposium on Principles of Programming Languages (POPL 1981), pp. 133–138 (1981)
Lin, A.W.: Accelerating tree-automatic relations. In: FSTTCS, pp. 313–324 (2012)
Lin, A.W., Nguyen, T.K., Rümmer, P., Sun, J.: Regular symmetry patterns (technical report). http://arxiv.org/abs/1510.08506 (cited in 2015)
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. Method. 9, 133–166 (2000)
Spermann, C., Leuschel, M.: ProB gets nauty: effective symmetry reduction for B and Z models. In: TASE, pp. 15–22 (2008)
Vojnar, T.: Cut-offs and automata in formal verification of infinite-state systems: Habilitation Thesis. Brno University of Technology, Faculty of Information Technology (2007)
Wahl, T., Donaldson, A.F.: Replication and abstraction: Symmetry in automated formal verification. Symmetry 2, 799–847 (2010)
Zhang, S.J., Sun, J., Sun, C., Liu, Y., Ma, J., Dong, J.S.: Constraint-based automatic symmetry detection. In: ASE, pp. 15–25 (2013)
Acknowledgment
Lin is supported by Yale-NUS Grants, Rümmer by the Swedish Research Council. We thank Marty Weissman for a fruitful discussion.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lin, A.W., Nguyen, T.K., Rümmer, P., Sun, J. (2016). Regular Symmetry Patterns. In: Jobstmann, B., Leino, K. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2016. Lecture Notes in Computer Science(), vol 9583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49122-5_22
Download citation
DOI: https://doi.org/10.1007/978-3-662-49122-5_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-49121-8
Online ISBN: 978-3-662-49122-5
eBook Packages: Computer ScienceComputer Science (R0)