Proving liveness with fairness using rewriting

A. Koprowski, H. Zantema

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

5 Citations (Scopus)

Abstract

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
PublisherSpringer
Chapter13
Pages232-247
Number of pages16
ISBN (Electronic)978-3-540-31730-2
ISBN (Print)3-540-29051-6, 978-3-540-29051-3
DOIs
Publication statusPublished - 2005

Publication series

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

Fingerprint

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

Cite this