Bundle Event Structures and CCSP^{⋆}

Rob van Glabbeek^{1} and Frits Vaandrager^{2}

1 National ICT Australia

School of Computer Science & Engineering, Univ. of New South Wales, Sydney 2052, Australia

                          rvg@cs.stanford.edu

2 Nijmegen Institute for Computing and Information Sciences, University of Nijmegen Postbus 9010, 6500 GL Nijmegen, The Netherlands

                            fvaan@cs.kun.nl

Abstract. We investigate which event structures can be denoted by means of closed CCS ∪ CSP expressions. Working up to isomorphism we find that

• all denotable event structures are bundle event structures,

• upon adding an infinitary parallel composition all bundle event structures are denotable,

• without it every finite bundle event structure can be denoted,

• as well as every countable prime event structure with binary conflict.

Up to hereditary history preserving bisimulation equivalence finitary conflict can be expressed in terms of binary conflict. In this setting all countable stable event structures are denotable.

Introduction

In concurrency theory many languages for the representation of concurrent systems have been proposed, including CCS, SCCS, CSP, Meije, ACP, COSY and LOTOS, all in several variations. Although most of these languages were originally equipped with an interleaving semantics, concurrency respecting interpretations have been proposed by various authors, using semantical models like Petri nets, event structures, transition systems—optionally with additional structure to represent causal independence—, causal trees, families of posets, etc. In recent years it has been established that there are canonical translations between most of these models, thereby making them into different representations of one and the same semantic concept [13, 17, 2, 19, 6]. In addition, the languages mentioned above are to a large extent intertranslatable, and can be regarded as dialects of one and the same system specification language.

This paper deals with the question which of these unified semantic objects can be denoted by closed expressions in this unified language. As a representative semantic model we take the event structures from Winskel [17]. Our findings can then be transmitted to other models by means of the canonical translations found in the literature. As a representative language we combine some operators from CCS [12] and CSP [3,

⋆ To appear in: Proceedings 14th International Conference on Concurrency Theory (CONCUR 2003), Marseille, France, LNCS, Springer, September 2003. \begin{matrix}c \\ ◯ \end{matrix} Springer-Verlag 1 This work was performed in part while the first author was employed at Stanford University. It was supported by ONR under grant number N00014-92-J-1974.

9]. Following a suggestion of Mogens Nielsen, such a combination is called CCSP. Our version of CCSP is sufficiently expressive to emulate most constructions from other languages found in the literature, including the ones provided with an event structure semantics in [17]. The chosen combination of operators appears to be optimal for carrying out the constructions in this paper. However, many other combinations would lead to the same results.

In [17] the subclass of stable event structures is defined, as well as the further subclass of prime event structures. In [18] a subclass of event structures with a binary conflict relation is proposed (see Figure 1 below). The prime event structures with binary conflict are exactly the (finitary) event structures originally introduced in [13]. It is well known that unstable event structures cannot be represented in CCSP-like languages in a causality respecting way. It is an interesting quest to extend such languages with novel operators that make this possible. This quest is not pursued here; we will be happy to just find out which of the stable event structures are denotable.

It is unreasonable to expect to find a CCSP expression denoting a given event structure exactly. Hence we will try to find for any given stable event structure a CCSP expression whose denotation as event structure is semantically equivalent. This makes our quest parametrised by the choice of a suitable semantic equivalence. We consider three choices for this parameter: isomorphism, history preserving bisimulation equivalence and (in this introduction only) ST-bisimulation equivalence.

Denotability up to isomorphism Up to isomorphism we characterise the denotable event structures as the bundle event structures proposed in Langerak [11]. As we will recall in Section 1, these include all prime event structures with binary conflict, and are included in the stable event structures with binary conflict (cf. Figure 1). In [11] examples can be found showing that these inclusions are strict.

event structures stable bundle prime  binary conflict

Fig. 1. Several classes of event structures

Our characterisation of the bundle event structures as the event structures that can be expressed by CCSP expressions is exact when dealing with the original finite bundle event structures and recursion-free CCSP. Our characterisation is also exact when dealing with arbitrary infinite bundle event structures and a version of CCSP with an infinite parallel composition operator. However, when dealing with countable event structures and CCSP expressions with arbitrary systems of recursion equations, or with recursive enumerable event structures and a recursive enumerable version of CCSP, all we can show is that the denotable event structures are a subclass of the bundle event structures that include all prime event structures with binary conflict.

In Section 2 a denotational semantics of CCSP is given in terms of event structures with binary conflict. This semantics follows the standard lines of [17, 18]. In the same section we show that the class of bundle event structures is closed under the CCSP operators, thereby establishing that CCSP expressions can denote bundle event structures only. Along the same lines one can show that the bundle event structures are closed under action refinement [5], the choice operators □ and ⊓ of CSP, and many other operators found in the literature. We are not aware of any operator interpreted on event structures for which the class of bundle event structures is not closed.

In Section 3 we show that up to isomorphism

• every finite bundle event structure can be denoted by a recursion-free CCSP expression,

• every countable prime event structure with binary conflict can be denoted by a CCSP expression,

• and every bundle event structure can be denoted by a CCSP expression with an infinitary parallel composition.

We also provide a recursive enumerable version of the second result. The same results can be obtained for the language of [17, 18].

Denotability up to hereditary history preserving bisimulation equivalence The concept of history preserving bisimulation equivalence stems from Rabinovich & Trakhtenbrot [15] and was adapted to event structures in Van Glabbeek & Goltz [5]. There it was suggested that the notion could be regarded as the coarsest equivalence that takes the interplay of causality and branching time completely into account. This makes the equivalence a semantically interesting choice of parameter to instantiate our quest with. We arrive at the positive conclusion that up to history preserving bisimulation every countable stable event structure can be denoted by a CCSP expression. This result is obtained in three steps, the first of which is the aforementioned denotability by CCSP expressions of countable prime event structures with binary conflict. In Section 4 we extend this to countable stable event structures, by observing that that every countable stable event structure with binary conflict is history preserving bisimulation equivalent with a countable prime event structure with binary conflict.

