Modular Termination of Graph Transformation

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


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.


  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). 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). 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). 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). 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). 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). 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). MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Hoffmann, B., Plump, D.: Implementing term rewriting by jungle evaluation. RAIRO Theor. Inform. Appl. 25(5), 445–472 (1991). 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). CrossRefGoogle Scholar
  14. 14.
    Krishna Rao, M.R.K.: Modular aspects of term graph rewriting. Theor. Comput. Sci. 208(1–2), 59–86 (1998). 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). 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). 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). CrossRefGoogle Scholar
  18. 18.
    Plump, D.: Termination of graph rewriting is undecidable. Fundam. Inform. 33(2), 201–209 (1998). 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). 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). MathSciNetzbMATHGoogle Scholar
  22. 22.
    Toyama, Y.: Counterexamples to termination for the direct sum of term rewriting systems. Inf. Process. Lett. 25, 141–143 (1987). 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). Google Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.University of YorkYorkUK

Personalised recommendations