Combining termination criteria by isolating deletion

Abstract

The functional behaviour of a graph transformation system is a crucial property in several application domains including model transformations and visual language engineering. Termination is one of the ingredients of functional behaviour and thus equally important. However, the termination of graph transformation systems is generally undecidable. Hence, most of the published termination criteria focus on specific classes of graph transformations. Unfortunately graph transformations with lots of production rules usually do not fit into one of these classes. It would be advantageous if different sets of the production rules in the graph transformation system could be verified using different criteria. This paper addresses this problem by providing structural conditions on the rules enabling such combination of termination criteria. © 2010 Springer-Verlag.