Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
B. Alpern and F. B. Schneider. Defining liveness. Inf. Pr. Lett., 21:181–185, 1985.
T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133–178, 2000.
F. Baader and T. Nipkow. Term Rewriting and All That. Cambr. Univ. Pr., 1998.
A. Bouajjani. Languages, rewriting systems, and verification of infinite-state systems. In Proc. ICALP’ 01, volume 2076 of LNCS, pages 24–39, 2001.
N. Dershowitz. Termination of rewriting. J. Symb. Comp., 3:69–116, 1987.
J. Giesl and T. Arts. Verification of Erlang processes by dependency pairs. Applicable Algebra in Engineering, Communication and Comp., 12(1,2):39–72, 2001.
J. Giesl and A. Middeldorp. Transforming context-sensitive rewrite systems. In Proc. 10th RTA, volume 1631 of Lecture Notes in Comp. Sc., pages 271–285, 1999.
J. Giesl and A. Middeldorp. Transformation techniques for context-sensitive rewrite systems. Journal of Functional Programming, 2003. To appear. Preliminary extended version in Technical Report AIB-2002-02, RWTH Aachen, Germany.
J. Giesl and H. Zantema. Liveness in rewriting. Technical Report AIB-2002-11, RWTH Aachen, Germany, 2002. http://aib.informatik.rwth-aachen.de.
L. Lamport. A new solution to Dijkstra’s concurrent programming problem. Communications of the ACM, 17(8):453–455, 1974.
H. Zantema. Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation, 17:23–50, 1994.
H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89–105, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giesl, J., Zantema, H. (2003). Liveness in Rewriting. In: Nieuwenhuis, R. (eds) Rewriting Techniques and Applications. RTA 2003. Lecture Notes in Computer Science, vol 2706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44881-0_23
Download citation
DOI: https://doi.org/10.1007/3-540-44881-0_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40254-1
Online ISBN: 978-3-540-44881-5
eBook Packages: Springer Book Archive