Advertisement

Modular Termination of Graph Transformation

  • Detlef PlumpEmail author
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10800)

Abstract

We establish a machine-checkable condition which ensures that the union of two terminating hypergraph transformation systems is terminating. The condition is based on so-called sequential critical pairs which represent consecutive rule applications that are not independent. In contrast to a corresponding modularity result for term rewriting, no restrictions on the form of rules are required. Our result applies to both systems with injective rules and systems with rules that merge nodes or edges.

References

  1. 1.
    Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRefzbMATHGoogle Scholar
  2. 2.
    Bezem, M., Klop, J.W., de Vrijer, R. (eds.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)zbMATHGoogle Scholar
  3. 3.
    Bruggink, H.J.S.: Towards a systematic method for proving termination of graph transformation systems. Electron. Notes Theor. Comput. Sci. 213(1), 23–38 (2008).  https://doi.org/10.1016/j.entcs.2008.04.072 CrossRefzbMATHGoogle Scholar
  4. 4.
    Bruggink, H.J.S., König, B., Nolte, D., Zantema, H.: Proving termination of graph transformation systems using weighted type graphs over semirings. In: Parisi-Presicce, F., Westfechtel, B. (eds.) ICGT 2015. LNCS, vol. 9151, pp. 52–68. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21145-9_4 CrossRefGoogle Scholar
  5. 5.
    Bruggink, H.J.S., König, B., Zantema, H.: Termination analysis for graph transformation systems. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 179–194. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44602-7_15 Google Scholar
  6. 6.
    Courcelle, B.: Graph rewriting: an algebraic and logic approach. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, Chap. 5. Elsevier (1990)Google Scholar
  7. 7.
    Dershowitz, N.: Termination of linear rewriting systems (preliminary version). In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 448–458. Springer, Heidelberg (1981).  https://doi.org/10.1007/3-540-10843-2_36 CrossRefGoogle Scholar
  8. 8.
    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
  9. 9.
    Ehrig, H., Rosen, B.K.: Commutativity of independent transformations on complex objects. Research Report RC 6251. IBM Thomas J. Watson Research Center, Yorktown Heights (1976)Google Scholar
  10. 10.
    Habel, A.: Hyperedge Replacement: Grammars and Languages. LNCS, vol. 643. Springer, Heidelberg (1992).  https://doi.org/10.1007/BFb0013875 zbMATHGoogle Scholar
  11. 11.
    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
  12. 12.
    Hoffmann, B., Plump, D.: Implementing term rewriting by jungle evaluation. RAIRO Theor. Inform. Appl. 25(5), 445–472 (1991).  https://doi.org/10.1051/ita/1991250504451 MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Hristakiev, I., Plump, D.: Towards critical pair analysis for the graph programming language GP 2. In: James, P., Roggenbach, M. (eds.) WADT 2016. LNCS, vol. 10644, pp. 153–169. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-72044-9_11 CrossRefGoogle Scholar
  14. 14.
    Krishna Rao, M.R.K.: Modular aspects of term graph rewriting. Theor. Comput. Sci. 208(1–2), 59–86 (1998).  https://doi.org/10.1016/S0304-3975(98)00079-6 MathSciNetzbMATHGoogle Scholar
  15. 15.
    Plump, D.: Implementing term rewriting by graph reduction: termination of combined systems. In: Kaplan, S., Okada, M. (eds.) CTRS 1990. LNCS, vol. 516, pp. 307–317. Springer, Heidelberg (1991).  https://doi.org/10.1007/3-540-54317-1_100 CrossRefGoogle Scholar
  16. 16.
    Plump, D.: On termination of graph rewriting. In: Nagl, M. (ed.) WG 1995. LNCS, vol. 1017, pp. 88–100. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60618-1_68 CrossRefGoogle Scholar
  17. 17.
    Plump, D.: Simplification orders for term graph rewriting. In: Prívara, I., Ružička, P. (eds.) MFCS 1997. LNCS, vol. 1295, pp. 458–467. Springer, Heidelberg (1997).  https://doi.org/10.1007/BFb0029989 CrossRefGoogle Scholar
  18. 18.
    Plump, D.: Termination of graph rewriting is undecidable. Fundam. Inform. 33(2), 201–209 (1998).  https://doi.org/10.3233/FI-1998-33204 MathSciNetzbMATHGoogle Scholar
  19. 19.
    Plump, D.: Computing by Graph Rewriting. Habilitation thesis, Universität Bremen, Fachbereich Mathematik und Informatik (1999)Google Scholar
  20. 20.
    Plump, D.: Confluence of graph transformation revisited. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 280–308. Springer, Heidelberg (2005).  https://doi.org/10.1007/11601548_16 CrossRefGoogle Scholar
  21. 21.
    Sabel, D., Zantema, H.: Termination of cycle rewriting by transformation and matrix interpretation. Log. Methods Comput. Sci. 13(1), 38 (2017).  https://doi.org/10.23638/LMCS-13(1:11)2017 MathSciNetzbMATHGoogle Scholar
  22. 22.
    Toyama, Y.: Counterexamples to termination for the direct sum of term rewriting systems. Inf. Process. Lett. 25, 141–143 (1987).  https://doi.org/10.1016/0020-0190(87)90122-0 MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Zantema, H., König, B., Bruggink, H.J.S.: Termination of cycle rewriting. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 476–490. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08918-8_33 Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.University of YorkYorkUK

Personalised recommendations