Interleaving Semantics

and Action Refinement with Atomic Choice

Ingo Czaja

Gesellschaft für Mathematik und Datenverarbeitung Postfach 1316, D-5205 Sankt Augustin, Germany

Rob J. van Glabbeek

Computer Science Department, Stanford University Stanford, CA 94305, USA

                              rvg@cs.stanford.edu

Ursula Goltz

Gesellschaft für Mathematik und Datenverarbeitung Postfach 1316, D-5205 Sankt Augustin, Germany

                               goltz@gmdzi.gmd.de

We investigate how to restrict the concept of action refinement such that established interleaving equivalences for concurrent systems are preserved under these restricted refinements. We show that interleaving bisimulation is preserved under refinement if we do not allow to refine action occurrences deciding choices and action occurrences involved in autoconcurrency. On the other hand, interleaving trace equivalence is still not preserved under these restricted refinements.

Keywords Concurrency, action refinement, atomicity, flow event structures, semantic equivalences, interleaving vs. partial orders, bisimulation.

Notes This paper appeared as Arbeitspapiere der GMD 594, Sankt Augustin 1991. The work presented here has partly been carried out within the Esprit Basic Research Action 3148 (DEMON) and the Sonderforschungsbereich 182 of the University of Erlangen-Nürnberg.

1 Introduction

For the design of concurrent systems, it can be useful to consider a hierarchy of representations, which allows refinement of unstructured entities on a more abstract design level by complex structures on a lower level. One approach which is being investigated is action refinement where the entities being refined are the actions which a system may perform. A single action in an abstract view may correspond to a process consisting of many actions in a more concrete representation. Action refinement is being investigated in process algebras [Aceto, AH, NEL] and in semantic models of concurrent systems [GG a/b/c, Vogler a/b, BDKP, Devillers, DD a/b, BGV].

Action refinement can be modelled as an operator, taking a system description P on a given level of abstraction as well as a refinement function ref associating processes with actions, and yielding a system description ref (P) on a lower level, obtained by replacing action occurrences by occurrences of the associated processes. It differs from many other operators that are considered for concurrent systems in that applying it on a representation of a system does not yield a representation of a different system, but a different representation of the same system.

An important question being considered is the following: Which equivalence notions for concurrent systems are preserved under refinement? Taking two system representations, P, Q, which are equivalent for some equivalence notion ∼, we would expect that ref (P) ∼ ref (Q) for any refinement function ref . This expectation indicates a big difference between action refinement and many other approaches for moving to a lower level of abstraction, in which adding more information about the precise implementation of systems makes it more likely that systems turn out to be different that were indistinguishable on the higher level of abstraction. Our expectation is based on the idea that in the original system representations P and Q it is not known how the actions will be implemented. However, it is decided that different occurrences of the same action will be implemented in the same way, so that any difference between P and Q that could arise after refinement is already visible in the abstract representations, namely through the use of different action names for corresponding events.

The preservation question has been addressed in the papers mentioned above. The usual approach to this problem is: Take some well-established equivalence notion. If it is not preserved under refinement, try to find the coarsest equivalence notion contained in it which has this property (see e.g. [Vogler a/b]).

What has not been considered so far is the following question. Given a well-established equivalence notion which is not preserved under refinement, is there a way of restricting either the allowed refinements or the class of system representations under consideration such that preservation of this equivalence in the restricted setting is obtained? This question is addressed in the present paper for two of the most basic equivalences.

We consider system descriptions in which the basic building blocks are the actions which may occur in a system. In our approach an action can be any activity which is considered as a conceptual entity on a chosen level of abstraction. Now we distinguish atomic actions that cannot be refined, and compound ones that can. One can think of atomic actions as being instantaneous and of compound actions as durational. Many approaches to concurrency in which actions are not supposed to be refined, in particular the interleaving approaches, in which parallelism is equated with arbitrary interleaving of action occurrences, can be thought of as dealing exclusively with the subclass of system representations were all actions in a system are atomic. On the other hand the action refinement approaches cited above take the possibility into account that any action can be refined. In this paper we look at systems in which some actions are atomic, and others can be refined. In particular we consider systems in which all action occurrences deciding choices, as well as all actions that can occur concurrently with themselves are atomic. These restrictions turn out to be sufficient to apply action refinement in certain interleaving semantics, while preserving semantic equivalence. Although the distinction between atomic and compound actions may be useful for motivating this research, technically one may just as well drop this distinction and restrict the class of allowed refinement functions to a class of what we call safe refinements. Those refinements do not refine action occurrences deciding choices and actions involved in autoconcurrency.

