The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Jürgen Giesl and Hans Zantema
Liveness in Rewriting
2002-11
Abstract:
In this paper, we show how the problem of verifying
liveness properties is related to termination of term
rewrite systems (TRSs). We formalize liveness in the
framework of rewriting and present a sound and
complete transformation to transform liveness problems
into TRSs. Then the transformed TRS terminates if and
only if the original liveness property holds. This
shows that liveness and termination are essentially
equivalent. To apply our approach in practice, we
introduce a simpler sound transformation which only
satisfies the `only if'-part. By refining existing
techniques for proving termination of TRSs we show
how liveness properties can be verified automatically.
As an example, we prove a liveness property of a
waiting line protocol for a network of processes.
Regards,
Volker
--
http://www-i2.informatik.rwth-aachen.de/stolz/
