A Termination Criterion for Graph Transformations with Negative Application Conditions

Abstract

Termination of graph transformations is in general undecidable, but it is possible to prove it for specific systems by checking for sufficient conditions. In the presence of rules with negative application conditions, the difficulties increase.
In this paper we propose a different approach to the identification of a (sufficient) criterion for termination, based on the construction of a labelled transition system whose states represent overlaps between the negative application condition and the right hand side that can give rise to cycles.