Well-behaved Flow Event Structures for Parallel Composition and Action Refinement

Rob van Glabbeek

Computer Science Department, Stanford University Stanford, CA 94305-9045, USA.

                                  rvg@cs.stanford.edu

Ursula Goltz

Institut für Software, Technische Universität Braunschweig Postfach 3329, D-38106 Braunschweig, Germany.

                                   U.Goltz@tu-bs.de

Flow event structures were introduced as a model for giving semantics to process algebras. However it turned out that certain restrictions have to be made to make them suitable for this purpose. In this paper, we investigate subclasses of flow event structures which are both suited for the process algebraic composition operators, and for action refinement as a means of regarding processes on different levels of abstraction.

First, suitable subclasses are characterised. Then two specific subclasses are proposed. The larger class generalises the one from [CZ], which is not suitable for action refinement. The smaller one is still sufficiently expressive for dealing with all standard process algebras and action refinement.

Keywords Concurrency, flow event structures, parallel composition, action refinement.

Introduction

Flow event structures were introduced in [BC-a] as a model of concurrency that is particularly suited for giving semantics to languages like CCS and CSP, while faithfully representing causality and branching time. Indeed, the interpretation of the operators of such languages in terms of flow event structures is particularly straightforward and intuitive [BC-a/b]. Structurally, flow event structures closely resemble prime event structures [NPW]. However, prime event structures are not as suitable for defining parallel composition operators with synchronisation. Flow event structures were proposed as a canonical generalisation of prime event structures suitable for defining parallel composition (besides all other CCS-like operators).

However, in [CZ] it turned out that the definition of parallel composition on flow event structures, although seemingly intuitive, does not always give the desired result. Technically, the problem can be pinpointed by the failure of parallel composition to correspond with the product in a suitable category of event structures, or — alternatively — as a failure of compositionality: the behaviour of the parallel composition of two flow event structures, as given by its family of configurations, is not determined by the behaviours of its two arguments.

This problem was solved in [CZ] by defining a subclass of flow event structures, closed under the operators of CCS, on which parallel composition is well-behaved. The subclass consists of those flow event structures which satisfy a complicated structural property, called Δ.

In [GG] we defined an operator for action refinement on flow event structures and other causality based, event oriented models of concurrency. This operator describes a change in the level of abstraction at which a system is represented by interpreting actions on a higher level by more complicated processes on a lower level. On flow event structures, this operator could be defined in a much more straightforward and intuitive way than on competing models like stable (or bundle) event structures or Petri nets.^{1} Action refinement turned out to behave compositionally on the entire domain of flow event structures.

In order to interpret both parallel composition and action refinement (and the other CCS-like operators) on flow event structures, it therefore seems appropriate to restrict attention to the flow event structures satisfying Δ. However, it turns out that this class is not closed under action refinement. Therefore, in this paper our aim is to define a different subclass of flow event structures, closed under action refinement, parallel composition and the other CCS-like operators, on which parallel composition still behaves well.

In [Winskel] a general parallel composition operator is proposed that is parameterised by the choice of a so-called synchronisation algebra. Depending on the choice of this parameter, the parallel composition operators of CCS, CSP, SCCS, ACP and many other system description languages can be obtained. Other process algebraic operators like choice, sequential composition, restriction, renaming etc. may be expressed in terms of action refinement. Therefore, it is sufficient to check closure under, and compositionality of, Winskel’s general parallel composition operator and action refinement; the same properties then hold for many other process algebraic operators, including the ones of CCS.

In this paper, we consider the parallel product of Winskel underlying his parallel composition operator on the domain of unlabelled flow event structures. The various instances of Winskel’s parallel composition operator can be expressed in terms of labelled versions of this parallel product and restriction. Accordingly we consider event refinement as the corresponding operator underlying action refinement. In Section 2 of this paper we formalise when parallel product is well-behaved on a subclass of flow event structures. We infer that parallel product is the categorical product in a suitable category of flow event structures if and only if that operator is well-behaved on that class. Moreover, as we show in Section 3, parallel product is compositional on any class of flow event structures on which it is well behaved. This implies that parallel composition is compositional on the labelled counterpart of such a class. The compositionality of the other CCS-like operators on such a class follows from the compositionality of action refinement. It remains to find a class of flow event structures, closed under parallel product and event refinement, on which parallel product is well behaved.

1In [DD], the model of free event structures is shown to be equally suitable as flow event structures for defining action refinement. However, like prime event structures, they are not very suitable for defining parallel composition with synchronisation.

In fact, two such subclasses are proposed in Section 4. The larger class turns out to contain all flow event structures satisfying Δ. The smaller one is still sufficiently expressive for dealing with all standard process algebras and action refinement. These classes will be proposed in Section 4 by introducing a semantic concept of (fairly) well-behaved flow event structures.

1 Basic notions

In this section, we introduce flow event structures and operators for event refinement and parallel composition.

A flow event structure describes a concurrent system as a set of events, modelling action occurrences, together with two relations: the flow relation represents “possible immediate causes” of events; the conflict relation expresses which events mutually exclude each other.

Definition 1.1