In Section 5 we complete the proof by showing that every countable stable event structure is history preserving bisimulation equivalent with a countable stable event structure with binary conflict. This result was first claimed by us in [8] for finite prime event structures. The claim was strengthened in [6] to include infinite ones. The first published proof (for prime event structures) appears in Nielsen & Winskel [14], who discovered the result independently. Their proof is somewhat nonconstructive however, in the sense that there is no construction giving a specific countable event structure with binary conflict for any given countable stable event structure with arbitrary conflict. Our proof offers such a construction and is somewhat shorter as well.

The results above hold even when merely working up to hereditary history preserving bisimulation equivalence, which is a finer variant of history preserving bisimulation equivalence, proposed by Bednarczyk [1].

Denotability up to ST-bisimulation equivalence The coarser ST-bisimulation equivalence, proposed in Van Glabbeek & Vaandrager [7], respects branching time and the possibility of actions to overlap in time, but abstracts from the faithful modelling of causality. By Theorem 1 in Van Glabbeek & Plotkin [6], every event structure, stable or not, is ST-bisimulation equivalent to a prime event structure. This result keeps being valid when assuming and requiring countability. It follows that up to STbisimulation equivalence every event structure can be denoted by a CCSP expression.

1 Bundle event structures

Bundle event structures are introduced in Langerak [11]. Here we add the alphabets for typed bundle event structures and generalise the notion to structures with infinite sets of events.

