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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Bezem, M., Klop, J.W., de Vrijer, R. (eds.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)
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
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
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
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)
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
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
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)
Habel, A.: Hyperedge Replacement: Grammars and Languages. LNCS, vol. 643. Springer, Heidelberg (1992). https://doi.org/10.1007/BFb0013875
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
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
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
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
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
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
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
Plump, D.: Termination of graph rewriting is undecidable. Fundam. Inform. 33(2), 201–209 (1998). https://doi.org/10.3233/FI-1998-33204
Plump, D.: Computing by Graph Rewriting. Habilitation thesis, Universität Bremen, Fachbereich Mathematik und Informatik (1999)
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
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
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
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this chapter
Cite this chapter
Plump, D. (2018). Modular Termination of Graph Transformation. In: Heckel, R., Taentzer, G. (eds) Graph Transformation, Specifications, and Nets. Lecture Notes in Computer Science(), vol 10800. Springer, Cham. https://doi.org/10.1007/978-3-319-75396-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-75396-6_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-75395-9
Online ISBN: 978-3-319-75396-6
eBook Packages: Computer ScienceComputer Science (R0)