\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 di \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}