A flow event structure is a triple E = (E, ≺, #) 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).

In graphical representations of flow event structures we represent ≺ by arcs of the form \overline{}−.

Let IE denote the domain of flow event structures. The components of a flow event structure E ∈ IE will be denoted by E_{E}, ≺_{E} and #_{E} — a convention that will also apply to other structures given as tuples. If clear from the context, the index E will be omitted. O denotes the empty flow event structure (∅, ∅, ∅).

The interpretation of the conflict and the flow relation is formalised by defining which subsets of events constitute possible runs of the represented system, and which of these runs terminate successfully.^{2} These subsets are called configurations (terminated configurations, resp.). Since in Section 4 we will introduce weaker notions of configuration, we will call these original configurations strong.

Definition 1.2 Let E ∈ IE.

(i) X ⊆ E is cycle-free in E iff (≺ ∩(X × X))^{+} (where ^{+} denotes transitive closure) is irreflexive. X ⊆ E is conflict-free in E iff # ∩ (X × X) = ∅.

(ii) X ⊆ E is a (strong) configuration of E iff X is finite, cycle-free, conflict-free and (strongly) left-closed up to conflicts: ∀d, e ∈ E : if e ∈ X, d ≺ e and d ∉ X then there exists an f ∈ X with d#f and f ≺ e.

A configuration X is called terminated iff ∀d ∈ E : d ∉ X ⇒ ∃e ∈ X with d#e. Conf (E) denotes the set of all configurations of E, and √(E) the set of all terminated configurations of E.

2As explained in [GG], the notion of successful termination is necessary for dealing with event refinement.

In [GG] we have shown that the notion of successful termination derived from the structural properties of flow event structures in the above definition is compatible with our notions of event refinement and sequential composition.

The behaviour of a flow event structure may be expressed in terms of a general and more abstract event oriented model of concurrent systems, in which a system is represented merely by its set of configurations and a termination predicate.

Definition 1.3 [GG]

(i) A configuration structure is a pair C = (C, √) where C is a family of finite sets (the configurations) and √ ⊆ C a termination predicate, satisfying X ∈ √ ∧ X ⊆ Y ∈ C_{C} ⇒ X = Y (i.e. terminating configurations must be maximal).

(ii) The configuration structure of E ∈ IE is defined as C(E) := (Conf (E), √(E)).

The set E_{C} of events of a configuration structure C is defined by E_{C} := ⋃_{X∈C_{C}} X.

Next we define the parallel product E × F as in [CZ] for flow event structures E and F. It represents the independent execution of events of E and F, where moreover each pair of events of d ∈ E and e ∈ F may synchronise (thereby excluding the independent occurrence of e and f and their synchronisation with other events).

Definition 1.4 Let E, F ∈ IE.

(i) The (partially synchronous) parallel product E × F is defined by – E_{E×F} = (E_{E} × {∗}) ∪ ({∗} × E_{F}) ∪ (E_{E} × E_{F}),

– (d, d′) ≺_{E×F} (e, e′) iff d ≺_{E} e or d′ ≺_{F} e′,

– (d, d′) #_{E×F} (e, e′) iff d #_{E} e or d′ #_{F} e′ or

(d = e ≠ ∗ ∧ d′ ≠ e′) or (d′ = e′ ≠ ∗ ∧ d ≠ e).

(ii) For any set X ⊆ E_{E×F} of events in E × F, we define the projections

\begin{matrix}π_{1}(X) := \{e ∈ E_{E} | ∃e′ ∈ E_{F} ∪ \{∗\} : (e, e′) ∈ X\} and \\ π_{2}(X) := \{e′ ∈ E_{F} | ∃e ∈ E_{E} ∪ \{∗\} : (e, e′) ∈ X\}. \end{matrix}

In the next section we will see that this definition does not always match the informal description of parallel product above.

Refinement of events in a flow event structure E may now be defined as follows (cf. [GG]). We assume a refinement function ref : E_{E} → IE −{O} mapping events to non-empty flow event structures, and replace each event e by a disjoint copy of ref (e). The conflict and causality structure will just be inherited.

Definition 1.5 Let E ∈ IE and let ref : E_{E} → IE − {O}.

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(e)}},

– (d, d′) ≺_{ref(E)} (e, e′) iff d ≺_{E} e or (d = e ∧ d′ ≺_{ref(d)} e′),

– (d, d′) #_{ref(E)} (e, e′) iff d #_{E} e or (d = e ∧ d′ #_{ref(d)} e′).

Sometimes we specify ref (e) only for certain events e. In this case we assume ref (e) = e for all other events e. As for most applications it is sufficient to consider flow event structures up to isomorphism, i.e. abstracting from the names of events, we will sometimes simplify the names of events in examples.

2 Requirements for well-behaved flow event structures

In our understanding, a run of the parallel product of two event structures ought to be composed of runs of its components. Therefore we expect that the projections of configurations of product event structures E × F are themselves configurations. The following example shows that for arbitrary flow event structures this is not the case.

Example 2.1

Consider the flow event structures E := \begin{matrix}b \overline{}− c \overline{}− d \\ # \\ a \end{matrix} and F := e \overline{}− f .

It is easy to verify that {(a, e), (c, f)} ∈ Conf (E ×F), although π_{1}({(a, e), (c, f)}) =

{a, c} ∉ Conf (E).

Castellani and Zhang [CZ] define a subclass of flow event structures where this problem does not occur. It consists of those flow event structures satisfying the so-called Δ-axiom.

Axiom Δ: a#b ≺ c ∧ a ≁ c ⇒ ∃d : b#d ≺ c ∧ ∀e#d : (e ≠ b ⇒ b#e ∼ c).

