A distributed operational semantics of CCS based on condition/event systems (Q1110338)

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 \(\Sigma_{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 \(\Sigma_{CCS}\) with the original and with the multiset (step) transition systems of the calculus.