On the relationship of CCS and CSP
- 164 Downloads
This paper compares two models of concurrency, Milner's Calculus of Communicating Systems (CCS) and the failures model of Communicating Sequential Processes (CSP) developed by Hoare, Brookes and Roscoe. By adapting Milner's synchronisation trees to serve as notation for both CCS and CSP, we are able to define a representation mapping for CSP processes. We define an equivalence relation on synchronisation trees which corresponds precisely to the notion of failure equivalence. Milner's calculus is founded on a different notion, observation equivalence. We show how these two equivalences are related. Just as Milner's equivalence can be characterised as the smallest relation satisfying a set of axioms, we find a suitable set of axioms for the failures equivalence relation. This again makes explicit the differences between the two systems, as well as revealing that the semantic models underlying CCS and CSP are comparable.
KeywordsNormal Form Proof System Parallel Composition Visible Action Communicate Sequential Process
Unable to display preview. Download preview PDF.
- Milner, R., A Calculus for Communicating Systems, Springer LNCS Vol. 92 (1980).Google Scholar
- Hoare, C.A.R., Brookes, S.D., and Roscoe, A.W., A Theory of Communicating Sequential Processes, Technical Report PRG-16, Oxford University Computing Laboratory, Programming Research Group (1981).Google Scholar
- Hennessy, M.C.B. and Plotkin, G.D., A Term Model for CCS, Proceedings of 9th MFCS Conference, Springer LNCS Vol. 88 (1980).Google Scholar
- Hennessy, M.C.B. and Milner, R., On observing nondeterminism and concurrency, in: Springer LNCS Vol. 85 (1979).Google Scholar
- Hoare, C.A.R., Communicating Sequential Processes, CACM 21, Vol. 8 (1978).Google Scholar
- Hennessy, M., and de Nicola, R., Testing equivalences for processes, Technical Report, University of Edinburgh (July 1982).Google Scholar
- Brookes, S.D., A Model for Communicating Sequential Processes, Ph.D thesis, University of Oxford (submitted 1983).Google Scholar
- Roscoe, A.W., A Mathematical Theory of Communicating Sequential Processes, Ph.D thesis, University of Oxford (1982).Google Scholar
- Darondeau, Ph., An enlarged definition and complete axiomatization of observational congruence of finite processes, Proceedings of International Symposium on Programming, Springer LNCS 137 (1982).Google Scholar
- Rounds, W.C., and Brookes, S.D., Possible futures, acceptances, refusals, and communicating processes, Proceedings of 22itnd Symposium on Foundations of Computer Science (October 1981).Google Scholar