Prof. Barbara König

Abstract:

Given a program or system, it is often important to know whether it
(always) terminates. Clearly - due to the undecidability of the halting
problem - this can not be solved in the general case. However, there are
several approximative methods that work well in practice. On the other
hand, there are only few approaches that can handle termination of
evolving graphs.

Here we introduce techniques for proving uniform termination of graph
transformation systems, based on matrix interpretations for string
rewriting. We generalize this technique by adapting it to graph
rewriting instead of string rewriting and by generalizing to ordered
semirings. In this way we obtain a framework which is based - depending
on the semiring - on so-called tropical, arctic and arithmetic type
graphs. These type graphs can be used to assign weights to graphs and to
show that these weights decrease in every rewriting step in order to
prove termination. We present an example involving counters and discuss
the implementation in the tool Grez.

(Joint work with H.J. Sander Bruggink, Dennis Nolte, Hans Zantema)