\documentclass{llncs}			% stylefile for Springer proceedings
\usepackage{times,latexsym}		% font, load symbols like \Box
\pagestyle{plain}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\df}[1]{Definition~\ref{df-#1}}
\newcommand{\thm}[1]{Theorem~\ref{thm-#1}}
\newcommand{\pr}[1]{Proposition~\ref{pr-#1}}

\newenvironment{itemise}{\begin{list}{$\bullet$}{\leftmargin 18pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
			\topsep 4pt \itemsep 2pt \parsep 2pt}}{\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dl}[1]{\mbox{\rm I\hspace{-0.55mm}#1}}	% openface letter
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}   % no vertical space
\newcommand{\Id}[1]{[\hspace{-1.4pt}[#1]\hspace{-1.2pt}]} % denotation
\newcommand{\rec}[1]{\plat{			 	% recursion
	\stackrel{\mbox{\tiny $/$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $\backslash$}}
	\!\!#1\!\!
	\stackrel{\mbox{\tiny $\backslash$}}
	{\raisebox{-.3ex}[.3ex]{\tiny $/$}} }}
\newcommand{\bis}[1]{ \;				% bisimulation
	\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,}
\newcommand{\rest}{\unitlength 1mm			% restriction operator
        \begin{picture}(2.16,3.2)
        \thinlines
        \put(1.12,-0.48){\line(0,1){3.52}}
	\put(0.87,1.77){\tiny $\backslash$}
        \end{picture} }
\newcommand{\interleave}{|\hspace{-1pt}|\hspace{-1pt}|}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%				Abbreviations			          %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\dl{N}}			    % natural numbers
\newcommand{\pow}{{\cal P}}			    % powerset
\newcommand{\fE}{{\cal E}}			    % function into \IE
\newcommand{\eE}{{\rm E}}			    % event structure
\newcommand{\eF}{{\rm F}}			    % event structure
\newcommand{\eG}{{\rm G}}			    % event structure

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%                               Titel                                  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}

\title{Bundle Event Structures and {CCSP}\thanks{To appear in: Proceedings
 14th International Conference on Concurrency Theory (CONCUR 2003),
 Marseille, France,  LNCS, Springer, September 2003.
 \hfill \copyright\ Springer-Verlag}}
\author{Rob van Glabbeek\inst{1} \and Frits Vaandrager\inst{2}}
\institute{National ICT Australia\\
 School of Computer Science \& Engineering,
 Univ.\ of New South Wales,
 Sydney 2052, Australia\\
 {\tt rvg@cs.stanford.edu}
\and
 Nijmegen Institute for Computing and Information Sciences,
 University of Nijmegen\\
 Postbus 9010, 6500 GL Nijmegen, The Netherlands\\
 \tt fvaan@cs.kun.nl}
\maketitle
\setcounter{footnote}{1}
\footnotetext{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.}
\refstepcounter{footnote}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{abstract}
We investigate which event structures can be denoted by means
of closed CCS $\cup$ CSP expressions. Working up to isomorphism we find that
\begin{list}{$\bullet$}{\leftmargin 15pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
			\topsep 0pt \itemsep 0pt \parsep 0pt}
\item all denotable event structures are bundle event structures,
\item upon adding an infinitary parallel composition all bundle event
structures are denotable,
\item without it every finite bundle event structure can be denoted,
\item as well as every countable prime event structure with binary conflict.
\end{list}
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.
\end{abstract}

\section*{Introduction}

In concurrency theory many languages for the representation of
concurrent systems have been proposed, including CCS, SCCS, CSP, {\sc
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\mbox{---,} 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 \cite{NPW81,Wi87a,BC94,WN94,GP95}. 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 {\em event structures}
from {\sc Winskel} \cite{Wi87a}. 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 \cite{Mi89} and CSP \cite{BHR84,Ho85}. 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 \cite{Wi87a}. 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 \cite{Wi87a} the subclass of {\em stable event structures} is
defined, as well as the further subclass of {\em prime event
structures}. In \cite{Wi89} a subclass of event structures with a 
{\em binary conflict relation} is proposed (see Figure~\ref{classes}
below). The prime event structures with binary conflict are exactly
the (finitary) event structures originally introduced in \cite{NPW81}.
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: {\em isomorphism}, {\em
history preserving bisimulation equivalence} and (in this introduction
only) {\em ST-bisimulation equivalence}.
\vspace{-1ex}

\subsubsection{Denotability up to isomorphism}
Up to isomorphism we characterise the denotable event structures as
the {\em bundle event structures} proposed in {\sc Langerak}
\cite{Lk92}. As we will recall in Section~\ref{event structures},
these include all prime event structures with binary conflict, and are
included in the stable event structures with binary conflict (cf.\
Figure~\ref{classes}). In \cite{Lk92} examples can be found showing that these
inclusions are strict.
\vspace{-1ex}

\begin{figure}[h]
%\input{classes}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
\small%
    \special{pn 3}%
    \special{ar 157 630 157 157 1.570796 3.141593}%
    \special{ar 157 157 157 157 -3.141593 -1.570796}%
    \special{ar 2992 157 157 157 -1.570796 -0.000000}%
    \special{ar 2992 630 157 157 -0.000000 1.570796}%
    \special{pa 0 630}%
    \special{pa 0 157}%
    \special{fp}%
    \special{pa 157 0}%
    \special{pa 2992 0}%
    \special{fp}%
    \special{pa 3150 157}%
    \special{pa 3150 630}%
    \special{fp}%
    \special{pa 2992 787}%
    \special{pa 157 787}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.079in
    \rlap{\kern 2.559in\lower\graphtemp\hbox to 0pt{\hss event structures\hss}}%
    \special{ar 157 630 157 157 1.570796 3.141593}%
    \special{ar 157 157 157 157 -3.141593 -1.570796}%
    \special{ar 1811 157 157 157 -1.570796 -0.000000}%
    \special{ar 1811 630 157 157 -0.000000 1.570796}%
    \special{pa 0 630}%
    \special{pa 0 157}%
    \special{fp}%
    \special{pa 157 0}%
    \special{pa 1811 0}%
    \special{fp}%
    \special{pa 1969 157}%
    \special{pa 1969 630}%
    \special{fp}%
    \special{pa 1811 787}%
    \special{pa 157 787}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.079in
    \rlap{\kern 1.575in\lower\graphtemp\hbox to 0pt{\hss stable\hss}}%
    \special{sh 0.150}%
    \special{ia 1417 551 157 157 0 6.28319}%
    \special{sh 0.150}%
    \special{ia 157 551 157 157 0 6.28319}%
    \special{sh 0.150}%
    \special{ia 157 630 157 157 0 6.28319}%
    \special{sh 0.150}%
    \special{ia 1417 630 157 157 0 6.28319}%
    \special{sh 0.150}%
    \special{pn 14}%
    \special{pa 1575 630}%
    \special{pa 1575 551}%
    \special{pa 0 551}%
    \special{pa 0 630}%
    \special{pa 1575 630}%
    \special{ip}%
    \special{sh 0.150}%
    \special{pa 1417 787}%
    \special{pa 1417 394}%
    \special{pa 157 394}%
    \special{pa 157 787}%
    \special{pa 1417 787}%
    \special{ip}%
    \special{pn 3}%
    \special{ar 157 630 157 157 1.570796 3.141593}%
    \special{ar 157 551 157 157 -3.141593 -1.570796}%
    \special{ar 1417 551 157 157 -1.570796 -0.000000}%
    \special{ar 1417 630 157 157 -0.000000 1.570796}%
    \special{pa 0 630}%
    \special{pa 0 551}%
    \special{fp}%
    \special{pa 157 394}%
    \special{pa 1417 394}%
    \special{fp}%
    \special{pa 1575 551}%
    \special{pa 1575 630}%
    \special{fp}%
    \special{pa 1417 787}%
    \special{pa 157 787}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.472in
    \rlap{\kern 1.181in\lower\graphtemp\hbox to 0pt{\hss bundle\hss}}%
    \special{ar 157 630 157 157 1.570796 3.141593}%
    \special{ar 157 157 157 157 -3.141593 -1.570796}%
    \special{ar 630 157 157 157 -1.570796 -0.000000}%
    \special{ar 630 630 157 157 -0.000000 1.570796}%
    \special{pa 0 630}%
    \special{pa 0 157}%
    \special{fp}%
    \special{pa 157 0}%
    \special{pa 630 0}%
    \special{fp}%
    \special{pa 787 157}%
    \special{pa 787 630}%
    \special{fp}%
    \special{pa 630 787}%
    \special{pa 157 787}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.079in
    \rlap{\kern 0.394in\lower\graphtemp\hbox to 0pt{\hss prime\hss}}%
    \special{ar 157 630 157 157 1.570796 3.141593}%
    \special{ar 157 551 157 157 -3.141593 -1.570796}%
    \special{ar 2992 551 157 157 -1.570796 -0.000000}%
    \special{ar 2992 630 157 157 -0.000000 1.570796}%
    \special{pa 0 630}%
    \special{pa 0 551}%
    \special{fp}%
    \special{pa 157 394}%
    \special{pa 2992 394}%
    \special{fp}%
    \special{pa 3150 551}%
    \special{pa 3150 630}%
    \special{fp}%
    \special{pa 2992 787}%
    \special{pa 157 787}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.472in
    \rlap{\kern 2.559in\lower\graphtemp\hbox to 0pt{\hss binary conflict\hss}}%
    \hbox{\vrule depth0.787in width0pt height 0pt}%
    \kern 3.150in
  }%
}%

\centerline{\box\graph}
\caption{\em Several classes of event structures\label{classes}}
\end{figure}\vspace{-1ex}

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~\ref{denotational} a denotational semantics of CCSP is
given in terms of event structures with binary conflict. This
semantics follows the standard lines of \cite{Wi87a,Wi89}.
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
{\em action refinement} \cite{GG01}, the choice operators $\Box$ and
$\sqcap$ 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~\ref{all} we show that up to isomorphism
\begin{itemise}
\item every {\em finite} bundle event structure can be denoted by a
recursion-free CCSP expression,
\item every {\em countable} prime event structure with binary conflict
can be denoted by a CCSP expression,
\item and {\em every} bundle event structure can be denoted by a
CCSP expression with an infinitary parallel composition.
\end{itemise}
We also provide a recursive enumerable version of the second result.
The same results can be obtained for the language of \cite{Wi87a,Wi89}.
\vspace{-2ex}

\subsubsection{Denotability up to hereditary history preserving bisimulation equivalence}
The concept of {\em history preserving bisimulation equivalence} stems
from {\sc Rabinovich \& Trakhtenbrot} \cite{RT88} and was adapted to
event structures in {\sc Van Glabbeek \& Goltz} \cite{GG01}. 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 {\em 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~\ref{stable} 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~\ref{conflict} 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 \cite{GV91} for
finite prime event structures. The claim was strengthened in
\cite{GP95} to include infinite ones. The first published proof (for
prime event structures) appears in {\sc Nielsen \& Winskel}
\cite{NW96}, 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 {\em hereditary
history preserving bisimulation equivalence}, which is a finer variant
of history preserving bisimulation equivalence, proposed by {\sc
Bednarczyk} \cite{Bz91}.\vspace{-2ex}

\subsubsection{Denotability up to ST-bisimulation equivalence}

The coarser {\em ST-bisimulation equivalence}, proposed in {\sc Van Glabbeek \&
Vaandrager} \cite{GV87}, respects branching time and the possibility
of actions to overlap in time, but abstracts from the faithful
modelling of causality. By Theorem 1 in {\sc Van Glabbeek \& Plotkin}
\cite{GP95}, 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
ST-bisimulation equivalence every event structure can be denoted by a
CCSP expression.\vspace{-1ex}

\section{Bundle event structures}\label{event structures}

Bundle event structures are introduced in {\sc Langerak} \cite{Lk92}.
Here we add the alphabets for {\em typed} bundle event structures and
generalise the notion to structures with infinite sets of events.

\begin{definition}\rm\label{df-bundle}
A {\em (typed) bundle event structure} is a 5-tuple $\eE =
(E,\#,\mapsto,A,l)$ where
\begin{itemise}
\item $E$ is a set of {\em events},
\item $\# \subseteq E\times E$ is an irreflexive and symmetric
      relation, the {\em conflict relation},
\item $\mapsto\,\subseteq 2^E\times E$ is the {\em bundle set},
      satisfying $X \mapsto e \Rightarrow \forall e_1,e_2\!\in\! X.~ e_1\!\neq\! e_2
      \Rightarrow e_1 \# e_2$,
\item $A$ is a set of {\em actions}, the {\em alphabet} of $\eE$,
\item and $l : E \rightarrow  A$ is the {\it labelling function}.
\end{itemise}
\end{definition}
A bundle event structure represents a concurrent system in the following
way: action names $a \in A$ represent actions the system might
perform and an event $e \in 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 \mapsto 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 $\eE$ will be denoted by
$E_\eE, \#_\eE, \mapsto_\eE, A_\eE$ and $l_\eE$; 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 {\it
configurations}. The causal relationships between events in a
configuration $x$ can be represented by a partial order $<_x$.

\begin{definition}\rm\label{df-configurations}
The set $C(\eE)$ of (finite) {\em configurations} of a bundle event
structure $\eE=(E,\#,\mapsto,A,l)$ consists of those finite $x \subseteq
E$ which are
\begin{itemise}
\item {\em conflict-free}: $\# \cap (x \times x) = \emptyset$,
\item and {\em secured}:\\ $\exists e_1,...,e_n~(n\geq 0)\!:
~x=\{e_1,...,e_{n}\} \wedge \forall i \!<\! n~
(Y \mapsto e_{i+1} \Rightarrow \{e_1,...,e_{i}\}\cap Y \!\neq\! \emptyset)$.
\end{itemise}
The {\em causality relation} $<_x$ on $x \in C(\eE)$ is $\{(d,e) \in x
\times x \mid \exists Y: d \in Y \mapsto e\}^+$.\linebreak[3]
Here $R^+$ denotes the transitive closure of a relation $R$.
\end{definition}
Following \cite{GG01}, 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 \in x \in C(\eE)$ and $Y \mapsto_\eE e$ then $x \cap Y$
has exactly one element. Hence $<_x$ is always a partial order.

We now define the {\em prime} and the {\em stable} event structures
with binary conflict, stemming from {\sc Winskel} \cite{Wi89}, and
show that the bundle event structures can be regarded as a
generalisation of the former and a special case of the latter.
\pagebreak[3]

\begin{definition}\rm\label{df-prime}
A {\em (typed) prime event structure with binary conflict}\\ is a
5-tuple $\eE = (E,<,\#,A,l)$ where 
\begin{itemise}
\item $E$, $A$, and $l$ are as above,
\item $< \;\subseteq E \times E$ is a partial order such that
$\forall e \in E : \{d \in E \mid d < e\} \mbox{ is finite,}$
\item and $\# \subseteq E \times E$ is an irreflexive, symmetric relation
satisfying
$$\forall d,e,f \in E: d < e \wedge d \# f \Rightarrow e \# f.$$
\end{itemise}
\end{definition}
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 \mapsto e ~~\Leftrightarrow~~ X=\{d\} \wedge d<e.$$
The definition of configurations given above is then consistent with
the one in \cite{Wi89}.

\begin{definition}\rm\label{df-stable}
A {\em (typed) event structure with binary conflict}\\ is a 5-tuple $\eE
= (E,\#,\vdash,A,l)$ where
\begin{itemise}
\item $E$, $\#$, $A$, and $l$ are as for bundle event structures,\\
${\it Con} = \{X \subseteq E \mid X$ finite and $d \# e$ for no $d,e\in X\}$
is the {\em consistency predicate},
\item and $\vdash\;\subseteq {\it Con} \times E$ is the {\it enabling
    relation}, satisfying $$X \vdash e \wedge X \subseteq Y \in {\it Con}
    \Rightarrow Y \vdash e.$$
\end{itemise}
$\eE$ is {\em stable} if $Y \vdash e$ implies that there is a least subset
$X$ of $Y$ with $X \vdash e$.
\end{definition}
$X \vdash e$ means that $X$ is a {\it possible cause} of $e$ in the
sense that $e$ can occur only if for certain $Y$ with $Y \vdash e$ all
events in $Y$ have occurred before.

\begin{definition}\rm\label{df-stable-configurations}
The set $C(\eE)$ of (finite) {\em configurations} of an event
structure with binary conflict $\eE=(E,\#,\vdash,A,l)$ consists of those
finite $x \subseteq E$ which are
\begin{itemise}
\item {\em conflict-free}: $\# \cap (x \times x) = \emptyset$, i.e.\ 
$x \in {\it Con}$,
\item and {\em secured}: $\exists e_1,...,e_n~(n\geq 0):
x=\{e_1,...,e_n\} \wedge \forall i < n~ \{e_1,...,e_i\} \vdash e_{i+1}$.
\end{itemise}
The {\em causality relation} $<_x$ on $x$ is
$\{(d,e) \in x \times x \mid \forall Y: Y \vdash e \Rightarrow d \in Y\}^+$.
\end{definition}
The causality relation gives a faithful description of the causal
relations in a configuration only if $\eE$ is stable. As shown in
\cite{Wi87a,Wi89}, 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.

\begin{definition}\rm\label{df-bundle - stable}
Given a bundle event structure $\eE = (E,\#,\mapsto,A,l)$, the {\em
associated} event structure with binary conflict $\fE(\eE)
=(E,\#,\vdash,A,l)$ is given by 
$$X \vdash e
~~\Leftrightarrow~~ X \in {\it Con} \wedge \forall Y\!: (Y\mapsto e
\Rightarrow X\cap Y \neq \emptyset).$$
\end{definition}

\begin{proposition}\label{pr-bundle - stable}
$\fE(\eE)$ is always stable. Moreover, the translation $\fE$ preserves
configurations and the causality relations $<_x$ on them.
\end{proposition}
\begin{proof}Straightforward.\end{proof}

\section{A denotational event structure semantics of CCSP}\label{denotational}

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 {\em variable names}. A {\em variable}
is a pair $X_A$ with $X \in V$ and $A \subseteq Act$.  The syntax of
CCSP is given by
$$P ::= 0_A ~\mbox{\Large $\,\mid\,$}~ aP ~\mbox{\Large $\,\mid\,$}~ P+P
~\mbox{\Large $\,\mid\,$}~ P \| P ~\mbox{\Large $\,\mid\,$}~ R(P) \mbox{\Large
~$\,\mid\,$}~ X_A ~\mbox{\Large $\,\mid\,$}~ \rec{X_A|S}\mbox{ (with }X_A \in V_S)$$
with $A \subseteq Act$, $a \in Act$, $R \subseteq Act \times Act$,
$X \in V$ and $S$ a {\em recursive specification}: a set of equations
$\{X_A = P_{X_A} \mid X_A \in V_S\}$ with $V_S \subseteq V \times Act$
(the {\em bound variables} of $S$) and $\alpha(P_{X_A})=A$ for all
$X_A \in V_S$ (were $\alpha(P_{X_A})$ is defined below).
The constant $0_A$ represents a process that is unable to perform any
action. The process $a P$ 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
$\rec{X_A|S}$ represents the $X_A$-component of a solution of the
system of recursive equations $S$.
A CCSP expression $P$ is {\em closed} if every occurrence of a
variable $X_A$ occurs in a subexpression $\rec{Y_B|S}$ of $P$ with
$X_A \in V_S$. An expression $a0_\emptyset$ is abbreviated $a$.

Just like the version of CSP from {\sc Hoare} \cite{Ho85}, the version
of CCSP used here is a typed language, in the sense that with every
process $P$ an explicit alphabet $\alpha(P) \subseteq 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 {\em typed}
event structures.
The constant 0 and the variables are indexed with an alphabet.
The alphabet of an arbitrary CCSP expression is given by:
\begin{itemise}
\item $\alpha(0_A) = \alpha(X_A) = \alpha(\rec{X_A|S}) = A$
\item $\alpha(aP)  = \{a\} \cup \alpha(P)$
\item $\alpha(P+Q) = \alpha(P \|Q) = \alpha(P) \cup \alpha(Q)$
\item $\alpha(R(P))= \{b \mid \exists a \in \alpha(P): (a,b)\in R\}$.
\end{itemise}\pagebreak[3]
Substitutions of expressions for variables are allowed only if the
alphabets match. For this reason a recursive specification $S$ is
declared syntactically incorrect if $\alpha(P_{X_A}) \neq A$ for some
$X_A \in 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,\#,\mapsto,\vdash,A,l)$, so
that the bundle interpretation is found by dropping $\vdash$, and the
stable interpretation by dropping $\mapsto$. When $\eE$ is an event
structure representing a CCSP expression $P$ then $A_\eE =
\alpha(P)$. Hence we can abstain from explicitly mentioning the
$A$-component in the forthcoming constructions.

\begin{definition}\rm\label{df-event-algebra}The operators of CCSP are
defined on event structures as follows:\\
Inaction: $\eE_{0_A}=(\emptyset,\emptyset,\emptyset,\emptyset,A,\emptyset)$.
\pagebreak[3]\\
Action prefix (for $a\in Act$):
\begin{itemise}
\item $E_{a\eE} = \{a\} \cup \{\hat{a}e \mid e \in E_\eE\}$
\item $l_{a\eE}(a)=a$ and $l_{a\eE}(\hat{a}e)=l_\eE(e)$
\item $\#_{a\eE} = \{(\hat{a}e,\hat{a}e') \mid e \#_\eE e'\}$
\item $\mapsto_{a\eE} = \{(\hat{a}X, \hat{a}e) \mid X\mapsto_\eE e\}
      \cup  \{(\{a\},\hat{a}e) \mid e \!\in\! E_\eE\}$
      in which $\hat{a}X=\{\hat{a}e \mid e \!\in\! X\}$
\item $\vdash_{a\eE}=\{(X,a)\mid X \in {\it Con}_{a\eE}\}
       \cup \{(\hat{a}X \cup \{a\},\hat{a}e) \mid X \vdash_\eE e\}$.
\end{itemise}
Alternative composition:
\begin{itemise}
\item $E_{\eE_1+\eE_2} = \{+_1 e \mid e \in E_{\eE_1}\} \cup
                         \{+_2 e \mid e \in E_{\eE_2}\}$
\item $l_{\eE_1+\eE_2}(+_i e) = l_{\eE_i} (e)$ ($i\!=\!1,2$)
\item $\#_{\eE_1+\eE_2} = \begin{array}[t]{l}
      \{(+_i e,+_ie') \mid e\#_{\eE_i} e',~i\!=\!1,2\} \,\cup\\
      \{(+_i e, +_j f)\mid e\in E_{\eE_i},~f\in E_{\eE_j},~ i\!\neq\! j\}
      \end{array}$
\item $\mapsto_{\eE_1+\eE_2} = \{(+_i X, +_i e) \mid X \mapsto_{\eE_i}e,~i\!=\!1,2\}$
      in which $+_i X = \{+_i e \mid e \in X\}$
\item $\vdash_{\eE_1+\eE_2} = \{(+_i X,+_i e)\mid X\vdash_{\eE_i}e,~i\!=\!1,2\}$.
\end{itemise}
Parallel composition:
\begin{itemise}
\item $E_{\eE\|\eF} = \begin{array}[t]{l}
                      \{(e\|*) \mid l_\eE(e) \not\in A_\eF\} \cup
                      \{(*\|f) \mid l_\eF(f) \not\in A_\eE\}\\ \cup\,
            	      \{(e\|f) \mid l_\eE(e)=l_\eF(f) \in A_\eE \cap A_\eF\}
		      \end{array}$
\item $l_{\eE\|\eF} (e\|*) = l_\eE(e)$,
      $l_{\eE\|\eF} (*\|f) = l_\eF(f)$ and
      $l_{\eE\|\eF} (e\|f) = l_\eE(e) = l_\eF(f)$
\item $\#_{\eE \| \eF} = 
      \{(e\|f,e'\|f') \mid (e\|f\neq e'\|f') \wedge ( e\#_\eE e' \vee
      e\!=\!e'\!\neq\! * \vee f \#_\eF f' \vee f\!=\!f'\!\neq\! *)\}$
\item $\mapsto_{\eE \| \eF} = \{(X\|\eF,e\|f) \mid X \mapsto_\eE e\}
      \cup \{(\eE\|Y,e\|f) \mid Y \mapsto_\eF f\}$\\ in which
      $X\|\eF=\{(e\|f) \in E_{\eE\|\eF} \mid e \in X\}$ and
      $\eE\|Y=\{(e\|f) \in E_{\eE\|\eF} \mid f \in Y\}$
\item $\vdash_{\eE \| \eF} = \{(X,e\|f) \mid (e=* \vee \pi_1(X)
      \vdash_{\eE} e) \wedge (f=* \vee \pi_2(X) \vdash_{\eF} f) \}$\\
      in which $\pi_1(X) = \{e \in E_\eE \mid \exists f\in E_\eF \cup
      \{*\}: e\|f \in X\}$\\
      and  $\pi_2(X) = \{f \in E_\eF \mid \exists e \in E_\eE \cup
      \{*\}: e\|f \in X\}$.
\end{itemise}
Relational renaming (for $R\subseteq Act\times Act$):
\begin{itemise}
\item $E_{R(\eE)} = \{R_b e \mid e \in E_\eE,~(l_\eE(e),b)\in R\}$
\item $l_{R(\eE)}(R_be)=b$
\item $\#_{R(\eE)} = \{(R_b e,R_c e') \mid e \#_\eE e' \vee
      (e=e'\wedge b\neq c)\}$
\item $\mapsto_{R(\eE)} = \{(R(X), R_b e) \mid X\mapsto_\eE e\}$\\
      in which $R(X)=\{R_b e \mid e \in X \wedge (l_\eE(e),b)\in R\}$
\item $\vdash_{R(\eE)}=\{(X,R_be) \mid X \in {\it Con} \wedge
      R^{-1}(X) \vdash e\}$\\ in which
      $R^{-1}(X)=\{e \in E_\eE \mid \exists b\in A_{R(\eE)}: R_be \in X\}$.
\end{itemise}
\end{definition}
The semantics for $0$, $a\eE$, $\eE+\eF$ and $\eE\|\eF$ follows the
lines of \cite{Wi87a,Wi89,BC94,Lk92}.
{\em Relational renaming} appears in \cite{Va93} and \cite{vG94a}. For
every relation $R \subseteq Act \times Act$ there is an operator $R$
that replaces each occurrence of an action $a$ by fresh occurrences
of the actions $\{b \mid aRb\}$. These occurrences are pairwise in
conflict, and inherit their causal relationships from their source.
The {\em relabelling} operators of CCS \cite{Mi89}, CSP \cite{BHR84}
and {\sc Winskel} \cite{Wi89} are special cases where $R$ is a
function; the {\em inverse image operator} of CSP \cite{BHR84} is the
special case where $R$ is the inverse of a function.  In case
$R(a)=\emptyset$, the definition implies that the events labelled
$a$ are removed; thus also the {\em restriction} operators of CCS and
\cite{Wi89} constitute special cases of relational
renaming. Relational renaming in turn is a special case of {\em action
refinement}, as studied for instance in \cite{GG01}. 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 $\rec{X_A|S}$ can be given by
means of least fixed point techniques, see e.g.\ \cite{Wi87a,Wi89}.
The fact that we allow recursive specifications of arbitrary size (in
\cite{Wi87a,Wi89} 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 $\Id{P}$
and a general event structure $\Id{P}_\fE$ for every closed CCSP
expression $P$.  For open CCSP expressions $\Id{P}$ and
$\Id{P}_\fE$ are functions from valuations of the variables to event
structures.

\begin{proposition}\label{pr-closed}
For every CCSP expression $P$ we have $\fE(\Id{P}) = \Id{P}_\fE$.
Hence the bundle event structures, seen as a subclass of the stable
event structures, are closed under the operators of CCSP.
\end{proposition}
\begin{proof} Straightforward with \df{event-algebra}.\end{proof}

\section{Denoting bundle event structures in CCSP}\label{all}

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 $\Id{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 $\eE$ and
$\eF$ are {\em isomorphic} ($\eE \cong \eF$) iff $A_\eE = A_\eF$ and
there exists a bijection between their sets of events preserving
$\mapsto$ (resp.\ $\vdash$), $\#$ 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.

\begin{proposition}\label{pr-iso-cong}{\bf (Congruence)}
Let $\eE,\eE'$ and $\eF$ be event structures with $\eE \cong \eE'$. Then
$a\eE \cong a\eE'$ for $a \in Act$, $~\eE + \eF \cong \eE' + \eF$,
$~\eF + \eE \cong \eF + \eE'$, $~\eE \| \eF \cong \eE' \| \eF$,
$~\eF \| \eE \cong \eF \| \eE'$ and $R(\eE) \cong R(\eE')$ for $R: Act
\rightarrow Act$.
\end{proposition}
\begin{proof} Immediate from the definitions.\end{proof}
The next one, essentially due to {\sc Hoare} \cite{Ho85},
allows us to drop brackets and abstract from the order of components
in nested parallel compositions.

\begin{proposition}\label{pr-associativity}
Let $\eE,\eF$ and $\eG$ be event structures. Then $\eE \| (\eF \| \eG)
\cong (\eE \| \eF) \| \eG$ and $\eE \| \eF \cong \eF \| \eE$.
\end{proposition}
\begin{proof} Straightforward.\end{proof}
Now we are ready to state the main theorems. We start with the
simplest case of finite prime event structures with binary conflict.

\begin{theorem}\label{thm-prime-ccsp}
For every finite prime event structure with binary conflict $\eE$
there is a closed recursion-free CCSP expression $P$ such that
$\Id{P} \cong \eE$.
\end{theorem}

\begin{proof}
As we are interested in $\eE$ only up to isomorphism, w.l.o.g.\ we may
assume that $E_\eE \subset Act$, i.e.\ the names of the events can
also be used as names of CCSP actions. Let $\eE'$ be the variant of
$\eE$ in which every event is labelled by itself. We first build a
CCSP expression denoting $\eE'$ (up to isomorphism), by encoding all
events and all elements of the conflict and causality relation of
$\eE'$ in terms of CCSP constructions. Subsequently, an expression for
$\eE$ is obtained by applying a renaming operator.
Let $E_\eE = \{a_1,...,a_n\}$, $\#_\eE=\{(b_1,c_1),...,(b_m,c_m)\}$
and $<_\eE = \{(d_1,e_1), ...,(d_k,e_k)\}$. Then
$$P = l_\eE\left[a_1 \| \cdots \| a_n \| (b_1+c_1) \| \cdots \| (b_m+c_m) \|
     \rule{0pt}{12pt}(d_1 e_1) \| \cdots \| (d_k e_k)\right] + 0_{A_\eE}.$$
Here $l_\eE$ is not only the labelling function of $\eE$, 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 $\Id{a \| (a+b)} \cong \Id{a+b}$
and $\Id{a \| (ab)} \cong \Id{b \| (ab)} \cong \Id{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 $\eE$ (up to
isomorphism). The term $0_{A_\eE}$ is added in case the alphabet of
$\eE$ contains actions that do not arise as the label of any event.
\end{proof}
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 \cite{BHR84}---as well. The
same cannot be done in CCS \cite{Mi89}, because there only handshaking
communication is available. 

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

\begin{theorem}\label{thm-bundle-ccsp}
For every finite bundle event structure $\eE$ there is a closed
recursion-free CCSP expression $P$ such that $\Id{P} \cong \eE$.
\end{theorem}

\begin{proof}
The proof goes along the same lines as the previous one, except that
instead of causal links $d <_\eE e$ we now have to encode bundles
$X \mapsto_\eE e$. Let $X = \{d_1,...,d_h\}$. Then the bundle $X
\mapsto_\eE 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)\}$.
\end{proof}
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 \mapsto e$ in which all events in $X$
have the same label.  However, there are other process algebraic operators
that can take over the r\^ole of relational renaming.
\pagebreak[3]

\begin{theorem}\label{thm-winskels}
For every finite bundle event structure $\eE$ there is a closed
recursion-free expression $P$ in the language from 
{\sc Winskel \cite{Wi89}} such that $\Id{P} \cong \eE$.
\end{theorem}
\begin{proof}
Winskel's language does not have relational renaming, but only
functional renaming and a restriction operator $\lceil$.
The restriction $\eE \lceil A$ behaves like $\eE$ but with its
events restricted to those with labels which lie in the set $A$.
The parallel composition $\times$ 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,\ast)$, 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 $\times$, 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
$\eE$ in which all actions have a different label and any image finite
relational renaming $R$, define a context $C_{R,\eE} [.]$ in Winskel's
language that behaves like $R$.
In the definition of this context, we use as a derived construct the
{\em interleaving} operator $\interleave$ that is given by
\begin{eqnarray*}
P \interleave Q & = & f (( P \times Q ) \lceil
\{ (a, \ast) \mid a \in \alpha(P) \} \cup
\{ (\ast, b) \mid b \in \alpha(Q) \} ),
\end{eqnarray*}
where $f$ is a functional renaming that renames each action
$(a, \ast)$ into $a$, and each action $(\ast, b)$ into $b$.
Let $\eE$ and $R$ be as stipulated. Now the context $C_{R,\eE} [.]$
can be defined as
\begin{eqnarray*}
C_{R,\eE} [.] & = & g ( ( [.] \times ( a_1 \interleave \cdots \interleave a_n ) ) \lceil R'),
\end{eqnarray*}
where $\{ a_b \mid \exists e \in E_\eE \wedge l_\eE(e)=a \wedge (a,b) \in R \} =
\{ a_1,\ldots a_n \}$, $R'=\{(a,a_b) \mid (a,b) \in R\}$
and $g$ is the functional renaming that renames each action $(a,a_b)$ into $b$.
We claim that $\Id{R(\eE)} = \Id{C_{R,\eE}[\eE]}$ for each bundle
event structure $\eE$ 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
\thm{bundle-ccsp} now yields the required result.
\end{proof}
%
In the presence of sequential composition, such as the operator $;$ in
CSP, a bundle $\{d_1,...,d_h\} \mapsto_\eE e$ can also be represented as
$(d_1 + \cdots + d_h);e$. However, a semantics of $;$ requires the
introduction of a special event-label $\surd$, 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
{\em sequencing} operator \cite{GG01} 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 {\em any}
bundle event structure can be denoted, up to isomorphism, in a variant
of CCSP with a suitable infinitary parallel composition $\|_{i \in 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.

\begin{theorem}\label{thm-prime-countable}
For every countable prime event structure with binary conflict $\eE$
there is a closed CCSP expression $P$ such that $\Id{P} \cong \eE$.
\end{theorem}

\begin{proof}
Although only the binary parallel composition exists in the syntax, a
countable parallel composition $P_0 \| P_1 \| \cdots$ can be created
with infinite unguarded recursion, namely as $\rec{X^0_{A_0}|S}$ where
$S$ contains the equations $X^i_{A_i} = P_i \| X^{i+1}_{A_{i+1}}$
where $A_i = \bigcup_{j \geq i} \alpha(P_j)$, for $i \in
\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 $\Id{\rec{X_A | (X_A \!=\! a \| X_A)}}$.  Thus,
for the generated parallel composition to be useful, we need to
require that for each $a \in A_0$ there is an $i$ with $a \not\in
A_i$, i.e.\ $\bigcap_{i \in \IN} A_i = \emptyset$.\hfill (*)

Now let $E_\eE = \{a_i \mid i\in \IN\}$, where the numbering is chosen
in such a way that $a_i <_\eE a_j \Rightarrow i<j$. As $<_\eE$ is a
partial order in which $\{d \in E \mid d <_\eE e\}$ is finite for all $e
\in E_\eE$, this is always possible.  Then the (possibly infinite)
parallel composition $\| \{a_j \mid a_i <_\eE a_j\}$ contains all
events that have $a_i$ as a causal predecessor, executed in
parallel. Hence $\Id{a_i( \| \{a_j \mid a_i <_\eE 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 \mid j \geq
i\}$.  The parallel composition of all such event structures for $i
\in \IN$ therefore contains all causal links of $\eE$, and satisfies
(*).  This structure is to be put in parallel with one containing all
conflicts, constructed in a similar way. As $\#_\eE$ is irreflexive
and symmetric, we only need to implement the conflicts $a_i \#_\eE
a_j$ with $i < j$. We find that $\eE$ is denoted by\\[2ex]\mbox{}\hfill 
$P = l_\eE \left[ \mbox{ \Large$\|$}_{i=0}^\infty
(a_i( \| \{a_j \mid a_i <_\eE a_j\}) \| \mbox{ \Large$\|$}_{i=0}^\infty
(a_i + \| \{a_j \mid j>i \wedge a_i \#_\eE a_j\}) \right] + 0_{A_E}$
\end{proof}
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 \subseteq
Act \times Act$ for which there exists a Turing machine enumerating
all pairs $(a,b) \in 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$^{\rm r.e.}$, by
requiring
\begin{itemise}
\item that Act is a r.e.\ set and all renaming operators are r.e.,
\item that only r.e.\ subsets of Act are allowed as indices of 0 and
      the variables.
\item and that recursive specifications $S$, seen as functions from
$V_S$ to the CCSP expressions, should be {\em primitive recursive},
with $V_S$ a primitive decidable set.
\end{itemise}
This makes the signature of the language decidable. The primitive
recursive requirement on $S$ even makes it decidable whether a
variable in a CCSP$^{\rm r.e.}$ expression is free \cite{vG94a}.
% It should be admitted, however, that in this setting it is still not
% decidable whether a string is a well-formed CCSP expression, because the
% condition $\alpha(P_{X_A})=A$ for the well-formedness of recursive
% specifications is undecidable. If this is felt to be a problem, one
% could declare such specifications syntactically correct, and define
% the value of corresponding expressions $\rec{X_A|S}$ to be 0.
Now we have the following recursive enumerable version of
\thm{prime-countable}:

\begin{theorem}\label{thm-r.e.}
Let $\eE$ be a prime event structure with binary conflict such that
$E_\eE$, $\#_\eE$, $<_\eE$, $A_\eE$ are recursive enumerable sets,
$l_\eE$ 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$^{\rm r.e.}$ expression $P$ such that
$\Id{P} \cong \eE$.
\end{theorem}

\section{Denoting stable event structures with binary conflict in CCSP}\label{stable}

In this section we infer from \thm{prime-countable} that up to
hereditary history preserving bisimulation equivalence any countable
stable event structure with binary conflict can be denoted by a closed
CCSP expression.

\begin{definition}\rm\label{df-hpb} Two stable event structures $\eE$ and $\eF$
are {\it history preserving bisimulation equivalent} ($\eE \bis{h}
\eF$) iff $A_\eE = A_\eF$ and there exists a relation $R \subseteq
C(\eE) \times C(\eF) \times {\pow}(E_\eE \times E_\eF)$---called a
{\it history preserving bisimulation}---such that
$(\emptyset,\emptyset,\emptyset) \in R$ and whenever $(x, y, f) \in R$
then
\begin{itemise}
\item
$f$ is an isomorphism between
$(x, <_x, l_{\eE} \rest x)$ and $(y, <_y, l_{\eF} \rest y)$,
\item
$x \subseteq x' \in C(\eE) \Rightarrow \exists y',f'$
with $y \subseteq y' \in C(\eF)$,
$(x',y',f') \!\in\! R$ and $f' \!\rest x\hspace*{-1mm}=\hspace*{-1mm}f$,
\item
$y \subseteq y' \in C(\eF) \Rightarrow \exists x',f'$
with $ x \subseteq x' \in C(\eE)$,
$(x',y',f') \!\in\! R$ and $f' \!\rest x \hspace*{-1mm}=\hspace*{-1mm}f$.
\end{itemise}
The bisimulation and the equivalence are {\em hereditary} ($\eE
\bis{hh} \eF$) if moreover
\begin{itemise}
\item
$x \supseteq x' \in C(\eE) \Rightarrow \exists y',f'$
with $y \supseteq y' \in C(\eF)$,
$(x',y',f') \!\in\! R$ and $f'\hspace*{-1mm}=\hspace*{-1mm}f \!\rest x'$,
\item
$y \supseteq y' \in C(\eF) \Rightarrow \exists x',f'$
with $ x \supseteq x' \in C(\eE)$,
$(x',y',f') \!\in\! R$ and $f'\hspace*{-1mm}=\hspace*{-1mm}f \!\rest x'$.
\end{itemise}
$R$ is {\em functional} if $R=\{(x,f(x),f\rest x) \mid x \in C(\eE)\}$
for a function $f\!:E_\eE \rightarrow E_\eF$.
\end{definition}
Note that a functional bisimulation is always hereditary. Moreover,
when checking that a function $f:E_\eE \rightarrow E_\eF$ induces an
history preserving bisimulation, the second requirement is trivially fulfilled.
{\sc Joyal, Nielsen \& Winskel} \cite{JNW96} characterised a
functional history preserving bisimulation as a categorical
construction called {\em open map}.

\df{hpb} also applies when $\eE$ and $\eF$ 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.

\begin{definition}
Given a stable event structure $\eE = (E,\#,\vdash,A,l)$ with binary
conflict, the associated prime event structure
$\eE' = (E',<,\#',A,l')$ is given by
\begin{itemise}
\item $E' = \{e_x \mid e \in x \in C(\eE)$ and $x$ is a minimal
      configuration containing $e \}$,
\item $d_x < e_y$ iff $x \subset y$,
\item $d_x \#' e_y$ iff $\eE$ has no configuration containing both $x$ and $y$,
\item $l'(e_X) = l(e)$.
\end{itemise}
\end{definition}
$\eE'$ is obviously a prime event structure with binary conflict, and
if $\eE$ is countable, then so is $\eE'$. 
Moreover, it is not too hard to check that the function $f:E' \rightarrow E$
given by $f(e_X)=e$ for $e \in 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 \cite{JNW96}. In view of this,
\thm{prime-countable} implies\pagebreak[3]

\begin{theorem}\label{thm-stable-binary-countable}
For every countable stable event structure with binary conflict $\eE$
there is a closed CCSP expression $P$ such that $\Id{P} \bis{hh} \eE$.
\end{theorem}

\section{Arbitrary conflict reduces to binary conflict}\label{conflict}

In \cite{Wi87a} event structures of the form $(E,Con,\vdash,A,l)$
appear, in which the predicate $Con$ of \df{stable} 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 \df{stable-configurations}.
Note that $Con$ can equivalently be represented by its complement:
an upwards closed set {\sc Confl} of finite nonempty sets of events.
Another equivalent representation is in terms of the minimal members
of {\sc Confl}: a collection $\#$ of finite nonempty sets of events,
such that there are no two different $\gamma,\gamma' \in \#$ with
$\gamma \subset \gamma'$. Now a finite set $x$ is {\em consistent} or
{\em conflict-free} if $\gamma \subseteq x$ for no $\gamma \in \#$.
In this representation event structures with a binary conflict
relation are literally a special case of the ones with arbitrary
conflict relations. Statement $\gamma \in \#$ means that the events in
$\gamma$ cannot {\em all} happen in the same run. It does not place a
restriction on proper subsets of $\gamma$.

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
\cite{GV91}. The generalisation to infinite event structures was
reported in \cite{GP95}. The same theorem has been discovered
independently by {\sc Nielsen \& Winskel} \cite{NW96}, where the first
published proof can be found. Although our proof is based on the same
idea as the one of \cite{NW96}, it is somewhat shorter and more constructive.

\begin{definition}\rm\label{df-conflict}
Let $\eE$ be a countable event structure with arbitrary conflict. For $e \in
E_\eE$ let $\#_e$ be the set of conflicts involving $e$: $\#_e =
\{\gamma \in \#_\eE \mid e \in \gamma\}$.
Define the event structure $2(\eE)$ by
\begin{itemise}
\item $E_{2(\eE)} = \{(e,t) \!\mid\! e \!\in\! E_\eE,\,t\!:\#_e \!\rightarrow\! \IN$
     with $t$ recursive and $\forall \gamma \!\in\! \#_e\!: t(\gamma) < |\gamma|\!-\!1\}$
\item $A_{2(\eE)} = A_\eE$ and $l_{2(\eE)}(e,t)=l_\eE(e)$
\item $\#_{2(\eE)} = \{((e,t),(e',t')) \mid (e=e' \wedge t \neq t') \vee
      (e\neq e'\wedge \exists \gamma \in \#_e: t(\gamma) = t'(\gamma))\}$
\item $\mapsto_{2(\eE)} = \{(2(X),(e,t)) \mid X\mapsto_\eE e\}$
      in which $2(X)=\{(e,t) \mid e \in X \}$
\item $\vdash_{2(\eE)}=\{(X,(e,t)) \mid \pi_1(X) \vdash e\}$ in which
      $\pi_1(X)=\{e \in E_\eE \mid \exists t: (e,t) \in X\}$.
\end{itemise}
\end{definition}
The idea behind this definition is the following: every member
$\gamma$ of the conflict relation on $\eE$ has $|\gamma|$ elements, of
which only $|\gamma|-1$ can be executed. This can be modelled as an
allocation of $|\gamma|-1$ seats to $|\gamma|$ events. Let us number
these seats from 0 to $|\gamma|-2$.  The event that is last in
grabbing a seat can not happen. In general an event can occur in many
elements $\gamma$ of $\#_\eE$, namely the ones in $\#_e$.  In order to
happen it has to grab a seat for each of these $\gamma$'s. Now
$2(\eE)$ 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 $\gamma \in \#_e$ in which $e$ participates
selects a seat $t(\gamma)<|\gamma|-1$. In \cite{NW96} a pair $(e,t)$
is called an event with a {\em 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 $\mapsto_{2\eE}$ or $\vdash_{2\eE}$,
depending on whether the original event structure was a bundle, or a
general one. Compare these definitions with the relational renaming
operator in Section~\ref{denotational}.  The conflict relation on
$2(\eE)$ 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 $\eE$.

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 \rightarrow \IN$ is {\em recursive} if there is a
partial recursive function $t':\pow_{\it fin}(E_\eE) \rightarrow \IN$ with
$t=t'\rest \#_e$ a total function. There is no need to assume that
$\#_e$ is a decidable set.)
The resulting requirement in \df{conflict} that all functions $t$
should be recursive, ensures that $2(\eE)$ is still countable. Without
the recursiveness requirement this would not be the case.

\begin{theorem}\label{thm-conflict}
Let $\eE$ be a countable stable event structure.  Then $2(\eE)$ is a
countable stable event structure with binary conflict and the function
$f:2(\eE) \rightarrow \eE$ given by $f(e,t)=e$ induces a history
preserving bisimulation.  Hence $2(\eE) \bis{hh} \eE$.
\end{theorem}

\begin{proof}
As $(e,t) \#_{2(\eE)} (e,t')$ for $t \neq t'$, it follows immediately
that $f\rest x$ is injective for every configuration $x$. Now suppose
$f(x)$ contains a conflict $\gamma \in \#_\eE$. Then in $x$ there must
be events $\{(e_i,t_i) \mid e_i \in \gamma\}$ with $t(e_i) <
|\gamma|-1$. Hence two of these events must be in conflict,
contradicting that $x$ is a configuration. If follows that $f(x)$ is
conflict-free. It is immediate from the definition of
$\mapsto_{2(\eE)}$ resp.\ $\vdash_{2\eE}$ that if
$(e_1,t_1),...,(e_n,t_n)$ secures $x$ in $2(\eE)$ then $e_1,...,e_n$
secures $f(x)$. Hence $x$ is a configuration of $\eE$. It is also
immediate from the definition of $\mapsto_{2(\eE)}$ resp.\
$\vdash_{2\eE}$ that $f$ preserves $<_x$ and labelling.

Now suppose $x \in C(2(\eE))$ and $f(x) \subseteq y' \in C(\eE)$. We
need to show that there is an $x' \in C(2(\eE))$ with $x \subseteq 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 $\gamma \in \#_e$
we have that $|\gamma \cap f(x)|\leq |\gamma|-2$. Hence there exists a
recursive $t: \#_e \rightarrow \IN$ satisfying, for all $\gamma \in
\#_e$, $t(\gamma) < |\gamma|-1$ and for no $(e',t') \in x$:
$t'(\gamma) = t(\gamma)$. It follows that $x' \stackrel{\rm def}{=} x
\cup \{(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 $\mapsto_{2(\eE)}$ resp.\ $\vdash_{2\eE}$.
Thus $x' \in C(2(\eE))$, which had to be proved. The other requirement
for $f$ inducing a history-preserving bisimulation is trivial.
\end{proof}
By combining this insight with \thm{stable-binary-countable}
it follows immediately that up to hereditary history preserving
bisimulation equivalence all countable stable event structures with
arbitrary conflicts are expressible in CCSP.

\subsubsection{Acknowledgement}
Thanks to Rom Langerak for valuable feedback.

%\bibliography{/uf/rvg/lib/abbreviations,/uf/rvg/lib/dbase,/uf/rvg/lib/new}
\begin{thebibliography}{10}
\small
\bibitem{Bz91}
{\sc M.~Bednarczyk} (1991):
\newblock {\em Hereditary history preserving bisimulation, or what is the power of the future perfect in program logics.}
\newblock Technical report, Polish Academy of Sciences, Gda\'nsk.
\newblock Available at {\tt ftp://ftp.ipipan.gda.pl/marek/historie.ps.gz}.

\bibitem{BC94}
{\sc G.~Boudol \& I.~Castellani} (1994):
\newblock {\em Flow models of distributed computations: Three equivalent semantics for {CCS}.}
\newblock {\sl Information and Computation} 114(2), pp. 247--314.

\bibitem{BHR84}
{\sc S.D. Brookes, C.A.R. Hoare \& A.W. Roscoe} (1984):
\newblock {\em A theory of communicating sequential processes.}
\newblock {\sl Journal of the ACM} 31(3), pp. 560--599.

\bibitem{vG94a}
{\sc R.J.~van Glabbeek} (1994):
\newblock {\em On the expressiveness of {ACP} (extended abstract).}
\newblock In A.~Ponse, C.~Verhoef \& S.F.M. van Vlijmen, editors: {\sl
{\rm Proceedings First Workshop on the} Algebra of Communicating Processes, {\rm ACP94, Utrecht}}, Workshops in Computing, Springer, pp. 188--217.
\newblock Available at {\tt http://boole.stanford.edu/pub/acp.ps.gz}.

\bibitem{GG01}
{\sc R.J.~van Glabbeek \& U.~Goltz} (2001):
\newblock {\em Refinement of actions and equivalence notions for concurrent systems.}
\newblock {\sl Acta Informatica} 37, pp. 229--327.

\bibitem{GP95}
{\sc R.J.~van Glabbeek \& G.D. Plotkin} (1995):
\newblock {\em Configuration structures (extended abstract).}
\newblock In D.~Kozen, editor: {\sl {\rm Proceedings $10^{th}$ Annual IEEE Symposium on} Logic in Computer Science {\rm (LICS95), San Diego, USA}}, IEEE Computer Society Press, pp. 199--209.

\bibitem{GV87}
{\sc R.J.~van Glabbeek \& F.W. Vaandrager} (1987):
\newblock {\em Petri net models for algebraic theories of concurrency (extended abstract).}
\newblock In J.W.~de Bakker, A.J. Nijman \& P.C. Treleaven, editors: {\sl {\rm Proceedings} PARLE, Parallel Architectures and Languages Europe, {\rm Eindhoven, The Netherlands, June 1987, Vol. II: Parallel Languages}}, {\sl \rm LNCS} 259, Springer, pp. 224--242.

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

\bibitem{Ho85}
{\sc C.A.R. Hoare} (1985):
\newblock {\em Communicating {S}equential {P}rocesses}.
\newblock Prentice Hall. %, Englewood Cliffs.

\bibitem{JNW96}
{\sc A.~Joyal, M.~Nielsen \& G.~Winskel} (1996):
\newblock {\em Bisimulation from open maps.}
\newblock {\sl Information and Computation} 127(2), pp. 164--185.

\bibitem{Lk92}
{\sc R.~Langerak} (1992):
\newblock {\em Transformations and Semantics for LOTOS}.
\newblock PhD thesis, Department of Computer Science, University of Twente.

\bibitem{Mi89}
{\sc R.~Milner} (1989):
\newblock {\em Communication and Concurrency}.
\newblock Prentice Hall, Englewood Cliffs.

\bibitem{NPW81}
{\sc M.~Nielsen, G.D. Plotkin \& G.~Winskel} (1981):
\newblock {\em Petri nets, event structures and domains, part {I}.}
\newblock {\sl Theoretical Computer Science} 13(1), pp. 85--108.

\bibitem{NW96}
{\sc M.~Nielsen \& G.~Winskel} (1996):
\newblock {\em Petri nets and bisimulation.}
\newblock {\sl Theoretical Computer Science} 153, pp. 211--244.

\bibitem{RT88}
{\sc A.~Rabinovich \& B.A. Trakhtenbrot} (1988):
\newblock {\em Behavior structures and nets.}
\newblock {\sl Fundamenta Informaticae} 11(4), pp. 357--404.

\bibitem{Va93}
{\sc F.W. Vaandrager} (1993):
\newblock {\em Expressiveness results for process algebras.}
\newblock In J.W. de~Bakker, W.P.~de Roever \& G.~Rozenberg, eds.: {\sl Proc. REX Workshop on Semantics: Foundations and Applications, {\rm Beekbergen, The Netherlands, June 1992}}, {\sl \rm LNCS} 666, Springer, pp. 609--638.

\bibitem{Wi87a}
{\sc G.~Winskel} (1987):
\newblock {\em Event structures.}
\newblock In W.~Brauer, W.~Reisig \& G.~Rozenberg, editors: {\sl Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, {\rm Bad Honnef, September 1986}}, {\sl \rm LNCS} 255, Springer, pp. 325--392.

\bibitem{Wi89}
{\sc G.~Winskel} (1989):
\newblock {\em An introduction to event structures.}
\newblock In J.W. de~Bakker, W.P.~de Roever \& G.~Rozenberg, editors: {\sl REX School and Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, {\rm Noordwijkerhout, The Netherlands, May/June 1988}}, {\sl \rm LNCS} 354, Springer, pp. 364--397.

\bibitem{WN94}
{\sc G.~Winskel \& M.~Nielsen} (1995):
\newblock {\em Models for concurrency.}
\newblock In S.~Abramsky, D.~Gabbay \& T.~Maibaum, editors:
{\sl Handbook of Logic in Computer Science}, Oxford University Press, pp. 1--148.\vspace{-1em}

\end{thebibliography}
\end{document}