It turns out that the branching structure (i.e. the relative order of action occurrences and choices between different courses of action) of concurrent systems plays a rôle in our results. We show that interleaving bisimulation, where the branching structure between alternative executions is taken into account, is preserved under safe refinements. On the other hand, we show that interleaving trace equivalence (where the branching structure is fully neglected) is still not preserved under these restricted refinements. To investigate safe refinements for equivalence notions between these two extremes in the linear time – branching time spectrum has to be left for future research.

2 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 ⟹ 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_{1} + a_{2} in a; b, b should occur alternatively caused by a_{1} or by a_{2}. 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 E = (E, ≺, #, l), where

– E is a set of events,

– ≺ ⊆ 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 E ∈ IE will be denoted by E_{E}, ≺_{E}, #_{E} and l_{E}. The index E will be omitted if clear from the context.

Two flow event structures E and F are isomorphic (E ≅ F) iff there exists a bijection between their sets of events preserving ≺, # 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, selfconflicting events will never occur in any configuration. d ≺ 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 Let E ∈ IE.

(i) X ⊆ E is left-closed up to conflicts iff ∀d, e ∈ E: if e ∈ X, d ≺ e and d ∉ X then there exists an f ∈ X with f ≺ e and d # f. X ⊆ E is conflict-free iff #_{E}⌈X = ∅.

(ii) X ⊆ E is a (finite) configuration of E iff X is finite, left-closed up to conflicts and conflict-free and does not contain a causality cycle: <_{X} := (≺ ∩(X × X))^{+} is irreflexive. Conf (E) denotes the set of all (finite) configurations of E.

(iii) A configuration X ∈ Conf (E) is called maximal iff X ⊆ Y ∈ Conf (E) implies X = Y. It is complete iff ∀d ∈ E : d ∉ 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 ≺ 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.

Definition 2.3 Let E ∈ IE, X ∈ Conf (E).

(i) X enables e ∈ E iff e ∉ X and X ∪ {e} ∈ Conf (E).

(ii) A subset Y ⊆ X is a prefix of X iff ∀d ∈ X, e ∈ Y : d <_{X} e ⇒ d ∈ Y (i.e. Y is left-closed in X w.r.t. <_{X}).

Proposition 2.1 Let E ∈ IE, X ∈ Conf (E).

(i) X enables e iff e ∉ X, ¬(∃d ∈ X with d#e) and ∀d ≺ e we have d ∈ X ∨∃f ∈ X with f ≺ e and d#f.

(ii) X can be written as X = {e_{1},…, e_{n}} such that for k < n : {e_{1},…, e_{k}} enables e_{k+1}.

(iii) For Y ⊆ X, Y ∈ Conf (E) iff Y is a prefix of X.

Proof See [Boudol]. □

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.

Definition 2.4 Let E ∈ IE.

X ⟶^{e}_{E} X′ iff X enables e and X′ = X ∪ {e}.

X ⟶^{a}_{E} X′ iff X ⟶^{e}_{E} X′ and l(e) = a ∈ Act.

The index E is omitted if clear from the context.

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 Let E ∈ IE.

(i) For X ∈ Conf (E), let co_{X} ⊆ X × X be defined by d co_{X} e iff ¬(d <_{X} e ∨ e <_{X} d) .

(ii) co ⊆ E × E is defined by d co e iff ∃X ∈ Conf (E), X enables both d and e and X ∪ {d, e} ∈ Conf (E).

(iii) ch ⊆ E × E is defined by d ch e iff ∃X ∈ Conf (E), X enables both d and e and X ∪ {d, e} ∉ Conf (E).

Proposition 2.2 Let E ∈ IE, d, e ∈ E.

(i) d co e ⇔ ∃X ∈ Conf (E) with d co_{X} e.

(ii) d ch e ⇒ d # e.

Proof (i): “⇒”: Let d co e. Then there exists X ∈ Conf (E) with d, e both enabled by X. Let Y := X ∪ {d, e}. We show that d co_{Y} e. Assume d <_{Y} e. 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 <_{Y} e) and by symmetry ¬(e <_{Y} d).

“⇐”: Let X ∈ Conf (E) with d co_{X} e. Let X′ = X − {f ∈ X | d <_{X} f ∨ e <_{X} f}. 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_{1} := X′ − {d}, X_{2} := X′ − {e}, X′′ := X′ − {d, e}. Then X′, X_{1}, X_{2}, X′′ ∈ Conf (E) with proposition 2.1(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 ∈ Conf (E), with X ⟶^{d} X_{1} and X ⟶^{e} X_{2}. Let X′ := X ∪ {d, e}.

X′ is finite, since X ∈ Conf (E).

X′ is conflict-free, since X_{1}, X_{2} ∈ Conf (E) and ¬(d # e).

X′ is left-closed up to conflicts: Suppose f ∈ X′, g ∈ E − X′ and g ≺ f. Then f ∈ X_{i} for i = 1 or i = 2 and g ∉ X_{i}, so ∃h ∈ X_{i} ⊆ X′ with h ≺ f and g#h, since X_{i} ∈ Conf (E).

X′ contains no cycles w.r.t. ≺: Suppose X′ contains a causality cycle. Since X_{2} ∈ Conf (E) this cycle must contain d. However, we will show that there is no c ∈ X′ with d ≺ c. Since X, X_{1} ∈ Conf (E), X must be a prefix of X_{1} by proposition 2.1(iii), implying that d is maximal in X_{1}. Thus the only candidate for c is e. So suppose d ≺ e. Since d ∉ X_{2} and e ∈ X_{2} ∈ Conf (E) there must be an f ∈ X_{2} ⊆ X′ with f ≺ e and d#f, contradicting the conflict-freeness of X′.

Thus X′ ∈ Conf (E). □

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

Definition 2.6 Let E ∈ IE be a prime event structure.

#^{1} ⊆ E × E (immediate conflict) is defined by

d #^{1}e iff d # e, f < d ⇒ ¬(f # e) and f < e ⇒ ¬(f # d).

Proposition 2.3 Let E ∈ IE be a prime event structure, d, e ∈ E.

Then d ch e ⇔ d #^{1}e.

Proof “⇒”: Let d ch e. Then there exists X ∈ Conf (E) enabling both d and e. d#e by proposition 2.2. Assume there is an f with f < d. Then f ∈ X, since X ∪ {d} is left-closed. Since f ∈ X ∪ {e} ∈ Conf (E), we have ¬(f#e). Similarly f < e ⇒ ¬(f # d).

“⇐”: Let d #^{1}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 ∉ X. Let X_{1} = X ∪ {d} and X_{2} := X ∪ {e}. Since d # e we have X ∪ {d, e} ∉ Conf (E), so it suffices to prove that X, X_{1} and X_{2} are configurations.

X, X_{1} and X_{2} are finite (axiom of finite causes). X, X_{1} and X_{2} are left-closed (transitivity of <). X, X_{1} and X_{2} are conflict-free: It suffices to prove that X_{1} is conflict-free, since this implies that X is conflict-free, and the conflict-freeness of X_{2} follows by symmetry. Suppose d′, e′ ∈ X_{1} 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 #^{1}. □

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 \overline{}.

[figure: E =; a; #; b; #; c; d; F =; a; #; b; c; d]

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 F they are not in syntactic conflict: ¬(a #_{F} c). We have E_{E} = E_{F}, ≺_{E} = ≺_{F} and l_{E} = l_{F}. Moreover the choice relations of E and F agree: only a ch b. Nevertheless E has a configuration {a, d} which F has not.

Refinement of actions in flow event structures may now be defined as follows. We assume a refinement function ref : Act ⟶ IE−{O} (where O denotes the empty flow event structure) and replace each event labelled by a by a disjoint copy of 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 ref : Act ⟶IE−{O} is called a refinement function .

(ii) Let E ∈ IE and let ref be a refinement function. Then the refinement of E by ref , ref (E), is the flow event structure defined by

− E_{ref (E)} = {(e, e′) | e ∈ E_{E}, e′ ∈ E_{ref (l_{E}(e))}},

− (d, d′) ≺_{ref (E)} (e, e′) iff d ≺_{E} e or (d = e ∧ d′ ≺_{ref (l_{E}(d))} e′), − (d, d′) #_{ref (E)} (e, e′) iff d #_{E} e or (d = e ∧ d′ #_{ref (l_{E}(d))} e′), − l_{ref (E)}(e, e′) = l_{ref (l_{E}(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 E and F below, corresponding to a|b and ab + ba.

[figure: E =; a; b; F =; a; b; #; b; a]

E and F are indistinguishable in any kind of interleaving semantics. We refine action a by a_{1}a_{2}, i.e. ref (a) = a_{1} a_{2}, \overline{}and then have

[figure: ref (E) =; a_{1}; b; a_{2}; ,; ref (F) =; a_{1}; a_{2}; b; #; b; a_{1}; a_{2}; .]

ref (E) and ref (F) are not interleaving equivalent, since a_{1}b a_{2} is a possible execution of ref (E) but not of ref (F).

Example 2.3

Consider the event structures E and F below, corresponding to a|a and aa.

E =  a a  F =  a a^{}

E and F are indistinguishable in common interleaving semantics. We refine a by a_{1}a_{2} and then have

[figure: ref (E) =; a_{1}; a_{1}; a_{2}; a_{2}; ,; ref (F) =; a_{1}; a_{2}; a_{1}; a_{2}; .]

Now ref (E) and ref (F) are not interleaving equivalent, since only in ref (E) it is possible to start with two occurrences of a_{1}.

We observe that in example 2.2 an event of F is refined which decides a choice. In example 2.3, 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 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_{1} +a_{2} +.... 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 ref (a) is complete. This can be obtained by requiring that all events of ref (a) are mutually in conflict.

Definition 2.8 Let E ∈ IE.

(i) An action a ∈ Act is critical in 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_{E} := {a ∈ Act | a is critical in E} is the set of all critical actions in E.

(ii) A refinement function ref is called safe w.r.t. E iff ∀a ∈ Crit_{E} ∀d, e ∈ E_{ref (a)}, d ≠ e : d#_{ref (a)}e.

Proposition 2.4 Let E ∈ IE, a ∈ Crit_{E}, and ref a safe refinement w.r.t. E.

Then every non-empty configuration of ref (a) is complete.

Proof Trivial. □

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.

3 Interleaving trace semantics

We now investigate whether interleaving equivalences are preserved by safe refinements. We start by considering the simplest notion, the usual interleaving trace equivalence where the possible sequences of actions are compared.

Definition 3.1

w = a_{1} … a_{n} ∈ Act^{∗} is a (sequential) trace of E ∈ IE iff

∃X_{0},…, X_{n} ∈ Conf (E) : X_{0} = ∅ and X_{i−1} ⟶^{a_{i}} X_{i} , i = 1,…, n.

SeqT races(E) denotes the set of all sequential traces of E.

E, F ∈ IE are called interleaving trace equivalent (E ≈_{it} F) iff SeqT races(E) = SeqT races(F).

The following example shows that this equivalence is not preserved by safe refinements.

Example 3.1

Consider the event structures E and F below, corresponding to a(b|c) and abc + acb.

[figure: E =; a; b; c; F =; a; a; #; b; c; c; b]

E ≈_{it} F, since the only traces for both event structures are abc and acb (and the prefixes). Action b is not critical. We refine b by b_{1}b_{2}.

[figure: ref (E) =; a; b_{1}; b_{2}; c; ref (F) =; a; a; #; b_{1}; b_{2}; c; c; b_{1}; b_{2}]

We have ref (E) ≉_{it} ref (F), since ab_{1}c ∈ SeqT races(ref (E)), but ab_{1}c ∉ SeqT races(ref (F)).

One can now ask if it is possible to strengthen the requirement of safe refinements, say into trace-safe refinements, by requiring more actions to be atomic, in such a way that interleaving trace equivalence is preserved under trace-safe refinements. Requiring all actions that can occur concurrently with another action to be atomic would work, but this constraint is very restrictive. It seems not easy to find a less restrictive one.

4 Interleaving bisimulation semantics

In this section we will show that interleaving bisimulation equivalence [Park, Milner] is preserved under safe refinements.

Definition 4.1 Let E, F ∈ IE.

A relation R ⊆ Conf (E) × Conf (F) is called an interleaving bisimulation between E and F iff (∅, ∅) ∈ R, and if (X, Y) ∈ R then

– X ⟶^{a} X′ ⇒ ∃Y′ with Y ⟶^{a} Y′ and (X′, Y′) ∈ R,

– Y ⟶^{a} Y′ ⇒ ∃X′ with X ⟶^{a} X′ and (X′, Y′) ∈ R.

E and F are interleaving bisimulation equivalent (E ≈_{ib} F) iff there exists an interleaving bisimulation between E and F .

In [GG a] it has been shown that the configurations of a refined event structure may be deduced compositionally from the configurations of the original event structure and those of the refinements of actions. We will use this result and the following lemmas in the proof of the refinement theorem.

Definition 4.2 Let E ∈ IE, let ref be a refinement function.

(i) We call X̃ a refinement of a configuration X ∈ Conf (E) by ref iff

− X̃ = ⋃_{e∈X}({e} × X_{e}) where ∀e ∈ X : X_{e} ∈ Conf (ref (l_{E}(e))) − {∅},

− busy(X̃) ⊆ max(X) where · max(X) denotes the set of all maximal events in X w.r.t. <_{X}, · busy(X̃) := X − compl(X̃) and · compl(X̃) := {e ∈ X | X_{e} is a complete configuration}.

(ii) ref (X) denotes the set of refinements of X ∈ Conf (E) by ref and for S ⊆ Conf (E), ref (S) = ⋃_{X∈S} ref (X).

Clearly, if X̃ ∈ ref (X) then X = pr(X̃) := {e ∈ E_{E} | ∃e′ ∈ E_{ref (l(e))} : (e, e′) ∈ X̃} and we have compl(X̃) ⊆ pr(X̃), pr(X̃) − max(pr(X̃)) ⊆ compl(X̃).

Proposition 4.1 [GG a] Let E ∈ IE, let ref be a refinement function.

Then Conf (ref (E)) = ref (Conf (E)).

Lemma 4.1 Let E ∈ IE, ref a refinement function and X̃ ∈ Conf (ref (E)).

If compl(X̃) ⊆ Y ⊆ pr(X̃) then Y ∈ Conf (E).

Proof Immediate from proposition 2.1(iii), since pr(X̃) − max(pr(X̃)) ⊆ Y ⊆ pr(X̃). □

With lemma 4.1 we have in particular compl(X̃) ∈ Conf (E).

Lemma 4.2 Let E ∈ IE, X ∈ Conf (E) and a ∉ Crit_{E}.

X ⟶^{a} X_{1}, X ⟶^{a} X_{2} ⇒ X_{1} = X_{2}.

Proof Immediate from the definitions. □

Lemma 4.3 Let E ∈ IE, ref a safe refinement function w.r.t. E and X̃ ∈ Conf (ref (E)).
If e ∈ pr(X̃) − compl(X̃) then l_{E}(e) ∉ Crit_{E}.

Proof With proposition 4.1 we have X_{e} ∈ Conf (ref (l_{E}(e))) − {∅}. If l_{E}(e) ∈ Crit_{E} than X_{e} is complete by proposition 2.4. However, since e ∈ pr(X̃) − compl(X̃), X_{e} is not complete. □

Lemma 4.4 Let E ∈ IE, ref a safe refinement function w.r.t. E and X̃ ∈ Conf (ref (E)).
If compl(X̃) ∪ {e} ∈ Conf (E) then pr(X̃) ∪ {e} ∈ Conf (E).

Proof W.l.o.g. we assume that e ∉ pr(X̃). With proposition 2.1(i) we prove that pr(X̃) enables e.

Suppose ∃d ∈ pr(X̃) with d#e. Since compl(X̃) ∪ {e} is conflict-free, it follows that d ∈ pr(X̃) − compl(X̃). Thus compl(X̃) enables d (with lemma 4.1) as well as e, so d ch e. However, with lemma 4.3 we have l(d) ∉ Crit_{E}, contradicting d ch e.

Now suppose d ≺ e and d ∉ pr(X̃) ⊇ compl(X̃). Since compl(X̃) ∪ {e} ∈ Conf (E) there is an f ∈ compl(X̃) ⊆ pr(X̃) with f ≺ e and d#f. □

With these lemmas we can prove the theorem.

Theorem 4.1 Let E, F ∈ IE, let ref be a safe refinement function w.r.t. E and F.
Then E ≈_{ib} F ⇒ ref (E) ≈_{ib} ref (F).

Proof Let R be a bisimulation between E and F. Let R̃ = {(X̃, Ỹ) ∈ Conf (ref (E)) × Conf (ref (F)) |

(compl(X̃), compl(Ỹ)) ∈ R,

there exist bijections f : pr(X̃) ⟶ pr(Ỹ) with l_{F}(f(e)) = l_{E}(e)
and f̃: X̃ ⟶ Ỹ with f̃(e, e′) = (f(e), e′)}

We show that R̃ is a bisimulation between ref (E) and ref (F).

i. Obviously (∅, ∅) ∈ R̃.

ii. Let (X̃, Ỹ) ∈ R̃. Then (compl(X̃), compl(Ỹ)) ∈ R and there are bijections f and f̃ as required in the definition of R̃. We have to show the bisimulation properties. It suffices to check one of them, the other follows by symmetry.

Let X̃ ⟶^{a} X̃′. Let X̃′ − X̃ = {(e^{o}, e^{∗})}, l_{E}(e^{o}) = b. Then l_{ref (E)}((e^{o}, e^{∗})) = l_{ref (b)}(e^{∗}) = a. Now we have to show : ∃Ỹ′ ∈ Conf (ref (F)) with Ỹ ⟶^{a} Ỹ′ and (X̃′, Ỹ′) ∈ R̃. For the construction of Ỹ′, we distinguish two cases.

1. pr(X̃′) = pr(X̃).

In this case we can use the bijection f to define Ỹ′, since its domain is not affected by adding the new event.

Let Ỹ′ := {(f(e), e′) | (e, e′) ∈ X̃′}. With Ỹ = {(f(e), e′) | (e, e′) ∈ X̃} we have Ỹ′ = Ỹ ∪ {(f(e^{o}), e^{∗})}.

First we show that Ỹ′ is a configuration with Ỹ ⟶^{a} Ỹ′. Then we define the new functions f′ and f̃′ and check their properties. Finally we prove (compl(X̃′), compl(Ỹ′)) ∈ R.

With proposition 4.1 we show Ỹ′ ∈ Conf (ref (F)):

− pr(Ỹ′) = f(pr(X̃′)) = f(pr(X̃)) = pr(Ỹ) ∈ Conf (F), since Ỹ ∈ Conf (ref (F));

− ∀d ∈ pr(Ỹ′): Y′_{d} = X′_{f^{−1}(d)} ∈ Conf (ref (l_{E}(f^{−1}(d)))) − {∅} = Conf (ref (l_{F}(d))) − {∅}, since X̃′ ∈ Conf (ref (E));

− busy(Ỹ′) = pr(Ỹ′) − compl(Ỹ′) ⊆ pr(Ỹ) − compl(Ỹ) ⊆ max(pr(Ỹ)) = max(pr(Ỹ′)), since pr(Ỹ) = pr(Ỹ′) and compl(Ỹ) ⊆ compl(Ỹ′).

Thus Ỹ′ is a configuration of ref (F). Since l_{ref (F)}((f(e^{o}), e^{∗})) = l_{ref (b)}(e^{∗}) = a we have Ỹ ⟶^{a} Ỹ′.

Let f′ := f and f̃′ := f̃∪ {((e^{o}, e^{∗}), (f(e^{o}), e^{∗}))}. The new function f̃′ is bijective, since the events (e^{o}, e^{∗}) and (f(e^{o}), e^{∗}) do not occur in the domain and the range of f̃, respectively. By construction f′ and f̃′ have the required properties.

In order to establish (X̃′, Ỹ′) ∈ R̃ we still have to show (compl(X̃′), compl(Ỹ′)) ∈ R. Again we have two cases:

1.1. compl(X̃′) = compl(X̃).

Using the properties of f̃′, compl(Ỹ′) = f′(compl(X̃′)) = f(compl(X̃)) = compl(Ỹ), hence (compl(X̃′), compl(Ỹ′)) ∈ R.

1.2. compl(X̃′) ≠ compl(X̃).

Then compl(X̃′) = compl(X̃) ∪ {e^{o}} and compl(X̃) ⟶^{b} compl(X̃′).

Since (compl(X̃), compl(Ỹ)) ∈ R there is a Y′ ∈ Conf (F) with compl(Ỹ) ⟶^{b} Y′ and (compl(X̃′), Y′) ∈ R. Using the properties of f̃′, compl(Ỹ′) = f′(compl(X̃′)) = f(compl(X̃) ∪ {e^{o}}) =

compl(Ỹ) ∪ {f(e^{o})}, hence compl(Ỹ) ⟶^{b} compl(Ỹ′).

Since e^{o} ∈ compl(X̃′) ⊆ pr(X̃′) = pr(X̃), it follows that e^{o} ∈ pr(X̃) − compl(X̃) and with lemma 4.3 b = l_{E}(e^{o}) ∉ Crit_{E}. Hence Y′ = compl(Ỹ′) with lemma 4.2. Thus (compl(X̃′), compl(Ỹ′)) ∈ R, which had to be proved.

2. pr(X̃′) ≠ pr(X̃).

The proof of the second case is similar to that of the first case. However the construction of Ỹ′ is more complicated since we cannot just use the function f. We need to describe the events by which f is extended.

pr(X̃′) = pr(X̃) ∪ {e^{o}} and l_{E}(e^{o}) = b.

compl(X̃′) = \{ \begin{matrix}compl(X̃) ∪ \{e^{o}\} & if \{e^{∗}\} is a complete configuration of ref (b) \\ compl(X̃) & otherwise \end{matrix}

Thus compl(X̃′) ⊆ compl(X̃) ∪ {e^{o}} ⊆ pr(X̃) ∪ {e^{o}} = pr(X̃′). With lemma 4.1 it follows that compl(X̃) ∪ {e^{o}} ∈ Conf (E).

Hence compl(X̃) ⟶^{b} compl(X̃) ∪ {e^{o}}.

Since (compl(X̃), compl(Ỹ)) ∈ R, there is a d^{o} ∈ E_{F} with compl(Ỹ) ⟶^{b} compl(Ỹ) ∪ {d^{o}},

l_{F}(d^{o}) = b and (compl(X̃) ∪ {e^{o}}, compl(Ỹ) ∪ {d^{o}}) ∈ R.

We now extend the bijection f by (e^{o}, d^{o}). For this we verify that d^{o} is not in the range of f: Suppose d^{o} ∈ pr(Ỹ). Since d^{o} ∉ compl(Ỹ), f^{−1}(d^{o}) ∈ pr(X̃)−compl(X̃). Thus compl(X̃)∪ {f^{−1}(d^{o})} ∈ Conf (E) with lemma 4.1 and compl(X̃) ⟶^{b} compl(X̃) ∪ {f^{−1}(d^{o})}. Hence b ∉ Crit_{E} with lemma 4.3 and then e^{o} = f^{−1}(d^{o}) with lemma 4.2. Thus e^{o} ∈ pr(X̃) which contradicts pr(X̃′) ≠ pr(X̃). So d^{o} ∉ pr(Ỹ).

Now we can define Ỹ′, f′ and f̃′. Let f′ := f ∪ (e^{o}, d^{o}) and Ỹ′ := {(f′(e), e′) | (e, e′) ∈ X̃′} = Ỹ ∪ {(d^{o}, e^{∗})}.

Using proposition 4.1 we proof Ỹ′ ∈ Conf (ref (F)):

− pr(Ỹ′) = pr(Ỹ) ∪ {d^{o}} ∈ Conf (F) with lemma 4.4;

− ∀d ∈ pr(Ỹ′): Y′_{d} = X′_{f′^{−1}(d)} ∈ Conf (ref (l_{E}(f′^{−1}(d))))−{∅} = Conf (ref (l_{F}(d)))−{∅}; − busy(Ỹ′) = pr(Ỹ′) − compl(Ỹ′) = pr(Ỹ) ∪ {d^{o}} − compl(Ỹ′) ⊆

pr(Ỹ) ∪ {d^{o}} − compl(Ỹ), since compl(Ỹ) ⊆ compl(Ỹ′).

It remains to show that pr(Ỹ) ∪ {d^{o}} − compl(Ỹ) ⊆ max(pr(Ỹ) ∪ {d^{o}}).

By proposition 2.1(iii) pr(Ỹ) is a prefix of pr(Ỹ) ∪ {d^{o}}, so d^{o} ∈ max(pr(Ỹ) ∪ {d^{o}}). Now suppose d ∈ pr(Ỹ) − compl(Ỹ), but d ∉ max(pr(Ỹ) ∪ {d^{o}}). Then d ∈ max(pr(Ỹ)) by proposition 4.1, so d <_{pr(Ỹ)∪{d^{o}}} d^{o}. Since compl(Ỹ) ∪ {d^{o}} is a prefix of pr(Ỹ)∪{d^{o}} by proposition 2.1(iii), we have d ∈ compl(Ỹ), which yields a contradiction.

Thus Ỹ′ is a configuration of ref (F) and with l_{ref (F)}(d^{o}, e^{∗}) = a we have Ỹ ⟶^{a} Ỹ′.

The new function f′ is bijective, as shown above. The same for f̃′ := f̃∪{((e^{o}, e^{∗}), (d^{o}, d^{∗}))}. By construction f′ and f̃′ have the required properties.

Now we show (X̃′, Ỹ′) ∈ R̃ by proving (compl(X̃′), compl(Ỹ′)) ∈ R. There are again two cases:

2.1. compl(X̃′) = compl(X̃).

By construction of Ỹ′ (as in part 1.1 of the proof) compl(Ỹ′) = compl(Ỹ) and hence (compl(X̃′), compl(Ỹ′)) ∈ R.

2.2. compl(X̃′) ≠ compl(X̃).

Then compl(X̃′) = compl(X̃) ∪ {e^{o}} and by construction of Ỹ′, compl(Ỹ′) = compl(Ỹ) ∪ {d^{o}}. We had already that (compl(X̃) ∪ {e^{o}}, compl(Ỹ)) ∪ {d^{o}}) ∈ R, hence (compl(X̃′), compl(Ỹ′)) ∈ R.

Thus R̃ is a bisimulation between ref (E) and ref (F). □

Conclusion

We have investigated here how two well-established interleaving equivalences behave with respect to a restricted notion of action refinement. We have considered a class of refinements where events deciding choices are considered atomic. It turned out that interleaving trace semantics — neglecting the branching structure — is then still not preserved under refinements whereas interleaving bisimulation yields the desired preservation result.

It remains to be investigated what happens for other interleaving equivalences in the linear time – branching time spectrum, e.g. for failure semantics. Another interesting question is what happens for step semantics (where several actions happening simultaneously are considered). The example a(bc|d) versus ab(c|d) + a(b|d)c with ref (d) = d_{1}d_{2} may be used to show that step trace equivalence is not preserved under safe refinements as considered here. For step bisimulation equivalence we conjecture that we do have preservation under safe refinements.

Acknowledgements The idea to investigate refinements with atomic choice was suggested by Manfred Broy. Three anonymous referees helped with their comments to improve the paper.

References

[Aceto] L. Aceto: Action Refinement in Process Algebras, PhD-Thesis, University of Sussex, 1990, Report No. 3/91, University of Sussex, Computer Science, February 1991

[AH] L. Aceto, M. Hennessy: Adding Action Refinement to a Finite Process Algebra, Report No. 6/90, University of Sussex, Computer Science, November 1990, extended abstract in: Proc. ICALP 91, LNCS 510, Springer-Verlag, pp 506–519, 1991

[BDKP] E. Best, R. Devillers, A. Kiehn, L. Pomello: Concurrent Bisimulation in Petri Nets, Acta Informatica, Vol. 28, pp 231–264, 1991

[Boudol] G. Boudol: Flow Event Structures and Flow Nets, in I. Guessarian (ed.): Semantics of Systems of Concurrent Processes, LNCS 469, Springer-Verlag, pp 62–95, 1990

[BC] G. Boudol, I. Castellani: Permutation of Transitions: An Event Structure Semantics for CCS and SCCS, in J.W. de Bakker, W.-P. de Roever & G. Rozenberg (eds.): Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, Springer-Verlag, pp 411–427, 1989

[BGV] W. Brauer, R. Gold, W. Vogler: A Survey of Behaviour and Equivalence Preserving Refinements of Petri Nets, in: Advances in Petri Nets 1990, LNCS 483, Springer-Verlag, pp 1–46, 1990

[DD a] Ph. Darondeau, P. Degano: Event structures, Causal trees, and Refinements, in: Proc. MFCS 90, LNCS 452, Springer-Verlag, pp 239–245, 1990

[DD b] Ph. Darondeau, P. Degano: Refinement of Actions in Event Structures and Causal Trees, manuscript, 1991

[Devillers] R. Devillers: Maximality Preserving Bisimulation, Technical Report LIT-1214, Université Libre de Bruxelles, March 1990, to appear in TCS

[GG a] R.J. van Glabbeek, U. Goltz: Refinement of Actions in Causality Based Models, in J.W. de Bakker, W.-P. de Roever & G. Rozenberg (eds.): Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, LNCS 430, Springer-Verlag, pp 267–300, 1990

[GG b] R.J. van Glabbeek, U. Goltz: Equivalences and Refinement, in: I. Guessarian (ed.): Semantics of Systems of Concurrent Processes, LNCS 469, Springer-Verlag, pp 309– 333, 1990 [GG c] R.J. van Glabbeek, U. Goltz: A Deadlock-sensitive Congruence for Action Refine-

ment, SFB-Bericht Nr. 342/23/90 A, TUM-19044, Technische Universität München, November 1990

[Milner] R. Milner: A Calculus of Communicating Systems, LNCS 92, Springer-Verlag, 1980

[NEL] M. Nielsen, U. Engberg, K. S. Larsen: Fully Abstract Models for a Process Language with Refinement, in J.W. de Bakker, W.-P. de Roever & G. Rozenberg (eds.): Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, Springer-Verlag, pp 523–548, 1989

[NPW] M. Nielsen, G.D. Plotkin, G. Winskel: Petri Nets, Event Structures and Domains, Part I, Theoretical Computer Science, Vol. 13, No. 1, pp 85–108, 1981

[Park] D. Park: Concurrency and Automata on Infinite Sequences, in P. Deussen (ed.): Proc. 5th GI-Conference on Theoretical Computer Science, LNCS 104, Springer-Verlag, pp 167–183, 1981

[Vogler a] W. Vogler: Failures Semantics Based on Interval Semiwords is a Congruence for Refinement, Distributed Computing, Vol. 4, pp 139–162, 1991

[Vogler b] W. Vogler: Bisimulation and Action Refinement, in: Proc. STACS 91, LNCS 480, Springer-Verlag, pp 309–321, 1991