Liveness in rewriting

J. Giesl, H. Zantema

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

13 Citaten (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.
Originele taal-2Engels
TitelRewriting techniques and applications : 14th international conference, RTA 2003, Valencia, Spain, June 9-11, 2003 : proceedings
RedacteurenR. Nieuwenhuis
Plaats van productieBerlin
ISBN van geprinte versie978-3-540-40254-1
StatusGepubliceerd - 2003

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743


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

Citeer dit