Action refinement

The concept of action refinement was introduced by Ursula Goltz and myself, inspired by an example in [CDP], and described as follows [GG]:
We consider the design of concurrent systems in the framework of approaches where the basic building blocks are the actions which may occur in a system. By an action we understand here any activity which is considered as a conceptual entity on a chosen level of abstraction. This allows the representation of systems in a hierarchical way, changing the level of abstraction by interpreting actions on a higher level by more complicated processes on a lower level. We refer to such a change in the level of abstraction as refinement of actions. This approach is in the line of stepwise refinement, a methodology in program development first named and described in [Wirth]: a ``program is gradually developed in a sequence of refinement steps. In each step, one or several instructions of the given program are decomposed into more detailed instructions.'' More recently the keyword ``refinement'' has been used to indicate any transformation of a program or system that can be justified because the transformed program is related to the original through an implementation relation. Suitable implementation relations are preorders such as trace inclusion, various kinds of simulation or any of the semantic equivalences mentioned in this paper. Many papers in this tradition can be found in [ BRR]. In order to distinguish our notion of refinement, which is more in the spirit of [Wirth], from these latter approaches, we adopt the terminology action refinement.
The main themes in [GG] are the definition of an operator for refinement of actions on various models of concurrency, and studying which semantic equivalence notions are preserved under action refinement. These remain popular themes, and pointers to dozens of papers in his tradition can be found in [GG]. Our concept of action refinement is characterised by the following properties: The first property is in contrast to [Wirth] and many subsequent papers employing stepwise refinement. There actions have a prescribed input/output behaviour, which makes it possible to prove the correctness of a refinement step with respect to this behaviour.

[DGR] abandons the second and fourth property. This paper presents refinement as a category-theoretic construction on event structures, where for every pair of events it is specified explicitly to what extent relations of causality and conflict are inherited by the event structures substituted for these events.

The third property is abandoned in [CGG], where a conceptual distinction between atomic and compound actions is made; only the latter ones may be refined.
In papers by Boudol, Gorrieri and others (see [GG] for references) another concept of ``atomicity'' is introduced such that all actions are atomic, but they may still be refined when preserving atomicity. This results in atomic subprocesses that can not be ``interrupted'' by other activities. In [Boudol] two aspects of atomicity are considered, namely the all-or-nothing property (recoverability) and interference freedom, and two kinds of action refinement are proposed.

The fourth property has been abandoned in papers by Zwiers, Wehrheim, Huhn and others (see [GG] for references). In these papers causal dependence is given by a global dependency relation between actions, as in the work of Mazurkiewicz. Now causal dependence is inherited only to the extent that it fits this global dependency relation. Using a new process algebraic language with a linear time semantics, [Zwiers] and others show how to apply action refinement with regard to global action dependencies to the design of layered systems, having a sequential structure which still allows some parallelism, using the principle of communication closed layers. [Huhn] considers systems consisting of a parallel composition of a fixed number of sequential agents; local refinement functions allow to refine an action differently in different agents. A corresponding notion of refinement is introduced for a logic based on local modalities.

All properties except the third are abandoned in papers by Rensink and Gorrieri (see [GG] or [GR] for references). There a refinement function does not determine a unique refinement of a given system. Instead they advocate the use of vertical implementation relations, parametrised by refinement functions, that allow several correct refinements. In such a refinement step again not all causal relations need to be inherited.

The papers [GG] and [GR] offer thorough introductions to action refinement as well as surveys of the literature.


L. Castellano, G. De Michelis & L. Pomello (1987): Concurrency vs Interleaving: An Instructive Example. Bulletin of the European Association for Theoretical Computer Science 31, pp. 12-15.
J.W. de Bakker, W.P. de Roever & G. Rozenberg, editors (1990): Proceedings REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, Mook, The Netherlands, May/June 1989, LNCS 430. Springer.
G. Boudol (1989): Atomic actions (note). Bulletin of the European Association for Theoretical Computer Science 38, pp. 136-144.
I. Czaja, R.J. van Glabbeek & U. Goltz (1992): Interleaving semantics and action refinement with atomic choice. In G. Rozenberg, editor: Advances in Petri Nets 1992, LNCS 609, Springer, pp. 89-107.
P. Degano, R. Gorrieri & G. Rosolini (1993): A categorical view of process refinement. In J.W. de Bakker, W.P. de Roever & G. Rozenberg, editors: Proceedings REX Workshop on Semantics: Foundations and Applications, Beekbergen, The Netherlands, June 1992, LNCS 666, Springer, pp. 138-153.
R.J. van Glabbeek & U. Goltz (2001): Refinement of Actions and Equivalence Notions for Concurrent Systems. Acta Informatica 37(4/5), pp. 229-327.
R. Gorrieri & A. Rensink (2001): Action Refinement. In J.A. Bergstra, A. Ponse & S.A. Smolka, editors: Handbook of Process Algebra, Elsevier, 2001, pp. 1047-1147.
M. Huhn (1996): Action refinement and property inheritance in systems of sequential agents. In U. Montanari & V. Sassone, editors: Proceedings CONCUR '96: 7th International Conference on Concurrency Theory, Pisa, Italy, August 1996, LNCS 1119, Springer, pp. 639-654.
N. Wirth (1971): Program Development by Stepwise Refinement. Communications of the ACM 14(4), pp. 221-227.
J. Zwiers (1992): Layering and action refinement for typed systems. In J.W. de Bakker, C. Huizing, W.P. de Roever & G. Rozenberg, editors: Proceedings REX Workshop on Real-Time: Theory in Practice, Mook, The Netherlands, June 1991, LNCS 600, Springer, pp. 687-723.
My own papers on action refinement are:
Rob van Glabbeek