A partial ordering semantics for CCS

A new operational semantics for "pure" CCS is proposed that considers the parallel operator as a first class one, and permits a description of the calculus in terms of partial orderings. The new semantics (also for unguarded agents) is given in the SOS style via the partial ordering derivation relation. CCS agents are decomposed into sets of sequential sub-agents, and the new derivations which relate sets of sub-agents describe their actions and their causal dependencies. The computations obtained by animating sets of sub-agents via the partial ordering derivation relation are "observed" either as interleaving or partial orderings of events. Interleavings coincide with Milner's many step derivations, and "linearizations" of partial orderings are all and only interleavings. In order to obtain more abstract semantics, we introduce two relations of partial ordering observational equivalence and congruence that preserve concurrency. These are finer than Milner's exactly in that they distinguish interleaving of sequential nondeterministic agents from their concurrent execution.