Abstract
In [Aceto, Bloom and Vaandrager, '92] two strategies are presented to produce axiomatisations of strong bisimulation equivalence for languages whose operational semantics can be expressed in the GSOS format of [Bloom, Istrail and Meyer, '90]. In [Aceto et al.] it is stated that if the GSOS systems satisfy certain finiteness conditions, one of these axiomatisations is strongly normalising and confluent. We show that their claim as a whole is wrong, but prove confluency and weak normalisation by presenting a normalising rewrite strategy. We can however prove strong normalisation for the axiomatisations of a decidable class of such systems. The analysis of the term rewriting properties of the axiomatisations is modulo the associativity and commutativity of the choice operation.
The author was sponsored by the ESPRIT Basic Research Action 7166, Concur2.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
L. Aceto, B. Bloom, and F.W. Vaandrager. Turning SOS rules into equations. In Proceedings 7th Annual Symposium on Logic in Computer Science, Santa Cruz, California, pages 113–124. IEEE Computer Society Press, 1992. Full version available as CWI Report CS-R9218, June 1992, Amsterdam. To appear in the LICS 92 Special Issue of Information and Computation.
G.J. Akkerman and J.C.M. Baeten. Term rewriting analysis in process algebra. Report P9006, Programming Research Group, University of Amsterdam, 1990.
B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can't be traced: Preliminary report. In Conference Record of the 15th ACM Symposium on Principles of Programming Languages, San Diego, California, pages 229–239, 1988. Full version available as Technical Report 90-1150, Department of Computer Science, Cornell University, Ithaca, New York, August 1990. Accepted to appear in Journal of the ACM.
J.F. Groote and F.W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202–260, October 1992.
J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing, 15:1155–1194, 1986.
J.W. Klop. Term rewriting systems. In Handbook of Logic in Computer Science, Volume II. Oxford University Press, 1992. To appear.
Huimin Lin. PAM: A Process Algebra Manipulator (Version 1.0). Report 4/93, Computer Science, University of Sussex, Brighton, February 1993.
E. Madelaine, R. de Simone, and D. Vergamini. ECRINS V2-1, USERS MANUAL, 1989.
R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.
G.D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
R. de Simone. Higher-level synchronising devices in MEIJE-SCCS. Theoretical Computer Science, 37:245–267, 1985.
C. Verhoef. A congruence theorem for structured operational semantics with predicates and negative premises. Computing Science Notes 93/18, Eindhoven University of Technology, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bosscher, D.J.B. (1994). Term rewriting properties of SOS axiomatisations. In: Hagiya, M., Mitchell, J.C. (eds) Theoretical Aspects of Computer Software. TACS 1994. Lecture Notes in Computer Science, vol 789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57887-0_108
Download citation
DOI: https://doi.org/10.1007/3-540-57887-0_108
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57887-1
Online ISBN: 978-3-540-48383-0
eBook Packages: Springer Book Archive