Contents of Basic Notions

We consider systems which are capable of performing actions from a given set Act of action names. By an action we understand here any activity which is considered as an conceptual entity on a chosen level of abstraction. We will not distinguish external and internal actions; we do not consider abstraction by hiding of actions in this paper.

We will sometimes give process algebra terms for examples to make them easier to understand: + will denote choice (as in CCS), | will denote parallel composition (without communication), a, b,...∈Act denote actions, and ; denotes a general sequential composition operator (like the one of ACP). The semicolon will sometimes be omitted and we use the usual precedence rule that ; binds stronger than the other operators. However this notation is only used for intuition; formally our results are established for event structures.

We will describe a concurrent system by a set of events where each event corresponds to an occurrence of some action. Therefore, events are labelled by action names.

The simplest form of event structures has been introduced in [NPW] and is usually referred to as prime event structures with binary conflicts. A labelled prime event structure is a tuple (E, < ,#, l ) where E is the set of events, < ⊆E×E is an (irreflexive) partial order (the causality relation), # ⊆E×E is the so-called conflict relation, and l : E→Act specifies the labelling of events by action names. As usual, we require < to satisfy the axiom of finite causes; that is, any event may have only finitely many predecessors. Furthermore, # is required to be irreflexive and symmetric and to respect the axiom of conflict heredity: ∀d, e, f∈E : d # e∧d < f $\Longrightarrow$ e # f.

A prime event structure represents a concurrent system in the following way: action names a∈Act represent actions the system may perform, an event e∈E labelled with a represents an occurrence of a during a possible run of the system, d < e means that d is a prerequisite for e and d # e means that d and e cannot happen both in the same run.

The behaviour of a prime event structure is described by explaining which subsets of events constitute possible runs of the represented system. These subsets are called configurations. They have to be conflict-free and they must be left-closed with respect to < (all prerequisites for any event occurring in the run must also occur).

As shown in [GG a], prime event structures are well suited to define a notion of action refinement, as long as actions are not refined by behaviours containing conflicts.

But as a consequence of the axioms explained above, it is cumbersome to define a more general notion of refinement directly for prime event structures. Whenever a given event occurs, it has to be ``enabled" by a unique set of events that is independent of the particular run of the system, namely by all its predecessors according to the causality relation. However, when refining a by a₁ + a₂ in a ;b, b should occur alternatively caused by a₁ or by a₂. In prime event structures, this may only be modelled by duplicating the b-event, leading to complicated definitions and proofs. Hence more expressive event structure representations are being used for refinement. Free event structures as defined in [DD a] seem to be weakest extension of prime event structures to allow refinements with conflicts in a straightforward way. However, difficulties with the interpretation of the notion of causality in this model lead in [DD b] to a restriction such that prime event structures are no longer a subclass. In [GG a, GG b], flow event structures [BC] have been used which are also a convenient model for CCS. This is the model we have chosen here as well, in order to establish our results also for refinements with conflicts.

We will now introduce the main concepts of flow event structures following closely [Boudol].

Definition 2.1

A (labelled) flow event structure (over an alphabet Act) is a 4-tuple
$\cal {E}$ = (E, $\prec$ ,#, l ), where

E is a set of events,
$\prec$ ⊆E×E is an irreflexive relation, the flow relation,
#⊆E×E is a symmetric relation, the conflict relation,
l : E→Act is the labelling function.

Let IE denote the domain of flow event structures labelled over Act. The components of $\cal {E}$ ∈ IE will be denoted by E, $\prec_{{\cal E}}^{}$ ,# and l. The index $\cal {E}$ will be omitted if clear from the context.

Two flow event structures $\cal {E}$ and $\cal {F}$ are isomorphic ( $\cal {E}$ ≅ $\cal {F}$ ) iff there exists a bijection between their sets of events preserving $\prec$ ,# and labelling. Often, we will not distinguish isomorphic event structures; the names of events are not important for us.

The interpretation of the conflict and the flow relation is formalised by defining configurations of flow event structures. Configurations must be conflict free; in particular, self-conflicting events will never occur in any configuration. d $\prec$ e will mean that d is a possible immediate cause for e. For an event to occur it is necessary that a complete non-conflicting set of its causes has occurred. Here a set of causes is complete if for any cause which is not contained there is a conflicting event which is contained. Finally, no cycles with respect to causal dependence may occur.

We will only consider finite configurations here. As usual, we assume that in a finite period of time only finitely many actions may be performed. Now the requirement says that we only consider runs which are executable in a finite period of time. This is no restriction since the infinite configurations which are usually considered are completely determined by the finite ones (see e.g. [Boudol]).

Definition 2.2

(i)	X⊆E is left-closed up to conflicts iff ∀d, e∈E: if e∈X, d $\prec$ e and d $\not\in$ X then there exists an f∈X with f $\prec$ e and d # f. X⊆E is conflict-free iff #⌈X = ∅.
(ii)	X⊆E is a (finite) configuration of $\cal {E}$ iff X is finite, left-closed up to conflicts and conflict-free and does not contain a causality cycle: < _X : = ( $\prec$ ∩(X×X))⁺ is irreflexive. $\it Conf\/$ ( $\cal {E}$ ) denotes the set of all (finite) configurations of $\cal {E}$ .
(iii)	A configuration X∈ $\it Conf\/$ ( $\cal {E}$ ) is called maximal iff X⊆Y∈ $\it Conf\/$ ( $\cal {E}$ ) implies X = Y. It is complete iff ∀d∈E : d $\not\in$ X⇒∃e∈X with d # e.

The relation < _X expresses causal dependence in the configuration X. Note that prime event structures are special flow event structures defining d $\prec$ e iff d < e. In prime event structures, the requirement of left-closedness up to conflicts for configurations reduces to left-closedness: ∀d, e∈E : if e∈X∧d < e then d∈X; furthermore, in each configuration X, the relation < _X coincides with <. However in prime event structures every maximal configuration is complete, whereas in flow event structures this need not be the case (although every complete configuration must be maximal). In [GG c] the difference between complete and maximal configurations is used to model deadlock behaviour: complete configurations indicate successful termination, whereas incomplete maximal configurations model deadlocks.

The following observations may offer some additional motivation for the definition of configurations above.

Proposition 2.1

(i)	X enables e iff e $\not\in$ X,¬(∃d∈X with d#e) and ∀d $\prec$ e we have d∈X∨∃f∈X with f $\prec$ e and d#f.
(ii)	X can be written as X = {e₁,..., e_n} such that for k < n : {e₁,..., e_k} enables e_k+1.
(iii)	For Y⊆X, Y∈ $\it Conf\/$ ( $\cal {E}$ ) iff Y is a prefix of X.

We now define transition relations between configurations, describing which event or which action may occur in a configuration and which configuration may then be obtained.

Next we introduce a relation co_X expressing when two events are concurrent (independent) within a configuration X, as well as a global relation co, expressing possible concurrency, and show that the relations correspond. Furthermore we define when there is a choice between two events.

Definition 2.5

(i)	For X∈ $\it Conf\/$ ( $\cal {E}$ ), let co_X⊆X×X be defined by d co_X e iff ¬(d < _Xe∨e < _Xd ) .
(ii)	co⊆E×E is defined by d co e iff ∃X∈ $\it Conf\/$ ( $\cal {E}$ ), X enables both d and e and X∪{d, e}∈ $\it Conf\/$ ( $\cal {E}$ ).
(iii)	ch⊆E×E is defined by d ch e iff ∃X∈ $\it Conf\/$ ( $\cal {E}$ ), X enables both d and e and X∪{d, e} $\not\in$ $\it Conf\/$ ( $\cal {E}$ ).

Proof
(i):
`` ⇒": Let d co e. Then there exists X∈ $\it Conf\/$ ( $\cal {E}$ ) with d, e both enabled by X.
Let Y : = X∪{d, e}. We show that d co_Y e.
Assume d < _Ye. Then X∪{e} would not be a prefix of Y, hence X∪{e} would not be a configuration and e not enabled by X. Thus ¬(d < _Ye) and by symmetry ¬(e < _Yd ).

`` ⇐": Let X∈ $\it Conf\/$ ( $\cal {E}$ ) with d co_X e. Let X' = X - {f∈X | d < _Xf∨e < _Xf}.
d, e∈X', since d, e∈X and d and e are not in < _X-relation.
Moreover d and e are maximal in X' w.r.t. < _X.
Let X₁ : = X' - {d}, X₂ : = X' - {e}, X'' : = X' - {d, e}.
Then X', X₁, X₂, X''∈ $\it Conf\/$ ( $\cal {E}$ ) with proposition

(iii) and d co e.

(ii):
Suppose d ch e, but ¬(d # e). We show that for each configuration X enabling d and e, also X' : = X∪{d, e} is a configuration.
Let X∈ $\it Conf\/$ ( $\cal {E}$ ), with X $\buildrel$ d $\over$ →X₁ and X $\buildrel$ e $\over$ →X₂. Let X' : = X∪{d, e}.

X' is conflict-free, since X₁, X₂∈ $\it Conf\/$ ( $\cal {E}$ ) and ¬(d # e).

X' is left-closed up to conflicts:
Suppose f∈X', g∈E - X' and g $\prec$ f. Then f∈X_i for i = 1 or i = 2 and g $\not\in$ X_i, so ∃h∈X_i⊆X' with h $\prec$ f and g#h, since X_i∈ $\it Conf\/$ ( $\cal {E}$ ).

X' contains no cycles w.r.t. $\prec$ :
Suppose X' contains a causality cycle. Since X₂∈ $\it Conf\/$ ( $\cal {E}$ ) this cycle must contain d. However, we will show that there is no c∈X' with d $\prec$ c. Since X, X₁∈ $\it Conf\/$ ( $\cal {E}$ ), X must be a prefix of X₁ by proposition

(iii), implying that d is maximal in X₁. Thus the only candidate for c is e. So suppose d $\prec$ e. Since d $\not\in$ X₂ and e∈X₂∈ $\it Conf\/$ ( $\cal {E}$ ) there must be an f∈X₂⊆X' with f $\prec$ e and d#f, contradicting the conflict-freeness of X'.

For prime event structures, the choice relation coincides with the non-inherited conflicts.

Proof
`` ⇒": Let d ch e. Then there exists X∈ $\it Conf\/$ ( $\cal {E}$ ) enabling both d and e.
d#e by proposition

.
Assume there is an f with f < d. Then f∈X, since X∪{d} is left-closed. Since f∈X∪{e}∈ $\it Conf\/$ ( $\cal {E}$ ), we have ¬(f#e).
Similarly f < e⇒¬(f # d ).

`` ⇐": Let d #¹e. Let X : = {f∈E | f < d∨f < e}.
Since d # e it cannot be the case that d < e or e < d by the axiom of conflict heredity and the irreflexivity of #. Thus d, e $\not\in$ X.
Let X₁ = X∪{d} and X₂ : = X∪{e}.
Since d # e we have X∪{d, e} $\not\in$ $\it Conf\/$ ( $\cal {E}$ ), so it suffices to prove that X, X₁ and X₂ are configurations.

X, X₁ and X₂ are finite (axiom of finite causes).
X, X₁ and X₂ are left-closed (transitivity of <).
X, X₁ and X₂ are conflict-free:
It suffices to prove that X₁ is conflict-free, since this implies that X is conflict-free, and the conflict-freeness of X₂ follows by symmetry.
Suppose d', e'∈X₁ and d' # e'. We may assume d'≤d and e' < e, since the cases that d' and e' are both predecessors of d or of e are excluded by the axiom of conflict heredity and the irreflexivity of #. But then d # e' by conflict heredity, violating the definition of #¹. $\Box$

Note that for prime event structures the conflict relation is fully determined by the immediate conflicts, and hence by the choice relation. On the other hand, in flow event structures the choice relation does not determine the conflict relation. Moreover, the part of the conflict relation that is not determined by the choice relation influences the set of configurations (as well as the deadlock behaviour [GG c]).

Example 2.1

Consider the following two flow event structures, where the labelling is the identity. Here and later we represent the flow relation by arrows of the form
$\begin{picture}(11,2) \put(0,1){\line (1,0){11}} \put(0,1){\vector(1,0){ 6}} \end{picture}$
.

$\begin{picture}(149,37)(-20,5) \put( 5,36){\makebox(0,0)[b]{${\cal E} =$}} \put(... ...} \put(99,20){\line (-3,-4){ 7.5}} \put(99,20){\vector(-3,-4){ 4}} \end{picture}$

In both event structures the events a and c are in semantic conflict, in the sense that they cannot occur in the same configuration. However, in $\cal {F}$ they are not in syntactic conflict: ¬(a # c).
We have E = E, $\prec_{{\cal E}}^{}$ = $\prec_{{\cal F}}^{}$ and l = l. Moreover the choice relations of $\cal {E}$ and $\cal {F}$ agree: only a ch b. Nevertheless $\cal {E}$ has a configuration {a, d} which $\cal {F}$ has not.

Refinement of actions in flow event structures may now be defined as follows. We assume a refinement function $\it ref\/$ : Act→ IE- {O} (where O denotes the empty flow event structure) and replace each event labelled by a by a disjoint copy of $\it ref\/$ (a). The conflict and causality structure will be inherited. Refinements in which some actions are replaced by the empty process can drastically change the behaviour of concurrent systems and can not be explained by a change in the level of abstraction at which these systems are regarded [GG a]. Therefore they are not considered here.

Definition 2.7

(i)

A function $\it ref\/$ : Act→IE- {O} is called a refinement function .

(ii)

Let $\cal {E}$ ∈ IE and let $\it ref\/$ be a refinement function.
Then the refinement of $\cal {E}$ by $\it ref\/$ , $\it ref\/$ ( $\cal {E}$ ), is the flow event structure defined by

-	E₍₎ = {(e, e') \| e∈E, e'∈E_(l(e))},
-	(d, d') $\prec_{{{\it ref\/}({\cal E})}}^{}$ (e, e') iff d $\prec_{{\cal E}}^{}$ e or ( d = e∧d' $\prec_{{{\it ref\/}(l_{\cal E}(d))}}^{}$ e'),
-	(d, d') #₍₎ (e, e') iff d # e or ( d = e∧d' #_(l(d)) e'),
-	l₍₎(e, e') = l_(l(e))(e') .

The following examples illustrate that the usual interleaving equivalences are not preserved under this refinement operation.

The event structures we consider in examples from now on will always be prime; hence we will only draw immediate conflicts and omit arcs for the elements of the flow relation obtainable by transitivity.

Example 2.2

Consider the event structures $\cal {E}$ and $\cal {F}$ below, corresponding to a| b and ab + ba.

$\begin{picture}(149,25)(-15,3) \put(15,21){\makebox(0,0)[b]{${\cal E} =$}} \put(... ...5}} \put(100,20){\line (0,-1){10}} \put(100,20){\vector(0,-1){ 5}} \end{picture}$

$\cal {E}$ and $\cal {F}$ are indistinguishable in any kind of interleaving semantics. We refine action a by a₁a₂, i.e. $\it ref\/$ (a) =
$\begin{picture}(22,2) \put(4,0){\makebox(0,0)[br]{$a_1$}} \put(17,0){\makebox(0,... ...l]{$a_2$,}} \put(5,1){\line (1,0){11}} \put(5,1){\vector(1,0){ 6}} \end{picture}$
and then have

$\begin{picture}(149,40)(-15,3) \put(15,36){\makebox(0,0)[b]{${\it ref\/}({\cal E... ... \put(100,35){\vector(0,-1){ 5}} \put(105,36){\makebox(0,0)[b]{.}} \end{picture}$

$\it ref\/$ ( $\cal {E}$ ) and $\it ref\/$ ( $\cal {F}$ ) are not interleaving equivalent, since a₁b a₂ is a possible execution of $\it ref\/$ ( $\cal {E}$ ) but not of $\it ref\/$ ( $\cal {F}$ ).

Example 2.3

Consider the event structures $\cal {E}$ and $\cal {F}$ below, corresponding to a| a and aa.

$\begin{picture}(149,24)(-15,4) \put(15,21){\makebox(0,0)[b]{${\cal E} =$}} \put(... ...$a$}} \put(80,20){\line (0,-1){10}} \put(80,20){\vector(0,-1){ 5}} \end{picture}$

$\cal {E}$ and $\cal {F}$ are indistinguishable in common interleaving semantics. We refine a by a₁a₂ and then have

$\begin{picture}(149,46)(-15,6) \put(15,45){\makebox(0,0)[b]{${\it ref\/}({\cal E... ...} \put(80,20){\vector(0,-1){4.5}} \put(85,45){\makebox(0,0)[b]{.}} \end{picture}$

Now $\it ref\/$ ( $\cal {E}$ ) and $\it ref\/$ ( $\cal {F}$ ) are not interleaving equivalent, since only in $\it ref\/$ ( $\cal {E}$ ) it is possible to start with two occurrences of a₁.

We observe that in example

an event of $\cal {F}$ is refined which decides a choice. In example

, an action is refined which may occur concurrently with itself. Hence we have identified two classes of events which will definitely cause problems for interleaving semantics if they are refined. We will now call actions labelling such events critical (with respect to a particular event structure $\cal {E}$ ) and consider the subclass of flow event structures where all critical actions are atomic, in the sense that they cannot really be refined. We could restrict the allowed refinement functions such that atomic actions may only be `refined' by themselves. However, our refinement theorem will hold even in a slightly more general setting. First of all we may allow renaming of atomic actions, obtained by refining them by conflict-free event structures containing exactly one event, as well as restriction of certain (atomic) actions, obtained by refining them by event structures consisting of one self-conflicting event. In this way the relabelling and restriction operators of CCS can still be understood as instances of the refinement operator. Moreover we allow generalised renamings, replacing (atomic) actions by (possibly infinite) choices a₁ + a₂ + ... . The crucial restriction is that the execution of any event of a refined atomic action a leads to its immediate termination, thereby preserving atomicity for these actions. Formally this is ensured if and only if every non-empty configuration of $\it ref\/$ (a) is complete. This can be obtained by requiring that all events of $\it ref\/$ (a) are mutually in conflict.

Definition 2.8

(i)	An action a∈ $\it Act\/$ is critical in $\cal {E}$ iff ∃d, e∈E with d ch e and l (d )= a or ∃d, e∈E, d≠e with d co e and l (d )= l (e) = a. Crit : = {a∈Act \| a is critical in $\cal {E}$ } is the set of all critical actions in $\cal {E}$ .
(ii)	A refinement function $\it ref\/$ is called safe w.r.t. $\cal {E}$ iff ∀a∈ Crit ∀d, e∈E_(a), d≠e : d#_(a)e.

In flow event structures it may be difficult to find out which actions are critical and should therefore be atomic. A safe strategy is to avoid autoconcurrency altogether and make every event which is in conflict with another event atomic. The result of this strategy depends on the particular flow event structure representation of a system by the choice of a syntactic conflict relation # (recall that semantic and syntactic conflict do not coincide for flow event structures). The most liberal possibilities for refinement are obtained by choosing a minimal conflict relation to model the intended behaviour.