Modular termination of graph transformation

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.