DERIVING DISTRIBUTED PROCESSES FROM CONCURRENT PROCESSES

In this paper we present a notion of refinement for process algebras motivated by converting an abstract specification into a concrete implementation. We start with CCS specifications and convert them to specifications with asynchronous message passing. A derived specification describes an implementation on distributed memory systems. That is individual actions in a CCS process are transformed into processes which may involve explicit message passing actions. As the original specification and the refined implementation exhibit different actions, they cannot be equated under the usual notions of observational equivalence. Hence we introduce an indexed relation, which allows irrelevant actions to be abstracted away. A few properties satisfied by the indexed relation are presented.