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:
Actions are uninterpreted, and there is no concept of the
correctness of a refinement.
The refinement of a given system description is completely
determined by a refinement function, mapping actions to system
descriptions.
All actions may be refined.
All relations of causal (in)dependence and conflict that exist
between actions before refinement are inherited by the refined
system.
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.
(with W.P. Weijland) Refinement in
branching time semantics, in which we show that branching
bisimulation is preserved under action refinement and weak bisimulation
isn't, when working with sequential systems only.
(with U. Goltz) Refinement of
actions in causality based models, in which the operation of
action refinement is defined on various kinds of event structures, the
here newly introduced configuration structures, and on Petri nets.
(with U. Goltz) A deadlock-sensitive
congruence for action refinement, in which we upgrade the
requirement of being preserved under action refinement into being a
congruence for action refinement, which forces us to distinguish
deadlock from successful termination.
(with N. Busi & R. Gorrieri)
Axiomatising ST-bisimulation equivalence, in which we give a
semantics and axiomatisation for a language with action refinement,
and also a new treatment of forgetful refinement,
refining an action into the empty process.
(with F.W. Vaandrager) The
difference between splitting in n and n+1, in
which we show that splitting actions in a sequence of finitely many
stages is not sufficient to obtain the discriminating power of general
action refinement.