Partial order semantics for refinement of actions---neither necessary nor always sufficient but appropriate when used with care

This note continues a series of papers in the Bulletin of the EATCS about the relative merits of partial order semantics and interleaving semantics, starting with [CDP]. That paper pointed out a significant advantage of partial order semantics, by formulating a desirable property of semantic equivalences that is not met by interleaving equivalences. This property is preservation under refinement of actions. A semantic equivalence is preserved under action refinement if two equivalent processes remain equivalent after replacing all occurrences of an action a by a more complicated process r(a). For example, r(a) may be a sequence of two actions a 1 and a2 • This property may be desirable in applications where concurrent systems are modelled at different levels of abstraction, and where the actions on an abstract level turn out to represent complex processes on a more concrete level. Therefore for example [Pratt] and [Lamport) already advocate the use of semantic equivalences that are not based on action atomicity.