\documentclass[12pt]{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% This format is suited for printing on A4 paper. It leaves %%%%
%%%% 2.5 cm space right and left of the text. On American paper %%%%
%%%% the right margin is 6 mm larger. The bottem margin (3.3cm) %%%%
%%%% is rather large, so that still 1.5 cm is left wenn printed %%%%
%%%% on American paper. -Rob van Glabbeek %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\unitlength 1mm % this is used in pictures %
\textwidth 16cm % A4 width is 21cm %
\oddsidemargin -0.04cm % +1 inch = 2.5cm %
\evensidemargin -0.04cm % +1 inch = 2.5cm %
\marginparwidth 1.8cm % only ... left to the edge %
\textheight 22.5cm % A4 height is 29.7cm. %
\topmargin -1cm % +1 inch +37 pt (empty) head %
% footer with pagenumber 30pt %
\parindent 0pt % paragraphs not indented ... %
\parskip 8pt plus 2pt minus 1 pt % but some space between them %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% The following implements a layout and numbering convention %%%%
%%%% chosen by Ursula Goltz. All theorem-like environments are %%%%
%%%% indented and in roman. Numbering of theorems, propositions %%%%
%%%% etc. happens seperately and by section. All environments %%%%
%%%% have two arguments: a label for future reference, and a %%%%
%%%% header for basic assumptions like "Let S be a set". -Rob %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{defi}{Definition}[section]
\newtheorem{theo}{Theorem}[section]
\newtheorem{prop}{Proposition}[section]
\newtheorem{lemm}{Lemma}[section]
\newtheorem{coro}{Corollary}[section]
\newtheorem{exam}{Example}[section]
\newtheorem{obs}{Observation}
\newenvironment{definition}[2]{\begin{defi} \rm \label{df-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{defi}}
\newenvironment{definitioni}[2]{\begin{defi} \rm \label{df-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em}}{\end{itemize}\end{defi}}
\newenvironment{theorem}[2]{\begin{theo} \rm \label{thm-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{theo}}
\newenvironment{proposition}[2]{\begin{prop} \rm \label{pr-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{prop}}
\newenvironment{propositioni}[2]{\begin{prop} \rm \label{pr-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em}}{\end{itemize}\end{prop}}
\newenvironment{lemma}[2]{\begin{lemm} \rm \label{lem-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{lemm}}
\newenvironment{corollary}[2]{\begin{coro} \rm \label{cor-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{coro}}
\newenvironment{corollaryi}[2]{\begin{coro} \rm \label{cor-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em}}{\end{itemize}\end{coro}}
\newenvironment{example}[2]{\begin{exam} \rm \label{ex-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{exam}}
\newenvironment{observation}[1]{\begin{obs} \rm \label{obs-#1}}{\end{obs}}
\newcommand{\df}[1]{Definition~\ref{df-#1}}
\newcommand{\thm}[1]{Theorem~\ref{thm-#1}}
\newcommand{\pr}[1]{Proposition~\ref{pr-#1}}
\newcommand{\lem}[1]{Lemma~\ref{lem-#1}}
\newcommand{\cor}[1]{Corollary~\ref{cor-#1}}
\newcommand{\ex}[1]{Example~\ref{ex-#1}}
\newcommand{\ob}[1]{Observation~\ref{obs-#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\kasten}{\hfill \rule{2.5mm}{2.5mm} } % end-of-proof box
\newenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf
Proof\ \ ]}{\mbox{}\kasten\end{trivlist}}
\newenvironment{notation}[1]{\begin{trivlist} \item[\hspace{\labelsep}\bf
Notation\ \ ] \mbox{#1}\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{trivlist}}
\newenvironment{itemise}{\begin{list}{$\bullet$}{\leftmargin 18pt
\labelwidth\leftmargini\advance\labelwidth-\labelsep
\topsep 4pt \itemsep 2pt \parsep 2pt}}{\end{list}}
\newcommand{\remark}[1]{\marginpar{\raggedright \scriptsize \it #1}}
\newcommand{\conf}{{\it Conf}} % configurations
\newcommand{\reff}{{\it ref}} % refinement
\newcommand{\fR}{{\cal R}} % reachable part
\newcommand{\eC}{{\cal C}} % confguration str.
\newcommand{\eD}{{\cal D}} % confguration str.
\newcommand{\eE}{{\cal E}} % event structure
\newcommand{\eF}{{\cal F}} % event structure
\newcommand{\si}[1]{#1} % notation from [GG]
\newcommand{\db}[1]{\mbox{
\begin{picture}(3,3)
\put(-1,0){$I$}
\put(-.5,0){$#1$}
\end{picture}} }
\newcommand{\lra}{
\begin{picture}(7.5,1)
\put(1,1){\vector(1,0){6}}
\end{picture} }
\newcommand{\mathdis}[3]
{\mathrel{\mathop{#2}\limits^{#1}_{#3}}}
\begin{document}
\bibliographystyle{plain}
\vspace*{1cm minus .3cm}
\begin{center}
{\Large \bf Well-behaved Flow Event Structures\\\vspace{3mm} for
Parallel Composition and Action Refinement} \vspace{1cm}\\ Rob van
Glabbeek\\ \footnotesize Computer Science Department, Stanford
University\\ Stanford, CA 94305-9045, USA.\\ {\tt
rvg@cs.stanford.edu} \vspace{1cm}\\ \normalsize Ursula Goltz\\
\footnotesize Institut f\"ur Software, Technische Universit\"at
Braunschweig\\ Postfach 3329, D-38106 Braunschweig, Germany.
\\ {\tt U.Goltz@tu-bs.de}
\end{center}
\vspace{4em minus 1.5em}
{\footnotesize Flow event structures were introduced as a model
for giving semantics to process algebras. However it turned out
that certain restrictions have to be made to make them suitable
for this purpose. In this paper, we investigate subclasses of flow
event structures which are both suited for the process algebraic
composition operators, and for action refinement as a means of
regarding processes on different levels of abstraction.
First, suitable subclasses are characterised. Then two specific
subclasses are proposed. The larger class generalises the one from
\cite{CZ}, which is not suitable for action refinement. The
smaller one is still sufficiently expressive for dealing with all
standard process algebras and action refinement.
\vspace{2em minus .6em}
{\normalsize\bf Keywords\ } Concurrency, flow event structures,
parallel composition, action refinement.
}
\section*{Introduction} Flow event structures were introduced in
\cite{BC-b} as a model of concurrency that is particularly suited for
giving semantics to languages like CCS and CSP, while faithfully
representing causality and branching time. Indeed, the interpretation
of the operators of such languages in terms of flow event structures
is particularly straightforward and intuitive \nocite{BC-c}[BC-a/b].
Structurally, flow event structures closely resemble prime event
structures \cite{NPW}. However, prime event structures are not as
suitable for defining parallel composition operators with
synchronisation. Flow event structures were proposed as a canonical
generalisation of prime event structures suitable for defining
parallel composition (besides all other CCS-like operators).
However, in \cite{CZ} it turned out that the definition of parallel
composition on flow event structures, although seemingly intuitive,
does not always give the desired result. Technically, the problem can
be pinpointed by the failure of parallel composition to correspond
with the product in a suitable category of event structures, or ---
alternatively --- as a failure of compositionality: the behaviour of
the parallel composition of two flow event structures, as given by its
family of configurations, is not determined by the behaviours of its
two arguments.
This problem was solved in \cite{CZ} by defining a subclass of
flow event structures, closed under the operators of CCS, on which
parallel composition is well-behaved. The subclass consists of
those flow event structures which satisfy a complicated structural
property, called $\Delta $.
In \cite{GG} we defined an operator for action refinement on flow
event structures and other causality based, event oriented models
of concurrency. This operator describes a change in the level of
abstraction at which a system is represented by interpreting
actions on a higher level by more complicated processes on a lower
level. On flow event structures, this operator could be defined
in a much more straightforward and intuitive way than on competing
models like stable (or bundle) event structures or Petri
nets.\footnote{In \cite{DD}, the model of \emph{free event
structures} is shown to be equally suitable as flow event
structures for defining action refinement. However, like prime
event structures, they are not very suitable for defining parallel
composition with synchronisation.} Action refinement turned out to
behave compositionally on the entire domain of flow event
structures.
In order to interpret both parallel composition and action
refinement (and the other CCS-like operators) on flow event
structures, it therefore seems appropriate to restrict attention
to the flow event structures satisfying $\Delta$. However, it
turns out that this class is not closed under action refinement.
Therefore, in this paper our aim is to define a different subclass
of flow event structures, closed under action refinement, parallel
composition and the other CCS-like operators, on which parallel
composition still behaves well.
In \cite{Winskel} a general parallel composition operator is
proposed that is parameterised by the choice of a so-called
\emph{synchronisation algebra}. Depending on the choice of this
parameter, the parallel composition operators of CCS, CSP, SCCS,
ACP and many other system description languages can be obtained.
Other process algebraic operators like choice, sequential
composition, restriction, renaming etc.\ may be expressed in terms
of action refinement. Therefore, it is sufficient to check closure
under, and compositionality of, Winskel's general parallel
composition operator and action refinement; the same properties
then hold for many other process algebraic operators, including
the ones of CCS.
In this paper, we consider the parallel product of Winskel
underlying his parallel composition operator on the domain of
unlabelled flow event structures. The various instances of
Winskel's parallel composition operator can be expressed in terms
of labelled versions of this parallel product and restriction.
Accordingly we consider event refinement as the corresponding
operator underlying action refinement. In
Section~\ref{requirements} of this paper we formalise when
parallel product is {\em well-behaved} on a subclass of flow event
structures. We infer that parallel product is the categorical
product in a suitable category of flow event structures if and
only if that operator is well-behaved on that class. Moreover, as
we show in Section~\ref{compositionality}, parallel product is
compositional on any class of flow event structures on which it is
well behaved. This implies that parallel composition is
compositional on the labelled counterpart of such a class. The
compositionality of the other CCS-like operators on such a class
follows from the compositionality of action refinement.
It remains to find a class of flow event structures, closed under
parallel product and event refinement, on which parallel product
is well behaved.
In fact, two such subclasses are proposed in
Section~\ref{solution}. The larger class turns out to contain all
flow event structures satisfying $\Delta$. The smaller one is
still sufficiently expressive for dealing with all standard
process algebras and action refinement. These classes will be
proposed in Section~\ref{solution} by introducing a semantic
concept of \emph{(fairly) well-behaved flow event structures}.
\newpage
\section{Basic notions}\label{flow}
In this section, we introduce flow event structures and operators for
event refinement and parallel composition.
%\subsection{Flow event structures}
A flow event structure describes a concurrent system as a set of
\emph{events}, modelling action occurrences, together with two
relations: the \emph{flow relation} represents ``possible immediate
causes'' of events; the \emph{conflict relation} expresses which
events mutually exclude each other.
\begin{definition}{flow}{ }
A {\it flow event structure}
\index{flow event structures}%
\index{event structures!flow}%
is a triple
${\cal E} = (E, \prec, \#)$ where
\\--
$E$ is a set of {\it events},
\index{event}%
\\--
$\prec \; \subseteq E \times E$ is an irreflexive relation (the {\it flow
\index{flow relation}%
relation}),
\\--
$\# \subseteq E \times E$ is a symmetric relation (the {\it conflict
\index{conflict relation}%
relation}).
\end{definition}
\index{graphical representations!of flow event structures}%
In graphical representations of flow event structures we represent
$\prec$ by arcs of the form $\lra\!\!\!-\!\!\!-\!\!\!-$.
% A self-conflicting event $d$ is denoted \raisebox{-3pt}
% {\begin{picture}(5,5)\put(0,0){\dashbox{1}(5,5){$d$}}\end{picture}}.
Let $\db{E}$ denote the domain of flow event
structures. The components of a flow event
structure ${\cal E} \in \db{E}$ will be denoted by
$E_{\cal E}$, $\prec_{\cal E}$ and $\#_{\cal E}$
--- a convention that will also apply to other structures given as tuples.
If clear from the context, the index ${\cal E}$ will be omitted.
$O$ denotes the empty flow event structure
\index{empty process}%
\index{event structures!empty}%
$(\emptyset,\emptyset,\emptyset)$.
The interpretation of the conflict and the flow relation is formalised
by defining which subsets of events constitute possible runs of the
represented system, and which of these runs terminate successfully.%
\footnote{As explained in \cite{GG}, the notion of successful
termination is necessary for dealing with event refinement.}
These subsets are called \emph{configurations} (\emph{terminated
configurations}, resp.). Since in Section \ref{solution} we will introduce
weaker notions of configuration, we will call these original configurations
\emph{strong}.
% They have to be conflict-free; in particular, self-conflicting events will
% never occur in any configuration. $d \prec e$ means that $d$ is a {\it
% possible immediate cause} for $e$. For an event to occur it is necessary that
% a \index{complete set of causes}%
% {\it complete} non-conflicting set of
% its causes has occurred. Here a set of
% causes is complete iff for any cause which is not contained there is a
% conflicting event which is contained. Finally, no cycles with respect
% to causal dependence may occur.
\begin{definitioni}{flow-conf}{Let ${\cal E} \in \db{E}$.}
\item[(i)]
$X \subseteq E$ is {\em cycle-free in} ${\cal E}$ iff $(\prec \cap (X \times X))^{+}$ (where $^+$
denotes transitive closure) is irreflexive.\\
\index{conflict-free}%
$X \subseteq E$ is {\em conflict-free in} ${\cal E}$ iff $\#
\cap (X \times X) = \emptyset$.
\item[(ii)]
\index{configuration}%
$X \subseteq E$ is a {\it (strong) configuration} of ${\cal E}$ iff $X$
is finite, cycle-free, conflict-free and \emph{(strongly) left-closed up
to conflicts}: \index{left-closed up to conflicts}%
$\forall d,e \in E :$ if $e \in X$, $d \prec e$ and $ d \not\in X$ then
there exists an $f \in X$ with $d \# f$ and $f \prec e$.
\index{causality cycle}%
\index{causality relation}%
\index{causality}%
\index{configuration!terminated}%
A configuration $X$ is called {\it terminated} iff $\forall d \in E: d
\notin X\Rightarrow \exists e \in X$ with $d\#e$.\\
{\it Conf} $({\cal E})$ denotes the set of all configurations of
${\cal E}$, and $\surd({\cal E})$ the set of all terminated
configurations of $\eE$.
\end{definitioni}
In \cite{GG} we have shown that the notion of successful termination
derived from the structural properties of flow event structures in the
above definition is compatible with our notions of event refinement
and sequential composition.
The behaviour of a flow event structure may be expressed in terms of a
general and more abstract event oriented model of concurrent systems, in
which a system is represented merely by its set of configurations and a
termination predicate.
\begin{definitioni}{configuration structures}{\cite{GG}}
\item[(i)]
A \emph{configuration structure}
is a pair ${\cal C}=(C,\surd)$ where $C$ is a
family of finite sets (the {\it configurations}) and
$\surd \subseteq C$ a {\em termination predicate}, satisfying
$X \!\in\! \surd \wedge X \!\subseteq\! Y \!\in\! C_\eC$ $\Rightarrow X=Y$
(i.e.\ terminating configurations must be maximal).
% $e \not\in X \in \surd \Rightarrow X\cup \{e\} \not\in C$,
\item[(ii)]
The \emph{configuration structure of} ${\cal E} \in I\!\!E$
is defined as ${\cal C}({\cal E}) :=(\conf({\cal E}),\; \surd({\cal E})).$
\end{definitioni}
The set $E_{\cal C}$ of {\it events} of a configuration structure
${\cal C}$ is defined by $E_{\cal C} := \mathdis{}{\bigcup}{X
\in C_{\cal C}} X$.
%\subsection{Parallel product}
Next we define the parallel product ${\cal E} \times {\cal F}$ as in
\cite{CZ} for flow event structures ${\cal E}$ and ${\cal F}$.
It represents the independent execution of events of ${\cal E}$ and ${\cal
F}$, where moreover each pair of events of $d \in E$ and $e \in F$ may
synchronise (thereby excluding the independent occurrence of $e$ and
$f$ and their synchronisation with other events).
\begin{definitioni}{product}{Let ${\cal E}, {\cal F} \in \db{E}$.}
\item[(i)]
The \emph{(partially synchronous) parallel product} ${\cal E}
\times {\cal F}$ is defined by
\\--
$E_{{\cal E} \times {\cal F}} = (E_{\cal E} \times \{*\}) \cup
(\{*\} \times E_{\cal F}) \cup (E_{\cal E} \times E_{\cal F}),$
\\--
$(d,d') \prec_{{\cal E} \times {\cal F}}(e,e')$
iff $d \prec_{\cal E} e$ or $d' \prec_{\cal F} e',$
\\--
$(d,d') \;\#_{{\cal E} \times {\cal F}}\; (e,e')$ iff
$d \;\#_{\cal E}\; e$ or $d' \;\#_{\cal F}\; e'$ or\\
\hspace*{4cm}
$(d = e \neq * \wedge d' \neq e')$
or $(d' = e' \neq * \wedge d \neq e).$
\item[(ii)]
For any set $\si{X} \subseteq E_{\eE\times\eF}$ of events in
$\eE\times\eF$, we define the projections
$$\begin{array}{l}\pi_{1}(X) := \{e \in E_{\eE} \mid \exists e'
\in E_{\eF} \cup \{*\}: (e,e') \in X\} \mbox{ and}\\ \pi_{2}(X) :=
\{e' \in E_{\eF} \mid \exists e \in E_{\eE} \cup \{*\}: (e,e') \in
X\}.\end{array}$$
\end{definitioni}
In the next section we will see that this definition does not always
match the informal description of parallel product above.
%\subsection{Refinement of events}
Refinement of events in a flow event structure $\eE$ may now be defined as
follows (cf. \cite{GG}). We assume a refinement function ${\it ref}: E_{\eE} \rightarrow
\db{E} - \{O\}$ mapping events to non-empty flow event
structures, and replace each event $e$ by a disjoint copy
of {\it ref} $(e)$. The conflict and causality structure will just be
inherited.
\pagebreak[3]
\begin{definition}{flow-ref}{Let ${\cal E} \in I\!\!E$ and
let ${\it ref}: E_{\eE} \rightarrow \db{E} - \{O\}$.}
The {\it refinement of ${\cal E}$ by} {\it ref}, {\it ref} $({\cal
E})$, is the flow event structure defined by\\
-- $E_{r\!e\!f({\cal E})} := \{(e,e') | e \in E_{\cal E}, e' \in
E_{r\!e\!f(e)}\},$\\
-- $(d,d') \prec_{r\!e\!f({\cal E})}(e,e')$ iff
$d \prec_{\cal E} e$ or $(d = e \wedge d' \prec_{r\!e\!f(d)}e')$,\\
-- $(d,d') \; \#_{r\!e\!f({\cal E})} \; (e,e')$ iff $d \; \#_{\cal
E} \; e$ or $(d = e \wedge d' \; \#_{r\!e\!f(d)} \; e'$).
\end{definition}
Sometimes we specify ${\it ref}(e)$ only for certain events $e$.
In this case we assume ${\it ref}(e) = e$ for all other events
$e$. As for most applications it is sufficient to consider flow
event structures up to isomorphism, i.e.\ abstracting from the
names of events, we will sometimes simplify the names of events in
examples.
\newpage
\section{$\!\!\!$Requirements for well-behaved flow event structures$\hspace{-1.38pt}$}\label{requirements}
In our understanding, a run of the parallel product of two event
structures ought to be composed of runs of its components.
Therefore we expect that the projections of configurations of
product event structures $\eE\times\eF$ are themselves
configurations. The following example shows that for arbitrary
flow event structures this is not the case.
\begin{example}{undesired}{}
Consider the flow event structures ${\cal E}:=\begin{array}{l} b
\lra\!\!\!- c \lra\!\!\!- d\\ \!\#\\ a \end{array}$ and ${\cal
F}:=\begin{array}{l} e \lra\!\!\!- f\end{array}$.\\ It is easy to
verify that $\{(a,e),(c,f)\}\in \conf(\eE \times \eF)$, although
$\pi_{1}(\{(a,e),(c,f)\}) = \{a,c\} \not\in \conf(\eE)$.
\end{example}
Castellani and Zhang \cite{CZ} define a subclass of flow event
structures where this problem does not occur. It consists of those
flow event structures satisfying the so-called $\Delta$-axiom.
\begin{trivlist} \item[\hspace{\labelsep}\bf
Axiom $\Delta$:] \hfill $a \# b \prec c \wedge a \not\sim c
\Rightarrow \exists d: b \# d \prec c \wedge \forall e \# d: (e
\neq b \Rightarrow b \# e \sim c).$ \hfill\mbox{}
\end{trivlist}
Here $e \sim e'$ abbreviates $e \# e' \vee e \prec e' \vee e'
\prec e$. The work of \cite{CZ} implies that on this class
parallel product is well-behaved in the sense that the projections
of configurations of product event structures are themselves
configurations, i.e.\ the problem illustrated in \ex{undesired}
does not occur. They also show that this class is closed under all
operators of CCS as defined in \cite{BC-b}. However, this class is
not closed under our refinement operator.
\begin{example}{delta}{}
Refining $b$ into $\begin{array}[c]{c}b_1\\ b_2\end{array}$ in~
\raisebox{-8mm}[5mm][10mm]{
\begin{picture}(20,0)
\put(0,10){\makebox(0,0){$a$}} \put(5,10){\makebox(0,0){$\#$}}
\put(10,10){\makebox(0,0){$b$}} \put(15,10){\makebox(0,0){$\#$}}
\put(10,7.5){\line(0,-1){6}} \put(10,7.5){\vector(0,-1){4}}
\put(20,10){\makebox(0,0){$d$}} \put(18,8){\line(-1,-1){6.5}}
\put(18,8){\vector(-1,-1){4}} \put(10,0){\makebox(0,0){$c$}}
\end{picture}}
~~yields~ \raisebox{-8mm}{
\begin{picture}(14,0)(6,0)
\put(4,18){\makebox(0,0){$a$}} \put(7,14){\makebox(0,0){$\#$}}
\put(9,18){\makebox(0,0){$\#$}} \put(14,18){\makebox(0,0){$b_1$}}
\put(14,15){\line(-1,-4){3.4}} \put(14,15){\vector(-1,-4){2.5}}
\put(17,14){\makebox(0,0){$\#$}} \put(10,10){\makebox(0,0){$b_2$}}
\put(15,10){\makebox(0,0){$\#$}} \put(10,7.5){\line(0,-1){6}}
\put(10,7.5){\vector(0,-1){4}} \put(20,10){\makebox(0,0){$d$}}
\put(18,8){\line(-1,-1){6.5}} \put(18,8){\vector(-1,-1){4}}
\put(10,0){\makebox(0,0){$c$}}
\end{picture}}
. The former structure satisfies $\Delta$, by lack of events $e
\neq b$ with $e \# d$. However, the latter does not: take $b
:=b_2$ and $e := b_1$; then $b_2 \# b_1$ fails to
hold.\footnote{When labelling event $a$ with $a$, $b$ with $\tau$,
$c$ with $c$ and $d$ with $\overline{a}$, the original event
structure can be denoted by the CCS-expression $a \,|\,
\overline{a}.c.{\sf nil}$. Hence, excluding this event structure
from consideration by strengthening the $\Delta$-axiom is not an
option.}
\end{example}
We will show that this problem can be solved by regarding a
different subclass of flow event structures, closed under event
refinement and parallel product, for which parallel product is
still well-behaved. In the remainder of this section we will
expand on the requirements to be imposed on such a class. In
Section~\ref{solution} we will propose two classes meeting these
requirements, one of which will contain the class from \cite{CZ},
i.e.\ all flow event structures satisfying $\Delta$.
\subsection{Closure requirements}\label{closure}
We require a suitable class of flow event structure to be closed
under parallel product and event refinement. This implies that the
corresponding class of labelled flow event structures will be
closed under Winskel's parameterised parallel composition operator
and under action refinement, which are the labelled counterparts
of parallel product and event refinement. The process algebraic
operators choice, sequential composition, restriction and renaming
can easily be expressed in terms of action refinement.
Furthermore, the parallel composition operators from CCS, CSP,
SCCS, ACP and many other system description languages can be
expressed in terms of Winskel's parallel composition, restriction
and renaming. In particular, all CCS operators as defined in
\cite{BC-b} can be expressed in terms of parallel composition and
action refinement. Hence a suitable class of flow event structures
will also be closed under all those operators.
\subsection{Parallel product should be well-behaved}
We propose to formulate the requirement of non-occurrence of the
problem illustrated in \ex{undesired} on a subclass of flow event
structures as follows.
\begin{definition}{well-behaved parallel}
{Let $\db{E}' \subseteq \db{E}$ be a class of flow event
structures.} Parallel product is said to be {\em well-behaved} on
$\db{E}'$ iff for every $\eE,\eF \in \db{E}'$ and $X \in \conf(\eE
\times \eF)$ we have $\pi_1(X) \in \conf(\eE)$ and $\pi_2(X) \in
\conf(\eF)$.
\end{definition}
\subsection{Compositionality}
An operator $f$ on a model of concurrency is said to be
compositional with respect to a certain notion of behaviour if the
behaviour of an application of $f$ is completely determined by the
behaviour of its arguments. For an $n$-ary operator $f$ on flow
event structures this means that $\eC(f(\eE_{1},\ldots,\eE_{n}))$
is derivable from $\eC(\eE_{1}), \ldots ,\eC(\eE_{n})$.
\begin{definition}{compositionality}{}
An operator $f: \db{E}^n \rightarrow \db{E}$ is called
\emph{compositional} iff there exists an $n$-ary operation on
configuration structures $f_{\eC}$ such that $\eC(f(\eE_{1},
\ldots ,\eE_{n})) = f_{\eC}(\eC(\eE_{1}), \ldots ,\eC(\eE_{n}))$.
\end{definition}
If $f$ is compositional then $\eC(\eE_{i})=\eC(\eE'_{i})$ for all
$i=1,\ldots,n$ implies $\eC(f(\eE_{1}, \ldots , \eE_{n})) =
\eC(f(\eE'_{1}, \ldots ,\eE'_{n})).$
We require that the process algebraic operators discussed in
Section \ref{closure} are compositional on our subclass of flow
event structures. As all these operators are expressible in terms
of parallel composition and action refinement, which are the
labelled counterparts of parallel product and event refinement, it
suffices to establish compositionality for the latter.
In \cite{GG}, compositionality for action refinement on the class
of all flow event structures has been established by showing that
${\cal C}(\reff({\cal E})) = \reff_{\cal C}({\cal C}({\cal E}))$,
where $\reff_{\eC}$ is the refinement operator on configuration
structures of \cite{GG} induced by the refinements $\reff_{\cal
C}(e) := {\cal C}(\reff(e))$ for $e \in E_{\eE}$. This result may
be immediately transferred to event refinement and is inherited
when taking subclasses of flow event structures.
However, for parallel product compositionality turns out to fail.
The anomaly of \ex{undesired} can be used to show that $\times$ is
not compositional on $\db{E}$.
\addtocounter{exam}{-2}\begin{example}{no comp}{{\bf (continued)}}
Let ${\cal E}' =$
\begin{picture}(24,10)(-2,4)
\put(0,11){\makebox(0,0){$b$}}
\put(10,10){\makebox(0,0){$c$}} \put(20,10){\makebox(0,0){$d$}}
\put(0,5){\makebox(0,0){$\#$}} \put(5,5){\makebox(0,0){$\#$}}
\put(0,0){\makebox(0,0){$a$}}
\put(2,10){\vector(1,0){4}}\put(2,10){\line(1,0){6}}
\put(12,10){\vector(1,0){4}}\put(12,10){\line(1,0){6}}
\put(2,2){\makebox(0,0){.}} \put(3,3){\makebox(0,0){.}}
\put(7,7){\makebox(0,0){.}} \put(8,8){\makebox(0,0){.}}
\end{picture}.\vspace{15pt}
Then $\eC(\eE)=\eC(\eE')$. However $\eC(\eE \times \eF) \neq
\eC(\eE' \times \eF)$, since $\{(a,e),(c,f)\} \not\in
\conf(\eE')$. The r\^ole of $d$ in this example is to ensure that
$\surd(\eE)=\surd(\eE')$.
\end{example}
In Section \ref{compositionality} we will show that
well-behavedness of parallel product on a subclass of flow event
structures guarantees its compositionality.
\subsection{Parallel product as a categorical product}
In \cite{CZ} a notion of morphism between flow event structures is
defined, making the class of flow event structures into a
category. Following \cite{Winskel}, they would like the parallel
product $\times$ to be the categorical product in this category.
For this it is, by definition, necessary that $\times$ is
well-behaved in the sense of \df{well-behaved parallel}.
\ex{undesired} shows that on the class of {\em all} flow event
structures this is not the case. However, they prove that on the
subclass of flow event structures satisfying the $\Delta$-axiom
$\times$ {\em is} the categorical product.
Interestingly, the only part of their proof using the
$\Delta$-axiom is where they show that the projections of
configurations of product event structures $\eE\times\eF$ are
themselves configurations. Hence their result can be partitioned
in two parts: $\times$ is well-behaved on the class of flow event
structures satisfying $\Delta$, and for any class of flow event
structures on which $\times$ is well-behaved this operator is in
fact the categorical product. Thus the requirement that on a
subclass of flow event structures $\times$ is the categorical
product w.r.t.\ the morphisms of \cite{CZ} is equivalent to the
requirement that on this subclass $\times$ is well-behaved.
\newpage
\section{Compositionality}\label{compositionality}
Let $\db{E}'$ be any class of flow event structures on which
parallel product is well-behaved. In this section we establish the
compositionality of parallel product on $\db{E}'$ by defining a
counterpart of this operator on the model of configuration
structures.
\begin{definition}{product conf}
{Let ${\cal C}$ and ${\cal D}$ be configuration structures.}
The \emph{parallel product} ${\cal C} \times {\cal D}$ is defined by
$$X \in C_{\eC \times {\cal D}} \Leftrightarrow \left\{
\begin{array}{@{}l@{}}
X \subseteq (E_{\cal C} \times \{*\}) \cup
(\{*\} \times E_{\cal D}) \cup (E_{\cal C} \times E_{\cal D})
\\[3pt]
\pi_1(X) \in C_{\cal C} \mbox{ and }
\pi_2(X) \in C_{\cal D} \\[3pt]
(d,d'),(e,e') \in X \Rightarrow \left\{
\begin{array}{@{}l@{}}
(d = e \neq *) \Rightarrow d'=e' \\
(d' = e' \neq *) \Rightarrow d=e.
\end{array}\right.\\
\end{array}\right.$$
$$X \in \surd_{\eC \times {\cal D}} \Leftrightarrow
X \in C_{\eC \times {\cal D}} \wedge
\pi_1(X) \in \surd_{\cal C} \wedge
\pi_2(X) \in \surd_{\cal D}.
$$ Here $\pi_{1}(X) := \{e \in E_{\eC} \mid \exists e' \in
E_{\eD} \cup \{*\}: (e,e') \in X\}$\\ and $\pi_{2}(X) := \{e' \in
E_{\eD} \mid \exists e \in E_{\eC} \cup \{*\}: (e,e') \in X\}$.
\end{definition}
The operator $\times$ defined above agrees with the categorical product
$\times_F$ defined in \cite{Winskel} on a category of {\em
families of configurations}, which are special kinds of configuration
structures without termination predicate. It is also similar to
the parallel product of \cite{PP}, defined on {\em event
automata}, which can be regarded as generalisations of
configuration structures without termination predicate.
The parallel product defined above does not quite qualify as the
operation $\times_{\eC}$ required by \df{compositionality}, for it
may introduce ``unreachable'' configurations, whereas such
configurations never occur in configuration structures of flow
event structures (as we will show in \pr{connected}). Semantically
these unreachable configurations are unimportant; virtually all
semantic equivalences on configuration structures proposed in the
literature identify structures that differ only in their
unreachable part. Hence, using the parallel product of \df{product
conf} we could prove compositionality ``up to'' such a semantic
equivalence. However, as we do not want to deal with equivalence
notions here, we will use a modified version of parallel product
on configuration structures which excludes unreachable
configurations.
\begin{definition}{connected}{Let $\eC$ be a configuration structure
and $X \in C_\eC$.} $X$ is {\em reachable} iff there are
$X_0,...,X_n \in C_{\cal C}$ with $\emptyset=X_0 \subset X_1 \subset
\cdots \subset X_n = X$ and $\forall i1$) with $e_{1} \prec e_{2} \prec
\ldots \prec e_{k+1} = e_{1}$. As $X$ is reachable $\exists
X_0,...,X_n \in C_{\eC^\circ(\eE)}$ with $\emptyset=X_0 \subset X_1
\subset \cdots \subset X_n = X$ and $\forall i