Liveness in rewriting

J. Giesl, H. Zantema

Research output: Book/ReportReportAcademic

89 Downloads (Pure)

Abstract

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.
Original languageEnglish
Place of PublicationAachen
PublisherRWTH Aachen
EditionMarch 2003 revised version
Publication statusPublished - 2002

Publication series

NameAachener Informatik Berichte
VolumeAIB2002-11
ISSN (Print)0935-3232

Fingerprint

Dive into the research topics of 'Liveness in rewriting'. Together they form a unique fingerprint.

Cite this