Liveness in rewriting

J. Giesl, H. Zantema

Onderzoeksoutput: Boek/rapportRapportAcademic

96 Downloads (Pure)


In this paper, we show how the problem of verifying liveness properties is related to termination of term rewrite systems (TRSs). We formalize live- ness in the framework of rewriting and present a sound and complete transformation to transform particular 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 examples, we prove a liveness property of a waiting line protocol for a network of processes and a liveness property of a protocol on a ring of processes.
Originele taal-2Engels
Plaats van productieAachen
UitgeverijRWTH Aachen
UitgaveMarch 2003 revised version
StatusGepubliceerd - 2002

Publicatie series

NaamAachener Informatik Berichte
ISSN van geprinte versie0935-3232


Duik in de onderzoeksthema's van 'Liveness in rewriting'. Samen vormen ze een unieke vingerafdruk.

Citeer dit