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 pureCCS where the actions consist of receiving and sending messages or data on communication channels; the standard prefixing operatora.p is replaced by the two operatorsc?x.p andc!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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Burns, G. A language for value-passing ccs. Technical Report ECS-LFCS-91-175, University of Edinburgh, August 1991.
Cleaveland, R., Parrow, J., Steffen, B. The concurrency workbench: A semantics based verification tool for finite state systems.ACM Transactions on Programming Systems, 15:36–72, 1989.
Groote, J.F., Ponse, A. The syntax and semantics ofμCRL. Technical Report CS-R9076, CWI, Amsterdam, 1990.
Groote, J.F., Ponse, A. Proof theory forμCRL. Technical Report CS-R9138, CWI, Amsterdam, 1991.
Hennessy, M.An Algebraic Theory of Processes. MIT Press, 1988.
Hennessy, M. A proof system for communicating processes with value-passing.Formal Aspects of Computer Science, 3:346–366, 1991.
Hennessy, M., Ingolfsdottir, A. A theory of communicating processes with value-passing.Information and Computation, 107(2):202–236, 1993.
Hennessy, M. Lin, H. Symbolic bisimulations. Theoretical Computer Science, 138:353–389, 1995.
Hennessy, M. Liu, X. A modal logic for message passing processes.Acta Informatica, 32:375–393, 1995.
Hoare, C.A.R., Roscoe, A.W. The laws of occam. Technical Report PRG Monograph 53, Oxford University Computing Laboratory, 1986.
Lin, H. PAM: A process algebra manipulator. In K. Larsen and A. Skou, editors,Computer Aided Verification, volume 575 ofLecture Notes in Computer Science, pages 136–146. Springer-Verlag, 1991. Also available as Sussex Computer Science Technical Report 9/91.
Lin, H. A verification tool for value-passing processes. InProceedings of 13th International Symposium on Protocol Specification, Testing Verification, IFIP Transactions. North-Holland, 1993.
Milner, R.Communication and Concurrency. Prentice-Hall, 1989.
Milner, R., Parrow, J., Walker, D. A calculus of mobile proceses, part i.Information and Computation, 100(1):1–40, 1992.
Parrow, J., Sangiorgi, D. Algebraic theories for value-passing calculi. Technical report, University of Edinburgh, 1993. Also Technical Report from SICS, Sweden. To appear in Information and Computation.
Walker, D. Automated analysis of mutual exclusion algorithms using CCS.Formal Aspects of Computing, 1:273–292, 1989.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Hennessy, M., Lin, H. Proof systems for message-passing process algebras. Formal Aspects of Computing 8, 379–407 (1996). https://doi.org/10.1007/BF01213531
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/BF01213531