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