Proving liveness with fairness using rewriting

A. Koprowski, H. Zantema

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

6 Citations (Scopus)


In this paper we combine rewriting techniques with verification issues. More precisely, we show how techniques for proving relative termination of term rewrite systems (TRSs) can be applied to prove liveness properties in fair computations. We do this using a new transformation which is stronger than the sound transformation from [5] but still is suitable for automation. On the one hand we show completeness of this approach under some mild conditions. On the other hand we show how this approach applies to some examples completely automatically, using the TPA tool designed for proving relative termination of TRSs. In particular we succeed in proving liveness in the classical readers-writers synchronization problem.
Original languageEnglish
Title of host publicationFrontiers of Combining Systems (Proceedings 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005)
EditorsB. Gramlich
Place of PublicationBerlin
Number of pages16
ISBN (Electronic)978-3-540-31730-2
ISBN (Print)3-540-29051-6, 978-3-540-29051-3
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science (LNCS)
ISSN (Print)0302-9743
NameLecture Notes in Artificial Intelligence (LNAI)


Dive into the research topics of 'Proving liveness with fairness using rewriting'. Together they form a unique fingerprint.

Cite this