Abstract
Symmetry reduction in model checking is a technique for reducing state spaces by exploiting the inherent symmetry of models, i.e., the interchangeability of their subcomponents. Model abstraction, which abstracts away the details of models, often strengthens the symmetry of the models. Graph rewriting systems allow us to express models in such a way that inherent symmetry manifests itself with graph isomorphism of states. In graph rewriting, the synergistic effect of symmetry reduction and model abstraction is obtained under graph isomorphism. This paper proposes a method for abstracting programs described in a hierarchical graph rewriting language LMNtal. The method automatically finds and abstracts away subgraphs of a graph rewriting system that are irrelevant to the results of model checking. The whole framework is developed within the syntax and the formal semantics of the modeling language LMNtal without introducing new domains or languages. We show that the proposed abstraction method combined with symmetry reduction reduces state spaces while preserving the soundness of model checking. We implemented the method on SLIM, an implementation of LMNtal with an LTL model checker, tested it with various concurrent algorithms, and confirmed that it automatically reduces the number of states by successfully extracting the symmetry of models.
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.
LMNtal homepage: https://www.ueda.info.waseda.ac.jp/lmntal/.
- 2.
Available at https://github.com/lmntal/slim.
- 3.
The details of this correspondence are beyond the scope of the present paper and not described here.
References
Backes, P., Reineke, J.: Analysis of infinite-state graph transformation systems by cluster abstraction. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 135–152. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46081-8_8
Ben-Ari, M.: Principles of Concurrent and Distributed Programming. Addison-Wesley, Boston (2006)
Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1), 77–104 (1996)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
Donaldson, A.F., Miller, A.: A computational group theoretic symmetry reduction package for the Spin model checker. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 374–380. Springer, Heidelberg (2006). https://doi.org/10.1007/11784180_29
Emerson, E.A., Havlicek, J.W., Trefler, R.J.: Virtual symmetry reduction. In: Proceedings o LICS 2000, pp. 121–131. IEEE Computer Society (2000)
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Form. Methods Syst. Des. 9(1–2), 105–131 (1996)
Feret, J.: An algebraic approach for inferring and using symmetries in rule-based models. Electron. Notes Theor. Comput. Sci. 316, 45–65 (2015)
Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and analysis using GROOVE. STTT 14(1), 15–40 (2012)
Gocho, M., Hori, T., Ueda, K.: Evolution of the LMNtal runtime to a parallel model checker. Comput. Softw. 28(4), 4\_137–4\_157 (2011)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Boston (2003)
Jensen, K.: Condensed state spaces for symmetrical coloured Petri Nets. Form. Methods Syst. Des. 9(1–2), 7–40 (1996)
Junttila, T.: On the symmetry reduction method for Petri Nets and similar formalisms. Ph.D. thesis, Helsinki University of Technology (2003)
Miller, A., Donaldson, A.F., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. 38(3), 8 (2006)
Milner, R.: The Space and Motion of Communicating Agents. Cambridge University Press, Cambridge (2009)
Norris, I.P.C., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1), 41–75 (1996)
Rensink, A.: Isomorphism checking in GROOVE. Electron. Commun. EASST 1 (2006). https://doi.org/10.14279/tuj.eceasst.1.77
Rensink, A., Distefano, D.: Abstract graph transformation. Electron. Notes Theor. Comput. Sci. 157(1), 39–59 (2006)
Rozenberg, G.: Handbook of Graph Grammars and Computing by Graph Transformation. World Scientific, Singapore (1997)
Schmidt, K.: Integrating low level symmetries into reachability analysis. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 315–330. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46419-0_22
Sistla, A.P., Godefroid, P.: Symmetry and reduced symmetry in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 91–103. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_9
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)
Ueda, K.: Encoding distributed process calculi into LMNtal. Electron. Notes Theor. Comput. Sci. 209, 187–200 (2008)
Ueda, K.: Encoding the pure lambda calculus into hierarchical graph rewriting. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 392–408. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70590-1_27
Ueda, K.: LMNtal as a hierarchical logic programming language. Theor. Comput. Sci. 410(46), 4784–4800 (2009)
Acknowledgments
The authors would like to thank anonymous reviewers for their useful comments. This work was partially supported by Grant-in-Aid for Scientific Research (B) JP18H03223, JSPS, Japan.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Tomioka, T., Tsunekawa, Y., Ueda, K. (2019). Introducing Symmetry to Graph Rewriting Systems with Process Abstraction. In: Guerra, E., Orejas, F. (eds) Graph Transformation. ICGT 2019. Lecture Notes in Computer Science(), vol 11629. Springer, Cham. https://doi.org/10.1007/978-3-030-23611-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-23611-3_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-23610-6
Online ISBN: 978-3-030-23611-3
eBook Packages: Computer ScienceComputer Science (R0)