DERIVING DISTRIBUTED PROCESSES FROM CONCURRENT PROCESSES

In this paper we present a notion of refinement for process algebras m otivated by converting an abstract specification into a concrete imple mentation. We start with CCS specifications and convert them to specif ications with asynchronous message passing. A derived specification de scribes an implementation on distributed memory systems. That is indiv idual actions in a CCS process are transformed into processes which ma y involve explicit message passing actions. As the original specificat ion and the refined implementation exhibit different actions, they can not be equated under the usual notions of observational equivalence. H ence we introduce an indexed relation, which allows irrelevant actions to be abstracted away. A few properties satisfied by the indexed rela tion are presented.