Abstract
We give sound and complete proof systems for a variety of bisimulation based equivalences over a message-passing process algebra. The process algebra is a generalisation of CCS where the actions consist of receiving and sending messages or data on communication channels; the standard prefixing operator a.p is replaced by the two operators c?x.p and c!e.p and in addition messages can be tested by a conditional construct. The various proof systems are parameterised on auxiliary proof systems for deciding on equalities or more general boolean identities over the expression language for data. The completeness of these proof systems are thus relative to the completeness of the auxiliary proof systems.
This work has been supported by the SERC grant GR/H16537 and the ESPRIT BRA project CONCUR II
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
G. Burns. A language for value-passing CCS. Technical Report ECS-LFCS-91-175, LFCS, University of Edinburgh, August 1991.
R. Cleaveland, J. Parrow, and B. Steffen. A semantics based verification tool for finite state systems. In Proceedings of the 9th International Symposium on Protocol Specification, Testing and Verification, North Holland, 1989.
J.F. Groote and A. Ponse. The syntax and semantics of μCRL. Technical Report CS-R9076, CWI, Amsterdam, 1990.
J.F. Groote and A. Ponse. Proof theory for μCRL. Technical Report CS-R9138, CWI, Amsterdam, 1991.
M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.
M. Hennessy. A proof system for communicating processes with value-passing. Formal Aspects of Computing, 3:346–366, 1991.
M. Hennessy and A. Ingolfsdottir. A theory of communicating processes with value-passing. Technical Report 3/89, CSAI, University of Sussex, 1992. To appear in Information and Computation.
M. Hennessy and H. Lin. Symbolic bisimulations. Technical Report 1/92, Computer Science, University of Sussex, 1992.
M. Hennessy and H. Lin. Proof systems for message-passing process algebras. Technical Report 5/93, Computer Science, University of Sussex, 1993.
C.A.R. Hoare and A.W. Roscoe. The laws of occam. Technical Report PRG Monograph, Oxford University, 1988.
H. Lin. PAM: A process algebra manipulator. In Computer Aided Verification, volume 575 of Lecture Notes in Computer Science, pages 136–146. Springer-Verlag, 1991.
H. Lin. A verification tool for value-passing process. Technical Report Forthcoming, Computer Science, University of Sussex, 1993.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile proceses, part i. Information and Computation, 100(1):1–40, 1992.
J. Parrow and D. Sangiorgi. Algebraic theories for value-passing calculi. Report Forthcoming, SICS and Edinburgh University, 1993.
D. Walker. Automated analysis of mutual exclusion algorithms using CCS. Formal Aspects of Computing, 1:273–292, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hennessy, M., Lin, H. (1993). Proof systems for message-passing process algebras. In: Best, E. (eds) CONCUR'93. CONCUR 1993. Lecture Notes in Computer Science, vol 715. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57208-2_15
Download citation
DOI: https://doi.org/10.1007/3-540-57208-2_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57208-4
Online ISBN: 978-3-540-47968-0
eBook Packages: Springer Book Archive