Bruggink, Sander:
Towards a systematic method for proving termination of graph transformation systems
In: Proceedings of the Graph Transformation for Verification and Concurrency workshop (GT-VC 2007) - Lisbon, 2007
Buchaufsatz/Kapitel in Sammelwerk / Fach: Informatik
Titel:
Towards a systematic method for proving termination of graph transformation systems
Autor(in):
Bruggink, Sander im Online-Personal- und -Vorlesungsverzeichnis LSF anzeigen
Erscheinungsjahr:
2007
Erschienen in:
Proceedings of the Graph Transformation for Verification and Concurrency workshop (GT-VC 2007) - Lisbon, 2007
Link URL:

Abstract:

We describe a method for proving the termination of graph transformation systems. The method is based on the fact that infinite reductions must include infinite 'creation chains', that is chains of edges in different graphs the reduction sequence, such that each edge is involved in creating the next edge. In our approach, the length of such creation chains is recorded by associating with each edge label a creation depth, which denotes the minimal length of a creation chain from an edge in the initial graph to that edge. We develop an algorithm which can prove the absence of such infinite chains (and therefore termination), analyse problems of the approach and propose possible solutions.