Refinement of actions and equivalence notions for concurrent systems

We study an operator for refinement of actions to be used in the design of concurrent systems. Actions on a given level of abstraction are replaced by more complicated processes on a lower level. This is done in such a way that the behaviour of the refined system may be inferred compositionally from the behaviour of the original system and from the behaviour of the processes substituted for actions. We recall that interleaving models of concurrent systems are not suited for defining such an operator in its general form. Instead, we define this operator on several causality based, event oriented models, taking into account the distinction between deadlock and successful termination. Then we investigate the interplay of action refinement with abstraction in terms of equivalence notions for concurrent systems, considering both linear time and branching time approaches. We show that besides the interleaving equivalences, also the equivalences based on steps are not preserved under refinement of actions. We prove that linear time partial order semantics are invariant under refinement. Finally we consider various bisimulation equivalences based on partial orders and show that the finest two of them are preserved under refinement whereas the others are not. Termination sensitive versions of these equivalences are even congruences for action refinement.