Liveness in rewriting

J. Giesl, H. Zantema

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

13 Citations (Scopus)
2 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 liveness 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
Title of host publicationRewriting techniques and applications : 14th international conference, RTA 2003, Valencia, Spain, June 9-11, 2003 : proceedings
EditorsR. Nieuwenhuis
Place of PublicationBerlin
ISBN (Print)978-3-540-40254-1
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


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

Cite this