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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1-2), 133–178 (2000)
Courtois, P.J., Heymans, F., Parnas, D.L.: Concurrent control with “readers” and “writers”. Commun. ACM 14(10), 667–668 (1971)
Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 279–301 (1982)
Francez, N.: Fairness. Springer, Heidelberg (1986)
Giesl, J., Zantema, H.: Liveness in rewriting. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 321–336. Springer, Heidelberg (2003)
Giesl, J., Zantema, H.: Simulating liveness by reduction strategies. Electr. Notes TCS 86(4) (2003)
Hoare, C.A.R.: Monitors: an operating system structuring concept. Commun. ACM 17(10), 549–557 (1974)
Koprowski, A., Zantema, H.: Proving liveness with fairness using rewriting. Technical Report CS-Report 05-06, Tech. Univ. of Eindhoven (March 2005), Available from http://w3.tue.nl/en/services/library/digilib/tue_publications/reports/
Lankford, D.S.: On proving term rewriting systems are noetherian. Technical Report MTP-3, Math. Dept., Louisiana Tech. Univ., Ruston (May 1979)
Raynal, M., Beeson, D.: Algorithms for mutual exclusion. MIT Press, Cambridge (1986)
Silberschatz, A., Galvin, P.B., Gagne, G.: Operating system concepts. John Wiley & Sons, Inc., Chichester (2004)
TeReSe. Term Rewriting Systems. Cambridge Tracts in TCS, vol. 55. Cambridge University Press, Cambridge (2003)
Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24(1/2), 89–105 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Koprowski, A., Zantema, H. (2005). Proving Liveness with Fairness Using Rewriting. In: Gramlich, B. (eds) Frontiers of Combining Systems. FroCoS 2005. Lecture Notes in Computer Science(), vol 3717. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11559306_13
Download citation
DOI: https://doi.org/10.1007/11559306_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29051-3
Online ISBN: 978-3-540-31730-2
eBook Packages: Computer ScienceComputer Science (R0)