Advertisement

On the Essence of Parallel Independence for the Double-Pushout and Sesqui-Pushout Approaches

  • Andrea CorradiniEmail author
  • Dominique Duval
  • Michael Löwe
  • Leila Ribeiro
  • Rodrigo MachadoEmail author
  • Andrei Costa
  • Guilherme Grochau Azzi
  • Jonas Santos Bezerra
  • Leonardo Marques Rodrigues
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10800)

Abstract

Parallel independence between transformation steps is a basic notion in the algebraic approaches to graph transformation, which is at the core of some static analysis techniques like Critical Pair Analysis. We propose a new categorical condition of parallel independence and show its equivalence with two other conditions proposed in the literature, for both left-linear and non-left-linear rules. Next we present some preliminary experimental results aimed at comparing the three conditions with respect to computational efficiency. To this aim, we implemented the three conditions, for left-linear rules only, in the Verigraph system, and used them to check parallel independence of pairs of overlapping redexes generated from some sample graph transformation systems over categories of typed graphs.

References

  1. 1.
    Bezerra, J.S., Costa, A., Azzi, G., Rodrigues, L.M., Machado, R., Ribeiro, L.: Verites/verigraph: parallel independence benchmarks, June 2017.  https://doi.org/10.5281/zenodo.814246
  2. 2.
    Bezerra, J.S., Costa, A., Ribeiro, L., Cota, É.F.: Formal verification of health assessment tools: a case study. Electr. Notes Theor. Comput. Sci. 324, 31–50 (2016).  https://doi.org/10.1016/j.entcs.2016.09.005 CrossRefGoogle Scholar
  3. 3.
    Born, K., Lambers, L., Strüber, D., Taentzer, G.: Granularity of conflicts and dependencies in graph transformation systems. In: de Lara, J., Plump, D. (eds.) ICGT 2017. LNCS, vol. 10373, pp. 125–141. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-61470-0_8 CrossRefGoogle Scholar
  4. 4.
    Corradini, A.: On the definition of parallel independence in the algebraic approaches to graph transformation. In: Milazzo, P., Varró, D., Wimmer, M. (eds.) STAF 2016. LNCS, vol. 9946, pp. 101–111. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-50230-4_8 CrossRefGoogle Scholar
  5. 5.
    Corradini, A., Duval, D., Prost, F., Ribeiro, L.: Parallelism in AGREE transformations. In: Echahed, R., Minas, M. (eds.) ICGT 2016. LNCS, vol. 9761, pp. 37–53. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-40530-8_3 CrossRefGoogle Scholar
  6. 6.
    Corradini, A., Gadducci, F.: On term graphs as an adhesive category. Electr. Notes Theor. Comput. Sci. 127(5), 43–56 (2005).  https://doi.org/10.1016/j.entcs.2005.02.014 CrossRefzbMATHGoogle Scholar
  7. 7.
    Corradini, A., Heindel, T., Hermann, F., König, B.: Sesqui-pushout rewriting. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 30–45. Springer, Heidelberg (2006).  https://doi.org/10.1007/11841883_4 CrossRefGoogle Scholar
  8. 8.
    Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., Löwe, M.: Algebraic approaches to graph transformation - Part I: basic concepts and double pushout approach. In: Handbook of Graph Grammars and Computing by Graph Transformations. Foundations, vol. 1, pp. 163–246. World Scientific Publishing Co., Inc (1997). http://www.worldscientific.com/doi/abs/10.1142/9789812384720_0003
  9. 9.
    Costa, A., Bezerra, J., Azzi, G., Rodrigues, L., Becker, T.R., Herdt, R.G., Machado, R.: Verigraph: a system for specification and analysis of graph grammars. In: Ribeiro, L., Lecomte, T. (eds.) SBMF 2016. LNCS, vol. 10090, pp. 78–94. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-49815-7_5 CrossRefGoogle Scholar
  10. 10.
    Danos, V., Heindel, T., Honorato-Zimmer, R., Stucki, S.: Reversible sesqui-pushout rewriting. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 161–176. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-09108-2_11 Google Scholar
  11. 11.
    Ehrig, H.: Introduction to the algebraic theory of graph grammars (a survey). In: Claus, V., Ehrig, H., Rozenberg, G. (eds.) Graph-Grammars and Their Application to Computer Science and Biology. LNCS, vol. 73, pp. 1–69. Springer, Heidelberg (1979).  https://doi.org/10.1007/BFb0025714 CrossRefGoogle Scholar
  12. 12.
    Ehrig, H., Kreowski, H.-J.: Parallelism of manipulations in multidimensional information structures. In: Mazurkiewicz, A. (ed.) MFCS 1976. LNCS, vol. 45, pp. 284–293. Springer, Heidelberg (1976).  https://doi.org/10.1007/3-540-07854-1_188 CrossRefGoogle Scholar
  13. 13.
    Habel, A., Müller, J., Plump, D.: Double-pushout graph transformation revisited. Math. Struct. Comput. Sci. 11(5), 637–688 (2001).  https://doi.org/10.1017/S0960129501003425 MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Kastenberg, H., Rensink, A.: Model checking dynamic states in GROOVE. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 299–305. Springer, Heidelberg (2006).  https://doi.org/10.1007/11691617_19 CrossRefGoogle Scholar
  15. 15.
    Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon (1970). http://www.sciencedirect.com/science/article/pii/B978008012975450028X
  16. 16.
    Lack, S., Sobocinski, P.: Adhesive and quasiadhesive categories. Theor. Inform. Appl. 39(3), 511–545 (2005).  https://doi.org/10.1051/ita:2005028 MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Lambers, L.: Certifying rule-based models using graph transformation. Ph.D. thesis, Technische Universität Berlin (2010).  https://doi.org/10.14279/depositonce-2348
  18. 18.
    Lambers, L., Ehrig, H., Orejas, F.: Efficient conflict detection in graph transformation systems by essential critical pairs. ENTCS 211, 17–26 (2008).  https://doi.org/10.1016/j.entcs.2008.04.026 zbMATHGoogle Scholar
  19. 19.
    Löwe, M.: Graph rewriting in span-categories. In: Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT 2010. LNCS, vol. 6372, pp. 218–233. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15928-2_15 CrossRefGoogle Scholar
  20. 20.
    Plump, D.: Evaluation of functional expressions by hypergraph rewriting. Ph.D. thesis, University of Bremen, Germany (1993). http://d-nb.info/940423774
  21. 21.
    Rosen, B.K.: A Church-Rosser theorem for graph grammars. ACM SIGACT News 7(3), 26–31 (1975).  https://doi.org/10.1145/1008343.1008344 CrossRefGoogle Scholar
  22. 22.
    Taentzer, G.: AGG: a graph transformation environment for modeling and validation of software. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 446–453. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-25959-6_35 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Università di PisaPisaItaly
  2. 2.Université Grenoble-AlpeGrenobleFrance
  3. 3.Fachhochschule für die Wirtschaft HannoverHannoverGermany
  4. 4.Universidade Federal do Rio Grande do SulPorto AlegreBrazil

Personalised recommendations