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 a given state, but also say which parts of the agents move when the global state changes. From the transition relation a Condition/Event system, called ?CCS, is immediately derived and two demonstrations are given of its adequacy as a truly concurrent and distributed CCS semantics. First, we prove that the abstract interleaving case graph of ?CCS (i.e., the case graph with arcs labelled by single actions) is homomorphic to the transition system defined by Milner's inference rules. Since the homomorphisrn preserves transitions, we also have that the synchronization trees of two corresponding nodes are identical. Thus, our construction gives a semantics which is consistent with the original interleaving semantics of CCS whatever behavioural equivalence is chosen. Second, we prove that the transition system expressing a multiset semantics for CCS is transition-preserving hornornorphic to the abstract case graph of ?CCS (i.e., the case graph with arcs labelled by multisets of actions) and thus that the amount of parallelism exhibited by ?CCS and by multiset CCS is the same.