ICSP and its relationship with ACSP and CSP

Abstract

A mathematical model for asynchronously communicating processes, called ICSP, is proposed in the style of the failures-divergences model for synchronously communicating processes. It improves on the ACSP model of Josephs, Hoare and He ([5]) by its ability to model infinitary processes while retaining the salient features of ACSP. The model is shown to be a c.p.o, under a natural determinism ordering. A host of operators are defined and proved to be continuous. We show that the ACSP model corresponds to the contextual equivalence on ICSP processes and that ICSP processes are essentially input buffered CSP processes which have only internal choice on output events. A category theoretic formulation of the results is also provided.