Definition 1. A (typed) bundle event structure is a 5-tuple E = (E, #, ↦, A, l) where

• E is a set of events,

• # ⊆ E × E is an irreflexive and symmetric relation, the conflict relation,

• ↦ ⊆ 2^{E}×E is the bundle set, satisfying X ↦ e ⇒ ∀e_{1}, e_{2} ∈X. e_{1} ≠e_{2} ⇒ e_{1}#e_{2},

• A is a set of actions, the alphabet of E,

• and l : E → A is the labelling function.

A bundle event structure represents a concurrent system in the following way: action names a ∈ A represent actions the system might perform and an event e ∈ E labelled with a represents an occurrence of a during a possible run of the system. In order for e to happen it is necessary that for every bundle X ↦ e, one of the elements of X occurred previously. The conflict d#e means that the events d and e cannot happen both in the same run.

The components of a bundle event structure E will be denoted by E_{E}, #_{E}, ↦_{E}, A_{E} and l_{E}; a convention that will also apply to other structures given as tuples.

The behaviour of a bundle event structure is described by explaining which subsets of events constitute possible (partial) runs of the represented system (thus formalising the interpretation of the bundle sets and the conflict relation). These subsets are called configurations. The causal relationships between events in a configuration x can be represented by a partial order <_{x}.

Definition 2. The set C(E) of (finite) configurations of a bundle event structure E = (E, #, ↦, A, l) consists of those finite x ⊆ E which are

• conflict-free: # ∩ (x × x) = ∅,

• and secured:

∃e_{1}, ..., e_{n} (n ≥ 0): x = {e_{1}, ..., e_{n}}∧∀i<n (Y ↦ e_{i+1} ⇒ {e_{1}, ..., e_{i}}∩Y ≠∅).

The causality relation <_{x} on x ∈ C(E) is {(d, e) ∈ x × x | ∃Y : d ∈ Y ↦ e}^{+}. Here R^{+} denotes the transitive closure of a relation R.

Following [5], we only consider finite configurations here; since the infinite configurations which are usually considered are completely determined by the finite ones, this causes no loss of generality. Note that if e ∈ x ∈ C(E) and Y ↦_{E} e then x ∩ Y has exactly one element. Hence <_{x} is always a partial order.

We now define the prime and the stable event structures with binary conflict, stemming from Winskel [18], and show that the bundle event structures can be regarded as a generalisation of the former and a special case of the latter.

Definition 3. A (typed) prime event structure with binary conflict is a 5-tuple E = (E, <, #, A, l) where

• E, A, and l are as above,

• < ⊆ E × E is a partial order such that ∀e ∈ E : {d ∈ E | d < e} is finite,

• and # ⊆ E × E is an irreflexive, symmetric relation satisfying

∀d, e, f ∈ E : d < e ∧ d#f ⇒ e#f.

Here d < e means that d is a prerequisite for e. Prime event structures with binary conflict can be regarded as special bundle event structures, by defining

X ↦ e ⇔ X = {d} ∧ d < e.

The definition of configurations given above is then consistent with the one in [18].

Definition 4. A (typed) event structure with binary conflict is a 5-tuple E = (E, #, ⊢, A, l) where

• E, #, A, and l are as for bundle event structures, Con = {X ⊆ E | X finite and d#e for no d, e ∈ X} is the consistency predicate,

• and ⊢ ⊆ Con × E is the enabling relation, satisfying

X ⊢ e ∧ X ⊆ Y ∈ Con ⇒ Y ⊢ e.

E is stable if Y ⊢ e implies that there is a least subset X of Y with X ⊢ e.

X ⊢ e means that X is a possible cause of e in the sense that e can occur only if for certain Y with Y ⊢ e all events in Y have occurred before.

Definition 5. The set C(E) of (finite) configurations of an event structure with binary conflict E = (E, #, ⊢, A, l) consists of those finite x ⊆ E which are

• conflict-free: # ∩ (x × x) = ∅, i.e. x ∈ Con,

• and secured: ∃e_{1}, ..., e_{n} (n ≥ 0) : x = {e_{1}, ..., e_{n}} ∧ ∀i < n {e_{1}, ..., e_{i}} ⊢ e_{i+1}.

The causality relation <_{x} on x is {(d, e) ∈ x × x | ∀Y : Y ⊢ e ⇒ d ∈ Y }^{+}.

The causality relation gives a faithful description of the causal relations in a configuration only if E is stable. As shown in [17, 18], unstable event structures can model causal relationships that cannot be captured in terms of partial orders. The following shows how bundle event structures can be regarded as special stable event structures with binary conflict.

Definition 6. Given a bundle event structure E = (E, #, ↦, A, l), the associated event structure with binary conflict E(E) = (E, #, ⊢, A, l) is given by

X ⊢ e ⇔ X ∈ Con ∧ ∀Y : (Y ↦ e ⇒ X ∩ Y ≠ ∅).

Proposition 1. E(E) is always stable. Moreover, the translation E preserves configurations and the causality relations <_{x} on them.

Proof. Straightforward.

2 A denotational event structure semantics of CCSP

CCSP is parametrised by the choice of an infinite set Act of actions, that we will assume to be fixed for this paper. We also assume an infinite set V of variable names. A variable is a pair X_{A} with X ∈ V and A ⊆ Act. The syntax of CCSP is given by

P ::= 0_{A} | aP | P + P | P ∥P | R(P) | X_{A} | {/ \atop \}X_{A}|S{\ \atop /} (with X_{A} ∈ V_{S})

with A ⊆ Act, a ∈ Act, R ⊆ Act × Act, X ∈ V and S a recursive specification: a set of equations {X_{A} = P_{X_{A}} | X_{A} ∈ V_{S}} with V_{S} ⊆ V × Act (the bound variables of S) and α(P_{X_{A}}) = A for all X_{A} ∈ V_{S} (were α(P_{X_{A}}) is defined below). The constant 0_{A} represents a process that is unable to perform any action. The process aP first performs the action a and then proceeds as P. The process P + Q will behave as either P or Q, ∥ is a partially synchronous parallel composition operator, R a renaming, and {/ \atop \}X_{A}|S{\ \atop /} represents the X_{A}-component of a solution of the system of recursive equations S. A CCSP expression P is closed if every occurrence of a variable X_{A} occurs in a subexpression {/ \atop \}Y_{B}|S{\ \atop /} of P with X_{A} ∈ V_{S}. An expression a0_{∅} is abbreviated a.

Just like the version of CSP from Hoare [9], the version of CCSP used here is a typed language, in the sense that with every process P an explicit alphabet α(P) ⊆ Act is associated, which is a superset of the set of all actions the process could possibly perform. This alphabet is exploited in the definition of P ∥Q: actions in the intersection of the alphabets of P and Q are required to synchronise, whereas all other actions of P and Q happen independently. Because of this, processes with different alphabets may never be identified, even if they can perform the same set of actions and are alike in all other aspects. It is for this reason that we interpret CCSP in terms of typed event structures. The constant 0 and the variables are indexed with an alphabet. The alphabet of an arbitrary CCSP expression is given by:

• α(0_{A}) = α(X_{A}) = α({/ \atop \}X_{A}|S{\ \atop /}) = A

• α(aP) = {a} ∪ α(P)

• α(P + Q) = α(P ∥Q) = α(P) ∪ α(Q)

• α(R(P)) = {b | ∃a ∈ α(P) : (a, b) ∈ R}.

Substitutions of expressions for variables are allowed only if the alphabets match. For this reason a recursive specification S is declared syntactically incorrect if α(P_{X_{A}}) ≠ A for some X_{A} ∈ V_{S}.

Below we define the CCSP operators formally on the domains of (typed) bundle and stable event structures with binary conflict. As our bundle and stable interpretations agree on the components E, #, A and l, they will be given as 6-tuples (E, #, ↦, ⊢, A, l), so that the bundle interpretation is found by dropping ⊢, and the stable interpretation by dropping ↦. When E is an event structure representing a CCSP expression P then A_{E} = α(P). Hence we can abstain from explicitly mentioning the A-component in the forthcoming constructions. Definition 7. The operators of CCSP are defined on event structures as follows: Inaction: E_{0_{A}} = (∅, ∅, ∅, ∅, A, ∅). Action prefix (for a ∈ Act):

• E_{aE} = {a} ∪ {âe | e ∈ E_{E}}

• l_{aE}(a) = a and l_{aE}(âe) = l_{E}(e)

• #_{aE} = {(âe, âe′) | e#_{E}e′}

• ↦_{aE}= {(âX, âe) | X ↦_{E} e}∪{({a}, âe) | e∈E_{E}} in which âX = {âe | e∈X} • ⊢_{aE}= {(X, a) | X ∈ Con_{aE}} ∪ {(âX ∪ {a}, âe) | X ⊢_{E} e}. Alternative composition:

• E_{E_{1}+E_{2}} = {+_{1}e | e ∈ E_{E_{1}}} ∪ {+_{2}e | e ∈ E_{E_{2}}}

• l_{E_{1}+E_{2}}(+_{i}e) = l_{E_{i}}(e) (i=1, 2)

• #_{E_{1}+E_{2}} = \begin{matrix}\{(+_{i}e, +_{i}e′) | e#_{E_{i}}e′, i=1, 2\} ∪ \\ \{(+_{i}e, +_{j}f) | e ∈ E_{E_{i}}, f ∈ E_{E_{j}}, i≠j\} \end{matrix}

• ↦_{E_{1}+E_{2}}= {(+_{i}X, +_{i}e) | X ↦_{E_{i}} e, i=1, 2} in which +_{i}X = {+_{i}e | e ∈ X} • ⊢_{E_{1}+E_{2}}= {(+_{i}X, +_{i}e) | X ⊢_{E_{i}} e, i=1, 2}. Parallel composition:

• E_{E∥F} = {(e∥∗) | l_{E}(e) ∉ A_{F}} ∪ {(∗∥f) | l_{F}(f) ∉ A_{E}} ∪ {(e∥f) | l_{E}(e) = l_{F}(f) ∈ A_{E} ∩ A_{F}}

• l_{E∥F}(e∥∗) = l_{E}(e), l_{E∥F}(∗∥f) = l_{F}(f) and l_{E∥F}(e∥f) = l_{E}(e) = l_{F}(f)

• #_{E∥F} = {(e∥f, e′∥f′) | (e∥f ≠ e′∥f′)∧(e#_{E}e′∨e=e′ ≠∗∨f#_{F}f′∨f =f′ ≠∗)} • ↦_{E∥F}= {(X∥F, e∥f) | X ↦_{E} e} ∪ {(E∥Y, e∥f) | Y ↦_{F} f}

in which X∥F = {(e∥f) ∈ E_{E∥F} | e ∈ X} and E∥Y = {(e∥f) ∈ E_{E∥F} | f ∈ Y } • ⊢_{E∥F}= {(X, e∥f) | (e = ∗ ∨ π_{1}(X) ⊢_{E} e) ∧ (f = ∗ ∨ π_{2}(X) ⊢_{F} f)}

in which π_{1}(X) = {e ∈ E_{E} | ∃f ∈ E_{F} ∪ {∗} : e∥f ∈ X}

and π_{2}(X) = {f ∈ E_{F} | ∃e ∈ E_{E} ∪ {∗} : e∥f ∈ X}. Relational renaming (for R ⊆ Act × Act):

• E_{R(E)} = {R_{b}e | e ∈ E_{E}, (l_{E}(e), b) ∈ R}

• l_{R(E)}(R_{b}e) = b

• #_{R(E)} = {(R_{b}e, R_{c}e′) | e#_{E}e′ ∨ (e = e′ ∧ b ≠ c)}

• ↦_{R(E)}= {(R(X), R_{b}e) | X ↦_{E} e} in which R(X) = {R_{b}e | e ∈ X ∧ (l_{E}(e), b) ∈ R}

• ⊢_{R(E)}= {(X, R_{b}e) | X ∈ Con ∧ R^{−1}(X) ⊢ e} in which R^{−1}(X) = {e ∈ E_{E} | ∃b ∈ A_{R(E)} : R_{b}e ∈ X}.

The semantics for 0, aE, E + F and E∥F follows the lines of [17, 18, 2, 11]. Relational renaming appears in [16] and [4]. For every relation R ⊆ Act×Act there is an operator R that replaces each occurrence of an action a by fresh occurrences of the actions {b | aRb}. These occurrences are pairwise in conflict, and inherit their causal relationships from their source. The relabelling operators of CCS [12], CSP [3] and Winskel [18] are special cases where R is a function; the inverse image operator of CSP [3] is the special case where R is the inverse of a function. In case R(a) = ∅, the definition implies that the events labelled a are removed; thus also the restriction operators of CCS and [18] constitute special cases of relational renaming. Relational renaming in turn is a special case of action refinement, as studied for instance in [5]. Also note that every relational renaming operator can be written as the composition of an inverse image operator and a functional renaming operator.

The meaning of the recursion constructs {/ \atop \}X_{A}|S{\ \atop /} can be given by means of least fixed point techniques, see e.g. [17, 18]. The fact that we allow recursive specifications of arbitrary size (in [17, 18] they are of size 1) does not create complications; we will not repeat the definitions here. Following the standard denotational approach this yields a bundle event structure [[P]] and a general event structure [[P]]_{E} for every closed CCSP expression P. For open CCSP expressions [[P]] and [[P]]_{E} are functions from valuations of the variables to event structures.

Proposition 2. For every CCSP expression P we have E([[P]]) = [[P]]_{E}. Hence the bundle event structures, seen as a subclass of the stable event structures, are closed under the operators of CCSP.

Proof. Straightforward with Definition 7.

3 Denoting bundle event structures in CCSP

In this section we address the question which event structures can be denoted by closed CCSP expressions of various kinds. As the events in structures [[P]] with P a closed CCSP expression have very particular names, whose choice seems to carry little semantic relevance, it is for this purpose most appropriate to study event structures up to isomorphism. Here two event structures E and F are isomorphic (E ≅ F) iff A_{E} = A_{F} and there exists a bijection between their sets of events preserving ↦ (resp. ⊢), # and labelling. Later we will see if the class of denotable event structures increases when considering a coarser equivalence.

The following proposition allows us to exchange, within a recursion-free CCSP expression, a closed subexpression by another expression denoting an isomorphic event structure.

Proposition 3. (Congruence) Let E, E′ and F be event structures with E ≅ E′. Then aE ≅ aE′ for a ∈ Act, E+F ≅ E′ +F, F+E ≅ F+E′, E∥F ≅ E′∥F, F∥E ≅ F∥E′ and R(E) ≅ R(E′) for R : Act → Act.

Proof. Immediate from the definitions.

The next one, essentially due to Hoare [9], allows us to drop brackets and abstract from the order of components in nested parallel compositions.

Proposition 4. Let E, F and G be event structures. Then E∥(F∥G) ≅ (E∥F)∥G and E∥F ≅ F∥E.

Proof. Straightforward.

Now we are ready to state the main theorems. We start with the simplest case of finite prime event structures with binary conflict.

Theorem 1. For every finite prime event structure with binary conflict E there is a closed recursion-free CCSP expression P such that [[P]] ≅ E.

Proof. As we are interested in E only up to isomorphism, w.l.o.g. we may assume that E_{E} ⊂ Act, i.e. the names of the events can also be used as names of CCSP actions. Let E′ be the variant of E in which every event is labelled by itself. We first build a CCSP expression denoting E′ (up to isomorphism), by encoding all events and all elements of the conflict and causality relation of E′ in terms of CCSP constructions. Subsequently, an expression for E is obtained by applying a renaming operator. Let E_{E} = {a_{1}, ..., a_{n}}, #_{E} = {(b_{1}, c_{1}), ..., (b_{m}, c_{m})} and <_{E}= {(d_{1}, e_{1}), ..., (d_{k}, e_{k})}. Then

P = l_{E} [a_{1}∥ ⋯ ∥a_{n}∥(b_{1} + c_{1})∥ ⋯ ∥(b_{m} + c_{m})∥(d_{1}e_{1})∥ ⋯ ∥(d_{k}e_{k})] + 0_{A_{E}}.

Here l_{E} is not only the labelling function of E, but also one of the renaming operators of CCSP. Note that the actions b_{i} and c_{i} (i = 1, ..., m), as well as d_{j} and e_{j} (j = 1, ..., k) are among the actions a_{1}, ..., a_{n}. We have that [[a∥(a + b)]] ≅ [[a + b]] and [[a∥(ab)]] ≅ [[b∥(ab)]] ≅ [[ab]]. Hence it would suffice to list as a_{1}, ..., a_{n} only those events not in conflict or in any causal relationship with another event. It is routine to check that the constructed expression denotes E (up to isomorphism). The term 0_{A_{E}} is added in case the alphabet of E contains actions that do not arise as the label of any event.

It is interesting to observe that the relational renaming operator is not needed in this proof; functional renaming would suffice. The proof above holds for the syntax of CSP—as in [3]—as well. The same cannot be done in CCS [12], because there only handshaking communication is available.

Now we pass to the case of finite bundle event structures.

Theorem 2. For every finite bundle event structure E there is a closed recursion-free CCSP expression P such that [[P]] ≅ E.

Proof. The proof goes along the same lines as the previous one, except that instead of causal links d <_{E} e we now have to encode bundles X ↦_{E} e. Let X = {d_{1}, ..., d_{h}}. Then the bundle X ↦_{E} e is represented by R(de) where d is a fresh action and R is the relational renaming {(d, d_{1}), (d, d_{2}), ..., (d, d_{h})(e, e)}.

One may wonder to what extent relational renaming is really needed here. For the language CCSP as given here it is, because with a straightforward structural induction one can check that all bundle event structures that can be denoted by recursion-free CCSP expressions with merely functional renaming only have bundles X ↦ e in which all events in X have the same label. However, there are other process algebraic operators that can take over the rôle of relational renaming.

Theorem 3. For every finite bundle event structure E there is a closed recursion-free expression P in the language from Winskel [18] such that [[P]] ≅ E.

Proof. Winskel’s language does not have relational renaming, but only functional renaming and a restriction operator ⌈. The restriction E⌈A behaves like E but with its events restricted to those with labels which lie in the set A. The parallel composition × in Winskel’s language allows every pair of events to synchronise; if e_{0} is labelled a_{0} and e_{1} is labelled a_{1} the synchronisation event is then labelled (a_{0}, a_{1}). Events need not synchronise however; an event e_{0} in the first component that does not synchronise with any event of the second will be labelled by (a_{0}, ∗), where a_{0} is the label of e_{0}. For the rest Winskel’s language is the same as CCSP, but untyped. The parallel operator of CCSP can be defined in terms of the operators ×, functional renaming and restriction. Although in a setting without recursion it is not possible to define CCSP’s relational renaming operation in terms of the operations of Winskel’s language, we can, for any finite bundle event structure E in which all actions have a different label and any image finite relational renaming R, define a context C_{R,E}[.] in Winskel’s language that behaves like R. In the definition of this context, we use as a derived construct the interleaving operator ||| that is given by

P |||Q = f((P × Q)⌈{(a, ∗) | a ∈ α(P)} ∪ {(∗, b) | b ∈ α(Q)}),

where f is a functional renaming that renames each action (a, ∗) into a, and each action (∗, b) into b. Let E and R be as stipulated. Now the context C_{R,E}[.] can be defined as

C_{R,E}[.] = g(([.] × (a_{1}||| ⋯ |||a_{n}))⌈R′),

where {a_{b} | ∃e ∈ E_{E}∧l_{E}(e) = a∧(a, b) ∈ R} = {a_{1}, … a_{n}}, R′ = {(a, a_{b}) | (a, b) ∈ R} and g is the functional renaming that renames each action (a, a_{b}) into b. We claim that [[R(E)]] = [[C_{R,E}[E]]] for each bundle event structure E in which all actions have a different label and any image finite relational renaming R. Using C_{R,de}(de) instead of R(de) in the proof of Theorem 2 now yields the required result.

In the presence of sequential composition, such as the operator ; in CSP, a bundle {d_{1}, ..., d_{h}} ↦_{E} e can also be represented as (d_{1} + ⋯ + d_{h}); e. However, a semantics of ; requires the introduction of a special event-label √, or some other additional structure, that helps to distinguish deadlock from successful termination. Arbitrary bundle event structures with this additional structure can in general not be represented by CSP expressions, at least not with the method employed here. Nevertheless, the construction above would work when taking ; to be a sequencing operator [5] that starts its second argument as soon as its first argument can perform no further actions.

Next we turn to infinite bundle event structures. Obviously any bundle event structure can be denoted, up to isomorphism, in a variant of CCSP with a suitable infinitary parallel composition ∥_{i∈I}P_{i}. If we stick to the binary versions of ∥ and + it is straightforward to check that only countable event structures can be denoted (event structures with countably many events and only countably many bundles), even in the presence of arbitrary large recursive specifications. Thus, the best we can hope for is that every countable bundle event structure can be denoted by a CCSP expression. We are not sure if this is true; however, it can be established for prime event structures with binary conflict.

Theorem 4. For every countable prime event structure with binary conflict E there is a closed CCSP expression P such that [[P]] ≅ E.

Proof. Although only the binary parallel composition exists in the syntax, a countable parallel composition P_{0}∥P_{1}∥ ⋯ can be created with infinite unguarded recursion, namely as {/ \atop \}X_{A_{0}}^{0}|S{\ \atop /} where S contains the equations X_{A_{i}}^{i} = P_{i}∥X_{A_{i+1}}^{i+1} where A_{i} = ⋃_{j≥i} α(P_{j}), for i ∈ IN. However, the denotational interpretation of such a system of equations contains only events whose existence can be proved by unwinding the recursion a finite number of times. There are for instance no events in [[{/ \atop \}X_{A}|(X_{A} =a∥X_{A}){\ \atop /}]]. Thus, for the generated parallel composition to be useful, we need to require that for each a ∈ A_{0} there is an i with a ∉ A_{i}, i.e. ⋂_{i∈IN} A_{i} = ∅. (*)

Now let E_{E} = {a_{i} | i ∈ IN}, where the numbering is chosen in such a way that a_{i} <_{E} a_{j} ⇒ i < j. As <_{E} is a partial order in which {d ∈ E | d <_{E} e} is finite for all e ∈ E_{E}, this is always possible. Then the (possibly infinite) parallel composition ∥{a_{j} | a_{i} <_{E} a_{j}} contains all events that have a_{i} as a causal predecessor, executed in parallel. Hence [[a_{i}(∥{a_{j} | a_{i} <_{E} a_{j}})]] is the fragment of the desired event structure that contains all causal links starting in a_{i}. Its alphabet is contained in {a_{j} | j ≥ i}. The parallel composition of all such event structures for i ∈ IN therefore contains all causal links of E, and satisfies (*). This structure is to be put in parallel with one containing all conflicts, constructed in a similar way. As #_{E} is irreflexive and symmetric, we only need to implement the conflicts a_{i}#_{E}a_{j} with i < j. We find that E is denoted by

P = l_{E} [ ∥_{i=0}^{∞}(a_{i}(∥{a_{j} | a_{i} <_{E} a_{j}})∥ ∥_{i=0}^{∞}(a_{i} + ∥{a_{j} | j > i ∧ a_{i}#_{E}a_{j}})] + 0_{A_{E}}

We leave it as an open problem whether the same can be achieved using only finite recursive specifications.

Due to the presence of uncountably many renaming operators, the signature of CCSP is undecidable. This can be changed by only allowing recursive enumerable renaming operators, i.e. operators R ⊆ Act×Act for which there exists a Turing machine enumerating all pairs (a, b) ∈ R. Such renaming operators can be represented by the source code describing the generating Turing machine. Codes are finite objects, and it is decidable whether a piece of text is the source code describing such a Turing machine. Now define a recursive enumerable version of CCSP, call it CCSP^{r.e.}, by requiring

• that Act is a r.e. set and all renaming operators are r.e.,

• that only r.e. subsets of Act are allowed as indices of 0 and the variables.

• and that recursive specifications S, seen as functions from V_{S} to the CCSP expressions, should be primitive recursive, with V_{S} a primitive decidable set.

This makes the signature of the language decidable. The primitive recursive requirement on S even makes it decidable whether a variable in a CCSP^{r.e.} expression is free [4]. Now we have the following recursive enumerable version of Theorem 4:

Theorem 5. Let E be a prime event structure with binary conflict such that E_{E}, #_{E}, <_{E}, A_{E} are recursive enumerable sets, l_{E} is a recursive function, and there is an algorithm that for every event returns the finite set of its causal predecessors. Then there is a closed CCSP^{r.e.} expression P such that [[P]] ≅ E.

4 Denoting stable event structures with binary conflict in CCSP

In this section we infer from Theorem 4 that up to hereditary history preserving bisimulation equivalence any countable stable event structure with binary conflict can be denoted by a closed CCSP expression.

Definition 8. Two stable event structures E and F are history preserving bisimulation equivalent (E \underline{↔}_{h} F) iff A_{E} = A_{F} and there exists a relation R ⊆ C(E) × C(F) × P(E_{E} × E_{F})—called a history preserving bisimulation—such that (∅, ∅, ∅) ∈ R and whenever (x, y, f) ∈ R then

• f is an isomorphism between (x, <_{x}, l_{E} ^{\}x) and (y, <_{y}, l_{F} ^{\}y),

• x ⊆ x′ ∈ C(E) ⇒ ∃y′, f′ with y ⊆ y′ ∈ C(F), (x′, y′, f′)∈R and f′^{\}x=f,

• y ⊆ y′ ∈ C(F) ⇒ ∃x′, f′ with x ⊆ x′ ∈ C(E), (x′, y′, f′)∈R and f′^{\}x=f.

The bisimulation and the equivalence are hereditary (E\underline{↔}_{hh} F) if moreover

• x ⊇ x′ ∈ C(E) ⇒ ∃y′, f′ with y ⊇ y′ ∈ C(F), (x′, y′, f′)∈R and f′=f^{\}x′,

• y ⊇ y′ ∈ C(F) ⇒ ∃x′, f′ with x ⊇ x′ ∈ C(E), (x′, y′, f′)∈R and f′=f^{\}x′.

R is functional if R = {(x, f(x), f ^{\}x) | x ∈ C(E)} for a function f: E_{E} → E_{F}.

Note that a functional bisimulation is always hereditary. Moreover, when checking that a function f : E_{E} → E_{F} induces an history preserving bisimulation, the second requirement is trivially fulfilled. Joyal, Nielsen & Winskel [10] characterised a functional history preserving bisimulation as a categorical construction called open map.

Definition 8 also applies when E and F are prime or bundle event structures, or when one of them is prime and the other is stable. We now show that every (countable) stable event structure with binary conflict is hereditary history preserving bisimulation equivalent with a (countable) prime event structure with binary conflict.

Definition 9. Given a stable event structure E = (E, #, ⊢, A, l) with binary conflict, the associated prime event structure E′ = (E′, <, #′, A, l′) is given by

• E′ = {e_{x} | e ∈ x ∈ C(E) and x is a minimal configuration containing e},

• d_{x} < e_{y} iff x ⊂ y,

• d_{x}#′e_{y} iff E has no configuration containing both x and y,

• l′(e_{X}) = l(e).

E′ is obviously a prime event structure with binary conflict, and if E is countable, then so is E′. Moreover, it is not too hard to check that the function f : E′ → E given by f(e_{X}) = e for e ∈ E′ induces a history preserving bisimulation. Therefore, any (countable) stable event structure with binary conflict is hereditary history preserving bisimulation equivalent with a (countable) prime event structure with binary conflict. This result also follows from the category theoretic results in [10]. In view of this, Theorem 4 implies

Theorem 6. For every countable stable event structure with binary conflict E there is a closed CCSP expression P such that [[P]]\underline{↔}_{hh} E.

5 Arbitrary conflict reduces to binary conflict

In [17] event structures of the form (E, Con, ⊢, A, l) appear, in which the predicate Con of Definition 4 is explicitly given rather then generated by a binary conflict relation. It is postulated that Con is a downwards closed nonempty set of finite sets of events. The configurations of such event structures and the causality relations on them are determined exactly as in Definition 5. Note that Con can equivalently be represented by its complement: an upwards closed set Confl of finite nonempty sets of events. Another equivalent representation is in terms of the minimal members of Confl: a collection # of finite nonempty sets of events, such that there are no two different γ, γ′ ∈ # with γ ⊂ γ′. Now a finite set x is consistent or conflict-free if γ ⊆ x for no γ ∈ #. In this representation event structures with a binary conflict relation are literally a special case of the ones with arbitrary conflict relations. Statement γ ∈ # means that the events in γ cannot all happen in the same run. It does not place a restriction on proper subsets of γ.

In this section we show that every (countable) stable event structure is history preserving bisimulation equivalent to a (countable) prime event structure with binary conflict. For finite prime event structures this theorem was claimed by us in [8]. The generalisation to infinite event structures was reported in [6]. The same theorem has been discovered independently by Nielsen & Winskel [14], where the first published proof can be found. Although our proof is based on the same idea as the one of [14], it is somewhat shorter and more constructive.

Definition 10. Let E be a countable event structure with arbitrary conflict. For e ∈ E_{E} let #_{e} be the set of conflicts involving e: #_{e} = {γ ∈ #_{E} | e ∈ γ}. Define the event structure 2(E) by

• E_{2(E)} = {(e, t)|e∈E_{E}, t: #_{e} →IN with t recursive and ∀γ ∈#_{e}: t(γ) < |γ|−1}

• A_{2(E)} = A_{E} and l_{2(E)}(e, t) = l_{E}(e)

• #_{2(E)} = {((e, t), (e′, t′)) | (e = e′ ∧ t ≠ t′) ∨ (e ≠ e′ ∧ ∃γ ∈ #_{e} : t(γ) = t′(γ))}

• ↦_{2(E)}= {(2(X), (e, t)) | X ↦_{E} e} in which 2(X) = {(e, t) | e ∈ X}

• ⊢_{2(E)}= {(X, (e, t)) | π_{1}(X) ⊢ e} in which π_{1}(X) = {e ∈ E_{E} | ∃t : (e, t) ∈ X}.

The idea behind this definition is the following: every member γ of the conflict relation on E has |γ| elements, of which only |γ| − 1 can be executed. This can be modelled as an allocation of |γ| − 1 seats to |γ| events. Let us number these seats from 0 to |γ| − 2. The event that is last in grabbing a seat can not happen. In general an event can occur in many elements γ of #_{E}, namely the ones in #_{e}. In order to happen it has to grab a seat for each of these γ’s. Now 2(E) is an event structure where this abstract notion of conflict has been implemented on a more down-to-earth level. The new events are allocations of old events to seats. To be precise, they are pairs (e, t), where e is the name of the source event and t a function that for every competition γ ∈ #_{e} in which e participates selects a seat t(γ) < |γ| − 1. In [14] a pair (e, t) is called an event with a twist; hence the choice of the letter t. Now the new events, which are old events allocated to seats, inherit their labelling and their causal dependencies from their source events. The causal dependencies are implemented by ↦_{2E} or ⊢_{2E}, depending on whether the original event structure was a bundle, or a general one. Compare these definitions with the relational renaming operator in Section 2. The conflict relation on 2(E) is binary. The first set of conflicts ensures that an event can occur with only one allocation to seats in the various conflicts. The second set, that no two events are assigned the same seat in any particular conflict. This implements the abstract notion of conflict in E.

When an event e′ occurs is does not really matter which seats it chooses in the various conflicts it participates in, as long as these seats are not yet taken by other events. For each event e that happened already, the chosen seats are given by the function t it happened with. Now e′ has to choose an allocation function t′ that is different from t in each conflict that involves both e′ and e. In order to make such a choice in a computationally respectful way, we assume that all allocation functions of events that happened previously are recursive. When e is about to happen, it can then calculate which seats are still free and choose a function that is recursive as well. (A function t : #_{e} → IN is recursive if there is a partial recursive function t′ : P_{fin}(E_{E}) → IN with t = t′ ^{\}#_{e} a total function. There is no need to assume that #_{e} is a decidable set.) The resulting requirement in Definition 10 that all functions t should be recursive, ensures that 2(E) is still countable. Without the recursiveness requirement this would not be the case.

Theorem 7. Let E be a countable stable event structure. Then 2(E) is a countable stable event structure with binary conflict and the function f : 2(E) → E given by f(e, t) = e induces a history preserving bisimulation. Hence 2(E)\underline{↔}_{hh} E.

Proof. As (e, t)#_{2(E)}(e, t′) for t ≠ t′, it follows immediately that f ^{\}x is injective for every configuration x. Now suppose f(x) contains a conflict γ ∈ #_{E}. Then in x there must be events {(e_{i}, t_{i}) | e_{i} ∈ γ} with t(e_{i}) < |γ| − 1. Hence two of these events must be in conflict, contradicting that x is a configuration. If follows that f(x) is conflictfree. It is immediate from the definition of ↦_{2(E)} resp. ⊢_{2E} that if (e_{1}, t_{1}), ..., (e_{n}, t_{n}) secures x in 2(E) then e_{1}, ..., e_{n} secures f(x). Hence x is a configuration of E. It is also immediate from the definition of ↦_{2(E)} resp. ⊢_{2E} that f preserves <_{x} and labelling.

Now suppose x ∈ C(2(E)) and f(x) ⊆ y′ ∈ C(E). We need to show that there is an x′ ∈ C(2(E)) with x ⊆ x′ and f(x′) = y′. By induction on |y′| it suffices to restrict attention to the case that there is exactly one event in y′ − f(x), call it e. As y′ is conflict-free, for every γ ∈ #_{e} we have that |γ ∩ f(x)| ≤ |γ| − 2. Hence there exists a recursive t : #_{e} → IN satisfying, for all γ ∈ #_{e}, t(γ) < |γ| − 1 and for no (e′, t′) ∈ x: t′(γ) = t(γ). It follows that x′ =^{def} x ∪ {(e, t)} is conflict-free. Moreover, any securing (e_{1}, t_{1}), ..., (e_{n}, t_{n}) of x can be extended with (e, t) into a securing of x′. This follows because e_{1}, ..., e_{n}, e is a securing of y′, using the definition of ↦_{2(E)} resp. ⊢_{2E}. Thus x′ ∈ C(2(E)), which had to be proved. The other requirement for f inducing a history-preserving bisimulation is trivial.

By combining this insight with Theorem 6 it follows immediately that up to hereditary history preserving bisimulation equivalence all countable stable event structures with arbitrary conflicts are expressible in CCSP.

Acknowledgement Thanks to Rom Langerak for valuable feedback.

References

1. M. Bednarczyk (1991): Hereditary history preserving bisimulation, or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences,

Gdańsk. Available at ftp://ftp.ipipan.gda.pl/marek/historie.ps.gz.

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

3. S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): A theory of communicating sequential processes. Journal of the ACM 31(3), pp. 560–599.

4. R.J. van Glabbeek (1994): On the expressiveness of ACP (extended abstract). In A. Ponse, C. Verhoef & S.F.M. van Vlijmen, editors: Proceedings First Workshop on the Algebra of Communicating Processes, ACP94, Utrecht, Workshops in Computing, Springer,

pp. 188–217. Available at http://boole.stanford.edu/pub/acp.ps.gz.

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

6. R.J. van Glabbeek & G.D. Plotkin (1995): Configuration structures (extended abstract). In D. Kozen, editor: Proceedings 10^{th} Annual IEEE Symposium on Logic in Computer Science (LICS95), San Diego, USA, IEEE Computer Society Press, pp. 199–209.

7. R.J. van Glabbeek & F.W. Vaandrager (1987): Petri net models for algebraic theories of concurrency (extended abstract). In J.W. de Bakker, A.J. Nijman & P.C. Treleaven, editors: Proceedings PARLE, Parallel Architectures and Languages Europe, Eindhoven, The Netherlands, June 1987, Vol. II: Parallel Languages, LNCS 259, Springer, pp. 224–242.

8. R.J. van Glabbeek & F.W. Vaandrager (1991): The difference between splitting in n and n + 1 (abstract). In E. Best & G. Rozenberg, eds.: Proc. 3^{rd} Workshop on Concurrency and Compositionality, Goslar, GMD-Studien Nr. 191, Universität Hildesheim, pp. 117–121. Full version in Information and Computation 136(2), 1997, pp. 109–142.

9. C.A.R. Hoare (1985): Communicating Sequential Processes. Prentice Hall.

10. A. Joyal, M. Nielsen & G. Winskel (1996): Bisimulation from open maps. Information and Computation 127(2), pp. 164–185.

11. R. Langerak (1992): Transformations and Semantics for LOTOS. PhD thesis, Department of Computer Science, University of Twente.

12. R. Milner (1989): Communication and Concurrency. Prentice Hall, Englewood Cliffs.

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

14. M. Nielsen & G. Winskel (1996): Petri nets and bisimulation. Theoretical Computer Science 153, pp. 211–244.

15. A. Rabinovich & B.A. Trakhtenbrot (1988): Behavior structures and nets. Fundamenta Informaticae 11(4), pp. 357–404.

16. F.W. Vaandrager (1993): Expressiveness results for process algebras. In J.W. de Bakker, W.P. de Roever & G. Rozenberg, eds.: Proc. REX Workshop on Semantics: Foundations and Applications, Beekbergen, The Netherlands, June 1992, LNCS 666, Springer, pp. 609–638.

17. 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.

18. G. Winskel (1989): An introduction to event structures. 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. 364–397.

19. G. Winskel & M. Nielsen (1995): Models for concurrency. In S. Abramsky, D. Gabbay & T. Maibaum, editors: Handbook of Logic in Computer Science, Oxford University Press, pp. 1–148.