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  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.
|Title of host publication||Frontiers of Combining Systems (Proceedings 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005)|
|Place of Publication||Berlin|
|Number of pages||16|
|ISBN (Print)||3-540-29051-6, 978-3-540-29051-3|
|Publication status||Published - 2005|
|Name||Lecture Notes in Computer Science (LNCS)|
|Name||Lecture Notes in Artificial Intelligence (LNAI)|