A distributed operational semantics for CCS based on condition/event systems

A new set of inference rules for the guarded version of Milner's Calculus of Communicating Systems is proposed. They not only describe the actions agents may perform when in a given state, but also say which parts of the agents move when the global state changes. From the transition relation a particular Petri Net, namely a Condition/Event system called ?_ccs, is immediately derived. Our construction gives a semantics which is consistent with the interleaving semantics of CCS and exhibits full parallelism. The proof consists of relating the case graph of ?_CCS with the original and with the multiset (step) transition systems of the calculus.