Here e ∼ e′ abbreviates e#e′ ∨ e ≺ e′ ∨ e′ ≺ e. The work of [CZ] implies that on this class parallel product is well-behaved in the sense that the projections of configurations of product event structures are themselves configurations, i.e. the problem illustrated in Example 2.1 does not occur. They also show that this class is closed under all operators of CCS as defined in [BC-a]. However, this class is not closed under our refinement operator.

Example 2.2

Refining b into \begin{matrix}b_{1} \\ b_{2} \end{matrix} in [figure: a; #; b; #; d; c] yields[figure: a; #; #; b_{1}; #; b_{2}; #; d; c]. The former structure satisfies

Δ, by lack of events e ≠ b with e#d. However, the latter does not: take b := b_{2} and e := b_{1}; then b_{2}#b_{1} fails to hold.^{3}

We will show that this problem can be solved by regarding a different subclass of flow event structures, closed under event refinement and parallel product, for which parallel product is still well-behaved. In the remainder of this section we will expand on the requirements to be imposed on such a class. In Section 4 we will propose two classes meeting these requirements, one of which will contain the class from [CZ], i.e. all flow event structures satisfying Δ.

3When labelling event a with a, b with τ, c with c and d with \overline{a}, the original event structure can be denoted by the CCS-expression a | \overline{a}.c.nil. Hence, excluding this event structure from consideration by strengthening the Δ-axiom is not an option.

2.1 Closure requirements

We require a suitable class of flow event structure to be closed under parallel product and event refinement. This implies that the corresponding class of labelled flow event structures will be closed under Winskel’s parameterised parallel composition operator and under action refinement, which are the labelled counterparts of parallel product and event refinement. The process algebraic operators choice, sequential composition, restriction and renaming can easily be expressed in terms of action refinement. Furthermore, the parallel composition operators from CCS, CSP, SCCS, ACP and many other system description languages can be expressed in terms of Winskel’s parallel composition, restriction and renaming. In particular, all CCS operators as defined in [BC-a] can be expressed in terms of parallel composition and action refinement. Hence a suitable class of flow event structures will also be closed under all those operators.

2.2 Parallel product should be well-behaved

We propose to formulate the requirement of non-occurrence of the problem illustrated in Example 2.1 on a subclass of flow event structures as follows.

Definition 2.1 Let IE′ ⊆ IE be a class of flow event structures.

Parallel product is said to be well-behaved on IE′ iff for every E, F ∈ IE′ and X ∈ Conf (E × F) we have π_{1}(X) ∈ Conf (E) and π_{2}(X) ∈ Conf (F).

2.3 Compositionality

An operator f on a model of concurrency is said to be compositional with respect to a certain notion of behaviour if the behaviour of an application of f is completely determined by the behaviour of its arguments. For an n-ary operator f on flow event structures this means that C(f(E_{1}, …, E_{n})) is derivable from C(E_{1}), …, C(E_{n}).

Definition 2.2

An operator f : IE^{n} → IE is called compositional iff there exists an n-ary operation on configuration structures f_{C} such that C(f(E_{1}, …, E_{n})) = f_{C}(C(E_{1}), …, C(E_{n})).

If f is compositional then C(E_{i}) = C(E′_{i}) for all i = 1, …, n implies C(f(E_{1}, …, E_{n})) = C(f(E′_{1}, …, E′_{n})).

We require that the process algebraic operators discussed in Section 2.1 are compositional on our subclass of flow event structures. As all these operators are expressible in terms of parallel composition and action refinement, which are the labelled counterparts of parallel product and event refinement, it suffices to establish compositionality for the latter.

In [GG], compositionality for action refinement on the class of all flow event structures has been established by showing that C(ref (E)) = ref_{C}(C(E)), where ref_{C} is the refinement operator on configuration structures of [GG] induced by the refinements ref_{C}(e) := C(ref (e)) for e ∈ E_{E}. This result may be immediately transferred to event refinement and is inherited when taking subclasses of flow event structures.

However, for parallel product compositionality turns out to fail. The anomaly of Example 2.1 can be used to show that × is not compositional on IE.

Example 2.1 (continued)

Let E′ = [figure: b; c; d; #; #; a; .; .; .; .] . Then C(E) = C(E′). However C(E × F) ≠ C(E′ × F),

since {(a, e), (c, f)} ∉ Conf (E′). The rôle of d in this example is to ensure that √(E) = √(E′).

In Section 3 we will show that well-behavedness of parallel product on a subclass of flow event structures guarantees its compositionality.

2.4 Parallel product as a categorical product

In [CZ] a notion of morphism between flow event structures is defined, making the class of flow event structures into a category. Following [Winskel], they would like the parallel product × to be the categorical product in this category. For this it is, by definition, necessary that × is well-behaved in the sense of Definition 2.1. Example 2.1 shows that on the class of all flow event structures this is not the case. However, they prove that on the subclass of flow event structures satisfying the Δ-axiom × is the categorical product.

Interestingly, the only part of their proof using the Δ-axiom is where they show that the projections of configurations of product event structures E × F are themselves configurations. Hence their result can be partitioned in two parts: × is well-behaved on the class of flow event structures satisfying Δ, and for any class of flow event structures on which × is well-behaved this operator is in fact the categorical product. Thus the requirement that on a subclass of flow event structures × is the categorical product w.r.t. the morphisms of [CZ] is equivalent to the requirement that on this subclass × is well-behaved.

3 Compositionality

Let IE′ be any class of flow event structures on which parallel product is well-behaved. In this section we establish the compositionality of parallel product on IE′ by defining a counterpart of this operator on the model of configuration structures.

Definition 3.1 Let C and D be configuration structures.

The parallel product C × D is defined by

X ∈ C_{C×D} ⇔ \begin{cases}X ⊆ (E_{C} × \{∗\}) ∪ (\{∗\} × E_{D}) ∪ (E_{C} × E_{D}) \\ π_{1}(X) ∈ C_{C} and π_{2}(X) ∈ C_{D} \\ (d, d′), (e, e′) ∈ X ⇒ \begin{cases}(d = e ≠ ∗) ⇒ d′ = e′ \\ (d′ = e′ ≠ ∗) ⇒ d = e. \end{cases} \end{cases}

X ∈ √_{C×D} ⇔ X ∈ C_{C×D} ∧ π_{1}(X) ∈ √_{C} ∧ π_{2}(X) ∈ √_{D}.

Here π_{1}(X) := {e ∈ E_{C} | ∃e′ ∈ E_{D} ∪ {∗} : (e, e′) ∈ X}
and π_{2}(X) := {e′ ∈ E_{D} | ∃e ∈ E_{C} ∪ {∗} : (e, e′) ∈ X}.

The operator × defined above agrees with the categorical product ×_{F} defined in [Winskel] on a category of families of configurations, which are special kinds of configuration structures without termination predicate. It is also similar to the parallel product of [PP], defined on event automata, which can be regarded as generalisations of configuration structures without termination predicate.

The parallel product defined above does not quite qualify as the operation ×_{C} required by Definition 2.2, for it may introduce “unreachable” configurations, whereas such configurations never occur in configuration structures of flow event structures (as we will show in Proposition 3.1). Semantically these unreachable configurations are unimportant; virtually all semantic equivalences on configuration structures proposed in the literature identify structures that differ only in their unreachable part. Hence, using the parallel product of Definition 3.1 we could prove compositionality “up to” such a semantic equivalence. However, as we do not want to deal with equivalence notions here, we will use a modified version of parallel product on configuration structures which excludes unreachable configurations.

Definition 3.2 Let C be a configuration structure and X ∈ C_{C}.

X is reachable iff there are X_{0}, ..., X_{n} ∈ C_{C} with ∅ = X_{0} ⊂ X_{1} ⊂ ⋯ ⊂ X_{n} = X and ∀i < n : |X_{i+1} − X_{i}| = 1. Let R(C_{C}) be the set of reachable configurations of C. The reachable part R(C) of C is given by R(C) := (R(C_{C}), √_{C} ∩ R(C_{C})). C is connected iff all its configurations are reachable, i.e. if R(C) = C.

Observation 1 A configuration structure C is connected iff for every X ∈ C_{C} with X ≠ ∅ there is a g ∈ X such that X − {g} ∈ C_{C}.

For configuration structures C and D let C ×_{R} D be defined as R(C × D). The operator ×_{R} has been defined inductively in [Costantini]. We will show that for well-behaved flow event structures E and F one has C(E × F) = C(E) ×_{R} C(F), thereby establishing the compositionality of parallel product for well-behaved flow event structures. We start by showing that the configuration structures of flow event structures are always connected.

Proposition 3.1 Let E ∈ IE.

Then C(E) is connected, i.e. R(C(E)) = C(E).

Proof Let E ∈ IE and ∅ ≠ X ∈ Conf (E). As X is cycle-free there must be a g ∈ X that is maximal in X w.r.t. ≺. By Observation 1 it suffices to show that X − {g} ∈ Conf (E).

Finiteness, cycle-freeness and conflict-freeness of X − {g} follow from the same properties of X. Let d ≺ e ∈ X − {g} and d ∉ X − {g}. As g is maximal in X we have d ≠ g. Because X is left-closed up to conflicts ∃f ∈ X : d#f ≺ e. As g is maximal in X we have f ≠ g, i.e. f ∈ X − {g}. Thus X − {g} is left-closed up to conflicts.

Notation For configuration structures C and D we write C ⊆ D for C_{C} ⊆ C_{D} ∧√_{C} ⊆ √_{D}.

Observation 2 If C ⊆ D then R(C) ⊆ R(D).

Now the desired compositionality result falls apart in two directions. We start by showing that C(E ×F) ⊆ C(E)×_{R} C(F), the only direction in which it is used that parallel product is well-behaved on IE′.

Lemma 3.1 Let E, F ∈ IE′.
Then C(E × F) ⊆ C(E) × C(F).

Proof We must show that Conf (E × F) ⊆ C_{C(E)×C(F)} and √(E × F) ⊆ √_{C(E)×C(F)}.

Let X ∈ Conf (E × F). We show that X ∈ C_{C(E)×C(F)}, according to Definition 3.1.

• As × is well-behaved on IE′, π_{1}(X) ∈ Conf (E) = C_{C(E)} and π_{2}(X) ∈ Conf (F) = C_{C(F)}.

• By Definition 1.4 we have X ⊆ E_{E×F} = (E_{E} ×{∗})∪({∗}×E_{F})∪(E_{E} ×E_{F}). That we even have X ⊆ (E_{C(E)} ×{∗})∪({∗}×E_{C(F)})∪(E_{C(E)} ×E_{C(F)}), i.e. the first requirement of Definition 3.1, now follows from the second requirement of Definition 3.1 established above.

• Suppose (d, d′), (e, e′) ∈ X and (d = e ≠ ∗), but d′ ≠ e′. Then (d, d′) # (e, e′), contradicting the conflict-freeness of X. The other condition follows by symmetry.

Now let X ∈ √(E × F). Then surely X ∈ Conf (E × F) ⊆ C_{C(E)×C(F)}. According to Definition 3.1 is remains to be be shown that π_{1}(X) ∈ √_{C(E)} and π_{2}(X) ∈ √_{C(F)}. Let ∗ ≠ d ∉ π_{1}(X). Then (d, ∗) ∉ X. So ∃(e, e′) ∈ X with (d, ∗) # (e, e′). Now e ∈ π_{1}(X) ∪ {∗}. Hence e ≠ d, so d#e ≠ ∗. Thus π_{1}(X) ∈ √_{C(E)}. That π_{2}(X) ∈ √_{C(F)} follows by symmetry.

Corollary 3.1 Let E, F ∈ IE′.
Then C(E × F) ⊆ C(E) ×_{R} C(F).

Proof C(E ×F) =^{Prop. 3 .1} R(C(E ×F)) ⊆^{Lemma 3 .1 , Obs. 2}R(C(E)×C(F)) =^{def .} C(E) ×_{R} C(F).

Clearly, the restriction to the reachable part is not needed for the direction of the compositionality result established above. For the other direction, it is only needed because of the requirement of cycle-freeness of configurations. We now proceed by dropping this requirement as an intermediate step.

Definition 3.3 Let E ∈ IE.

X ⊆ E is a possibly cyclic configuration of E iff X is finite, conflict-free and leftclosed up to conflicts. Such a configuration is called terminated iff ∀d ∈ E : d ∉ X ⇒ ∃e ∈ X with d#e. Conf^{∘}(E) denotes the set of all possibly cyclic configurations of E, and √^{∘}(E) the set of all terminated ones. Furthermore, let C^{∘}(E) := (Conf^{∘}(E), √^{∘}(E)).

Lemma 3.2 Let E, F ∈ IE.

Then C(E) × C(F) ⊆ C^{∘}(E × F).

Proof Let X ∈ C_{C(E)×C(F)}. We show that X ∈ Conf^{∘}(E × F).

• X is finite, since π_{1}(X) and π_{2}(X) are finite.

• X is conflict-free, due to the last requirement for X ∈ C_{C(E)×C(F)} of Definition 3.1 and the conflict-freeness of π_{1}(X) and π_{2}(X).

• Let (d, d′) ≺ (e, e′) ∈ X and (d, d′) ∉ X. Then either d ≺ e or d′ ≺ e′, say d ≺ e. In particular d, e ≠ ∗. We have e ∈ π_{1}(X) ∈ Conf (E). There are two possibilities for d:

– d ∉ π_{1}(X). Then ∃f ∈π_{1}(X) : d#f ≺ e. So ∃(f, f′)∈X : (d, d′)#(f, f′)≺(e, e′).

– d ∈ π_{1}(X). Then ∃(d, d′′) ∈ X. Hence d′ ≠ d′′. We have (d, d′) # (d, d′′) ≺ (e, e′).

Hence X is left-closed up to conflicts.

Now let X ∈ √_{C(E)×C(F)}. We show that X ∈ √^{∘}(E × F).

Let (d, d′) ∈ E_{E×F} with (d, d′) ∉ X. Then either d ≠ ∗ or d′ ≠ ∗, say d ≠ ∗. Again there are two possibilities for d:

– d ∉ π_{1}(X). As π_{1}(X) ∈ √_{C(E)} there must be an e ∈ π_{1}(X) with d#e. Hence

∃(e, e′) ∈ X with (d, d′) # (e, e′).

– d ∈ π_{1}(X). Then ∃(d, d′′) ∈ X. Hence d′ ≠ d′′. We have (d, d′) # (d, d′′).

Hence X is terminating.

The following lemma shows that for possibly cyclic configurations of flow event structures the requirements cycle-free and reachable are equivalent.

Lemma 3.3 Let E ∈ IE.
Then R(C^{∘}(E)) = C(E).

Proof “⊇”: By definition C(E) ⊆ C^{∘}(E), so by Proposition 3.1 and Observation 2 C(E) = R(C(E)) ⊆ R(C^{∘}(E)).

“⊆”: Let X ∈ R(C^{∘}(E)). It suffices to show that X is cycle-free. Suppose X contains a cycle: ∃e_{1}, …, e_{k+1} ∈ X (k > 1) with e_{1} ≺ e_{2} ≺ … ≺ e_{k+1} = e_{1}. As X is reachable ∃X_{0}, ..., X_{n} ∈ C_{C^{∘}(E)} with ∅ = X_{0} ⊂ X_{1} ⊂ ⋯ ⊂ X_{n} = X and ∀i < n : |X_{i+1} − X_{i}| = 1. Let i < n be such that X_{i+1} ⊇ {e_{1}, …, e_{k}} and e_{j} ∉ X_{i} for a certain j ∈ {1, …, k}. As e_{j} ≺ e_{j+1} ∈ X_{i} ∈ C_{C^{∘}(E)} there must be an f ∈ X_{i} ⊂ X_{i+1} with e_{j}#f ≺ e_{j+1}. So f, e_{j} ∈ X_{i+1}, contradicting the conflict-freeness of X_{j+1}.

Corollary 3.2 Let E and F be arbitrary flow event structures.
Then C(E × F) ⊇ C(E) ×_{R} C(F).

Proof C(E) ×_{R} C(F) =^{def .} R(C(E)×C(F)) ⊆^{Lemma 3 .2 , Obs. 2}R(C^{∘}(E×F)) =^{Lemma 3 .3} C(E×F).

Together, Corollaries 3.1 and 3.2 say that parallel product is compositional on any class of flow event structures on which parallel product is well-behaved.

4 Well-behaved flow event structures

In this section we define two subclasses of flow event structures, both satisfying the requirements of Section 2. To this end we define two notions of configuration for flow event structures, the weak and the fairly weak configurations,^{4} that are more liberal than the standard notion of Definition 1.2. The two subclasses of flow event structures will be the classes on which the weak, resp. the fairly weak, notion of configuration coincides with the standard one. The larger class, using fairly weak configurations, contains all flow event structures satisfying Δ.

Definition 4.1 Let E ∈ IE.

X ⊆ E is a [fairly] weak configuration of E iff X is finite, cycle-free, conflict-free and [fairly] weakly left-closed up to conflicts: ∀d, e ∈ E : if e ∈ X, d ≺ e and d ∉ X then there exists an f ∈ X with d#f [and ¬(e ≺ f)]. Such a configuration is called terminated iff ∀d ∈ E : d ∉ X ⇒ ∃e ∈ X with d#e. Conf_{w}(E) [resp. Conf_{fw}(E)] denotes the set of all [fairly] weak configurations of E, and √_{w}(E) [resp. √_{fw}(E)] the set of all terminated [fairly] weak configurations of E. The [fairly] weak configuration structure of E is C_{[f]w}(E) := (Conf_{[f]w}(E), √_{[f]w}(E)).

Observation 3 Note that every strong configuration is certainly fairly weak, and every fairly weak configuration is certainly weak.

On the other hand, in Example 2.1 the set of events {a, c} constitutes a [fairly] weak

configuration of E but not a strong one. Furthermore, in G = [figure: b; #; c; a] the set of events

{a, c} constitutes a weak configuration but not a fairly weak one.

Definition 4.2

A flow event structure is called [fairly] well-behaved iff all its [fairly] weak configurations are strong.

Note that well-behaved flow event structures are certainly fairly well-behaved. The structure G above is fairly well-behaved, but not well-behaved. The structure E of Example 2.1 is not even well-behaved.

In the remainder of this section we will show that

• the classes of [fairly] well-behaved flow event structures are closed under event refinement and parallel product,

• parallel product is well-behaved on these classes,

• flow event structures satisfying the Δ-axiom are fairly well-behaved.

4We will put the material on fairly weak configurations and the related subclass in square brackets.

The structure G on the previous page satisfies the Δ-axiom. Hence, flow event structures satisfying the Δ-axiom are not always well-behaved.

First we establish that the classes of [fairly] well-behaved flow event structures are closed under event refinement. To this end, we show that the appropriate projections of the [fairly] weak configurations of refined flow event structures are themselves [fairly] weak configurations.

Notation Let E ∈ IE and let ref : E_{E} → IE − {O}.

For any set X ⊆ E_{ref (E)} of events in ref (E), define the projections

π_{1}(X) := {e | ∃f : (e, f) ∈ X} and π_{2}^{e}(X) := {f | (e, f) ∈ X}.

Now X can be written as X = ⋃_{e∈π_{1}(X)} {e} × π_{2}^{e}(X).

Proposition 4.1 Let E ∈ IE, let ref : E_{E} → IE − {O} and let X ∈ Conf_{[f]w}(ref (E)).

(i) π_{1}(X) ∈ Conf_{[f]w}(E),

(ii) π_{2}^{e}(X) ∈ Conf_{[f]w}(ref (e)) for all e ∈ π_{1}(X),

(iii) π_{2}^{e}(X) ∈ √_{[f]w}(ref (e)) when e not maximal in π_{1}(X) w.r.t. ≺.

Proof

(i) That π_{1}(X) is finite, cycle-free and conflict free follows from the corresponding properties of X. We show that π_{1}(X) is [fairly] weakly left-closed up to conflicts.

Let e ∈ π_{1}(X), d ∈ E_{E} with d ≺_{E} e and d ∉ π_{1}(X). We have to show that there exists an f ∈ π_{1}(X) with f#_{E}d [and ¬(e ≺_{E} f)]. Since e ∈ π_{1}(X) there must be some (e, e′) ∈ X. There exists (d, d′) ∈ E_{ref(E)}, (d, d′) ∉ X since ref (d) ≠ O and d ∉ π_{1}(X). Furthermore (d, d′) ≺_{ref(E)} (e, e′) since d ≺_{E} e. So there exists (f, f′) ∈ X with (f, f′)#_{ref (E)}(d, d′) [and ¬((e, e′) ≺_{ref (E)} (f, f′))]. f ≠ d since f ∈ π_{1}(X), d ∉ π_{1}(X); hence f#_{E}d. [As ¬((e, e′) ≺_{ref (E)} (f, f′)) we cannot have e ≺_{E} f and we are done.]

(ii) Let e ∈ π_{1}(X). Obviously π_{2}^{e}(X) ⊆ E_{ref (e)}. π_{2}^{e}(X) is finite, cycle-free and conflict-free since X is finite, cycle-free and conflictfree. We show that π_{2}^{e}(X) is [fairly] weakly left-closed up to conflicts.

Let d′ ∈ E_{ref (e)}, d′ ≺_{ref (e)} e′ ∈ π_{2}^{e}(X), d′ ∉ π_{2}^{e}(X). Then (e, d′) ∈ E_{ref(E)}, (e, d′) ≺_{ref(E)} (e, e′) ∈ X and (e, d′) ∉ X. So there exists (f, f′) ∈ X with (f, f′)#_{ref(E)}(e, d′) [and ¬((e, e′) ≺_{ref(E)} (f, f′))]. As f, e ∈ π_{1}(X) we have ¬(f#_{E}e), so f = e ∧ f′#_{ref (e)}d′. Thus f′ ∈ π_{2}^{e}(X) [and ¬(e′ ≺_{ref (e)} f′)].

(iii) Suppose e is not maximal in π_{1}(X). Then there exists f ∈ π_{1}(X) with e ≺_{E} f, so there is an (f, f′) ∈ X. Let d′ ∈ E_{ref (e)} − π_{2}^{e}(X). We have (e, d′) ≺_{ref (E)} (f, f′) and (e, d′) ∉ X. Since X is a [fairly] weak configuration, there exists (g,g′)∈X with (g,g′)#_{ref (E)}(e,d′). As g, e ∈ π_{1}(X), we have ¬(g#_{E}e). Hence g = e, g′ ∈ π_{2}^{e}(X) and g′#_{ref (e)}d′.

Theorem 4.1

Let E ∈ IE be [fairly] well-behaved and ref : E_{E} → IE − {O} such that ref (e) is [fairly] well-behaved for all e ∈ E_{E}. Then ref (E) is [fairly] well-behaved, i.e. Conf_{[f]w}(ref (E)) = Conf (ref (E)).

Proof Let X ∈ Conf_{[f]w}(ref (E)). We have to show that X is (strongly) left-closed up to conflicts. Let (d, d′) ≺ (e, e′) ∈ X and (d, d′) ∉ X. There are three cases to consider.

• Suppose d ≺ e and d ∉ π_{1}(X). We have π_{1}(X) ∈ Conf_{[f]w}(E) = Conf (E) by Proposition 4.1(i). Hence ∃f ∈ π_{1}(X) such that d#f ≺ e. So ∃(f, f′) ∈ X. It follows that (d, d′)#(f, f′) ≺ (e, e′).

• Suppose d ≺ e and d ∈ π_{1}(X). We have d′ ∉ π_{2}^{d}(X) ∈ √_{[f]w}(ref (d)) = √(ref (d)) by Proposition 4.1(iii). Hence ∃d′′ ∈ π_{2}^{d}(X) such that d′#d′′. So (d, d′′) ∈ X. It follows that (d, d′)#(d, d′′) ≺ (e, e′).

• Suppose d = e and d′ ≺ e′. We have d′ ∉ π_{2}^{e}(X) ∈ Conf_{[f]w}(ref (e)) = Conf (ref (e)) by Proposition 4.1(ii). Hence ∃f′ ∈ π_{2}^{e}(X) such that d′#f′ ≺ e′. So (e, f′) ∈ X. It follows that (e, d′)#(e, f′) ≺ (e, e′).

Next we establish that the classes of [fairly] well-behaved flow event structures are closed under parallel product. We first show that the projections of the [fairly] weak configurations of the product of two flow event structures are themselves [fairly] weak configurations.

Proposition 4.2 Let E, F ∈ IE and X ∈ Conf_{[f]w}(E × F).
Then π_{1}(X) ∈ Conf_{[f]w}(E) and π_{2}(X) ∈ Conf_{[f]w}(F).

Proof We show that π_{1}(X) ∈ Conf_{[f]w}(E); then π_{2}(X) ∈ Conf_{[f]w}(F) follows by symmetry. As X is finite, cycle-free and conflict-free, so is π_{1}(X). Suppose d ≺ e ∈ π_{1}(X) and ∗ ≠ d ∉ π_{1}(X). Then ∃(e, e′) ∈ X, whereas (d, ∗) ∉ X. Moreover (d, ∗) ≺ (e, e′). Thus ∃(f, f′) ∈ X : (d, ∗) # (f, f′) [and ¬((e, e′) ≺ (f, f′))]. Now f ∈ π_{1}(X) ∪ {∗}, so f ≠ d. It must be that f ≠ ∗ and d # f, since (d, ∗) # (f, f′). [In case e ≺ f we would have (e, e′) ≺ (f, f′).] Thus π_{1}(X) is [fairly] weakly left-closed up to conflicts.

Example 2.1 shows that Proposition 4.2 does not hold for strong configurations.

Theorem 4.2 Let E, F ∈ IE be [fairly] well-behaved.

Then E × F is [fairly] well-behaved, i.e. Conf_{[f]w}(E × F) = Conf (E × F).

Proof Let X ∈ Conf_{[f]w}(E × F). We have to show that X is (strongly) left-closed up to conflicts. Let (d, d′) ≺ (e, e′) ∈ X and (d, d′) ∉ X. Then either d ≺ e or d′ ≺ e′, say d ≺ e (so d, e ≠ ∗). By Proposition 4.2 and the well-behavedness of E we have π_{1}(X) ∈ Conf_{[f]w}(E) = Conf (E). There are two cases to consider.

• Suppose d ∉ π_{1}(X). Then ∃f ∈ π_{1}(X) with d#f ≺ e. Thus ∃(f, f′) ∈ X. We have (d, d′)#(f, f′) ≺ (e, e′).

• Suppose d ∈ π_{1}(X). Then ∃(d, d′′) ∈ X. Using Definition 1.4 we have (d, d′)#(d, d′′) ≺ (e, e′).

As an immediate consequence of Proposition 4.2 we obtain the result that parallel product is well-behaved on the classes of [fairly] well-behaved flow event structures.

Theorem 4.3 Let E, F ∈ IE be [fairly] well-behaved and X ∈ Conf (E × F).
Then π_{1}(X) ∈ Conf (E) and π_{2}(X) ∈ Conf (F).

Proof Let E, F ∈ IE be [fairly] well-behaved and X ∈ Conf (E × F) ⊆^{Observation 3} Conf_{[f]w}(E × F). With Proposition 4.2 and the [fairly] well-behavedness of E and F we obtain π_{1}(X) ∈ Conf_{[f]w}(E) = Conf (E) and π_{2}(X) ∈ Conf_{[f]w}(F) = Conf (F)).

Finally, we show that flow event structures satisfying the Δ-axiom are fairly well-behaved.

Theorem 4.4 Let E ∈ IE.

If E satisfies Δ then E is fairly well-behaved.

Proof Let E satisfy Δ. Let X be a fairly weak configuration of E. We show that X is strong. It suffices to show that X is strongly left closed up to conflicts. Suppose b ≺ c ∈ X, b ∉ X. We have to show that there exists an f ∈ X with f#b and f ≺ c. As X is fairly weakly left closed up to conflicts, there is an a ∈ X with a#b and ¬(c ≺ a). In case a ≺ c, we take f = a. Otherwise, there exists a d as required by the Δ-axiom (a ≁ c since a, c ∈ X and ¬(c ≺ a)). If d ∈ X we take f = d. Otherwise, as X is fairly weakly left closed up to conflicts and d ≺ c ∈ X, d ∉ X, there must be an f ∈ X with f#d and ¬(c ≺ f). As b ∉ X we have f ≠ b. Since ¬(c ≺ f), ¬(c#f) (c,f in configuration X), the Δ-axiom yields b#f ≺ c.

5 Concluding remark

We have proposed two subclasses of flow event structures which are suitable for modelling parallel composition, action refinement and many other operators of CCS-like languages. These classes consist of those flow event structures on which the traditional “strong” notion of configuration agrees with a new, “weak” or “fairly weak”, one. When restricting attention to these classes, the notion of configuration for flow event structures could just as well be defined to be the weak or the fairly weak one; the classes could then be defined with the auxiliary notion of a strong configuration.

As flow event structures have been introduced precisely for their suitability in giving semantics to CCS-like languages, and the flow event structures equipped with the strong notion of configuration have been shown to fail for this purpose outside our classes, it can be argued that the strong notion of configuration has no particular advantages over the weak or fairly weak one. Instead one may wonder whether the weak or the fairly weak notion of configuration, or variants thereof, may be useful outside our classes. We leave this as a question for future research.

Acknowledgment

Arend Rensink challenged our original believe that the Δ-axiom would be preserved under action refinement in flow event structures and helped us find Counterexample 2.2.

References

[BC-a] G. Boudol & I. Castellani (1989): Permutation of transitions: an event structure semantics for CCS and SCCS. In J.W. de Bakker, W.P. de Roever & G. Rozenberg, editors: REX School and Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Noordwijkerhout, The Netherlands, May/June 1988, LNCS 354, Springer, pp. 411–427.

[BC-b] G. Boudol & I. Castellani (1994): Flow models of distributed computations: Three equivalent semantics for CCS. Information and Computation 114, pp. 247–314.

[CZ] I. Castellani & G.Q. Zhang (1997): Parallel product of event structures. Theoretical Computer Science 179, pp. 203–215.

[Costantini] R. Costantini (1995): Abstraktion in ereignisbasierten Modellen verteilter Systeme. Dissertation, Univ. Hildesheim. Verlag Dr. Kovaĉ.

[DD] Ph. Darondeau & P. Degano (1993): Refinement of actions in event structures and causal trees. Theoretical Computer Science 118, pp. 21–48.

[GG] R.J. van Glabbeek & U. Goltz (2001): Refinement of actions and equivalence notions for concurrent systems. Acta Informatica 37, pp. 229–327.

[NPW] M. Nielsen, G.D. Plotkin & G. Winskel (1981): Petri nets, event structures and domains, part I. Theoretical Computer Science 13(1), pp. 85–108.

[PP] G.M. Pinna & A. Poigné (1995): On the nature of events: another perspective in concurrency. Theoretical Computer Science 138(2), pp. 425–454.

[Winskel] G. Winskel (1987): Event structures. In W. Brauer, W. Reisig & G. Rozenberg, editors: Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, Bad Honnef, September 1986, LNCS 255, Springer, pp. 325–392.