\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 i<n: |X_{i+1} - X_{i}| = 1$.
Let $R(C_\eC)$ be the set of reachable configurations of $\eC$.
\\
The {\em reachable part} ${\cal R}(\eC)$ of $\eC$ is given by
${\cal R}(\eC) := (R(C_\eC),\surd_\eC \cap R(C_\eC))$.
\\
$\eC$ is {\em connected} iff all its configurations are reachable,
i.e.\ if ${\cal R}(\eC)=\eC$.
\end{definition}

\begin{observation}{connected}
A configuration structure $\eC$ is connected iff for every $X \in
C_\eC$ with $X \neq \emptyset$ there is a $g \in X$ such that $X-\{g\}
\in C_\eC$.
\end{observation}

For configuration structures $\eC$ and $\cal D$ let $\eC
\times_{\cal R} \eD$ be defined as ${\cal R} (\eC \times \cal D)$.
The operator $\times_{\cal R}$ has been defined inductively in
\cite{Costantini}. We will show that for well-behaved flow
event structures $\eE$ and $\eF$ one has $\eC(\eE \times \eF) =
\eC(\eE) \times_{\cal R} \eC(\eF)$, thereby establishing the
compositionality of parallel product for well-behaved flow event
structures. We start by showing that the configuration structures
of flow event structures are always connected.

\begin{proposition}{connected}{Let $\eE \in \db{E}$.}
Then $\eC(\eE)$ is connected, i.e.\ ${\cal R}(\eC(\eE)) =
\eC(\eE)$.
\end{proposition}

\begin{proof}
Let $\eE \in \db{E}$ and $\emptyset \neq X \in \conf(\eE)$. As $X$
is cycle-free there must be a $g \in X$  that is maximal in $X$
w.r.t.\ $\prec$. By \ob{connected} it suffices to show that
$X-\{g\} \in \conf(\eE)$.

Finiteness, cycle-freeness and conflict-freeness of $X-\{g\}$
follow from the same properties of $X$. Let $d \prec e \in
X-\{g\}$ and $d \not\in X-\{g\}$. As $g$ is maximal in $X$ we have
$d \neq g$. Because $X$ is left-closed up to conflicts $\exists f
\in X: d \# f \prec e$. As $g$ is maximal in $X$ we have $f \neq
g$, i.e.\ $f \in X-\{g\}$. Thus $X-\{g\}$ is left-closed up to
conflicts.
\end{proof}

\begin{trivlist} \item[\hspace{\labelsep}\bf
    Notation] For configuration structures $\eC$ and $\eD$ we
write $\eC \subseteq \eD$ for $C_\eC \subseteq C_\eD \wedge \surd_\eC
\subseteq \surd_\eD$.
\end{trivlist}

\begin{observation}{inclusion}
    If $\eC \subseteq \eD$ then ${\cal R}(\eC) \subseteq {\cal R}(\eD)$.
\end{observation}

Now the desired compositionality result falls apart in two
directions. We start by showing that $\eC(\eE \times \eF)
\subseteq \eC(\eE) \times_{\cal R} \eC(\eF)$, the only direction
in which it is used that parallel product is well-behaved on
$\db{E}'$.

\begin{lemma}{product weak}
    {Let $\eE,\eF \in \db{E}'$.}
    Then $\eC(\eE\times\eF) \subseteq \eC(\eE)\times\eC(\eF)$.
\end{lemma}

\begin{proof}
We must show that $\conf(\eE \times \eF) \subseteq C_{\eC(\eE)
\times \eC(\eF)}$ and $\surd(\eE \times \eF) \subseteq
\surd_{\eC(\eE) \times \eC(\eF)}$.\\[6pt] Let $X \in \conf(\eE
\times \eF)$. We show that $X \in C_{\eC(\eE)\times\eC(\eF)}$,
according to \df{product conf}. \vspace{-6pt}
\begin{itemise}
\item As $\times$ is well-behaved on $\db{E}'$, $\pi_1(X) \in \conf(\eE) =
C_{\eC(\eE)}$ and $\pi_2(X) \in \conf(\eF) = C_{\eC(\eF)}$.
\item By \df{product} we have $X \subseteq E_{{\cal E} \times {\cal
F}} = (E_{\cal E} \times \{*\}) \cup (\{*\} \times E_{\cal F})
\cup (E_{\cal E} \times E_{\cal F})$.  That we even have $X
\subseteq (E_{\eC(\eE)} \times \{*\}) \cup (\{*\} \times
E_{\eC(\eF)}) \cup (E_{\eC(\eE)} \times E_{\eC(\eF)})$, i.e.\ the
first requirement of \df{product conf}, now follows from the
second requirement of \df{product conf} established above.
\item Suppose $(d,d'),(e,e') \in X$ and $(d = e \neq *)$, but $d' \neq e'$.
Then $(d,d') \;\#\; (e,e')$, contradicting the conflict-freeness of $X$.
The other condition follows by symmetry.
\end{itemise}
Now let $X \in \surd(\eE \times \eF)$. Then surely $X \in
\conf(\eE \times \eF) \subseteq C_{\eC(\eE) \times \eC(\eF)}$.
According to \df{product conf} is remains to be be shown that
$\pi_1(X) \in \surd_{\eC(\eE)}$ and $\pi_{2}(X) \in
\surd_{\eC(\eF)}$. Let $* \neq d \not\in \pi_1(X)$. Then $(d,*)
\not\in X$. So $\exists (e,e') \in X$ with $(d,*) \;\#\; (e,e')$.
Now $e \in \pi_1(X) \cup \{*\}$. Hence $e \neq d$, so $d \# e \neq
*$. Thus $\pi_1(X) \in \surd_{\eC(\eE)}$. That $\pi_2(X) \in
\surd_{\eC(\eF)}$ follows by symmetry.
\end{proof}

\begin{corollary}{product compositionality}
    {Let $\eE,\eF \in \db{E}'$.}
    Then $\eC(\eE\times\eF) \subseteq \eC(\eE)\times_\fR \eC(\eF)$.
\end{corollary}

\begin{proof}
$\!\!\eC(\eE\!\times\!\eF) \!\stackrel{\it
Prop.~\ref{pr-connected}}{=}\! {\cal R}(\eC(\eE\!\times\!\eF))
\!\!\!\stackrel{\it \lem{product weak},~
Obs.~\ref{obs-inclusion}}{\subseteq}\!\!\! {\cal
R}(\eC(\eE)\!\times\!\eC(\eF)) \stackrel{\it def.}{=} \eC(\eE)
\times_{\cal R} \eC(\eF)$.
\end{proof}

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

\begin{definition}{cyclic configurations}{{Let ${\cal E} \in \db{E}$.}}
$X \subseteq E$ is a {\it possibly cyclic configuration} of ${\cal
E}$ iff $X$ is finite, conflict-free and left-closed up to
conflicts.\\
\index{configuration!terminated}%
Such a configuration is called {\it terminated}
iff $\forall d \in E: d \notin X\Rightarrow \exists e \in X$ with
$d\#e$.\\
${\it Conf}^\circ ({\cal E})$ denotes the set of all possibly cyclic configurations
of ${\cal E}$, and $\surd^\circ({\cal E})$ the set of all terminated ones.
Furthermore, let ${\cal C}^\circ({\cal E}) :=(\conf^\circ({\cal E}),\;
\surd^\circ({\cal E}))$.
\end{definition}

\begin{lemma}{product acyclic}
    {Let $\eE,\eF \in \db{E}$.}
    Then $\eC(\eE)\times\eC(\eF) \subseteq \eC^\circ(\eE\times\eF)$.
\end{lemma}

{\bf Proof\ } Let $X \in C_{\eC(\eE)\times\eC(\eF)}$. We show that
$X \in \conf^\circ (\eE \times \eF)$.
\begin{itemise}
\item $X$ is finite, since $\pi_1(X)$ and $\pi_2(X)$ are finite.
\item $X$ is conflict-free, due to the last requirement for $X \in
C_{\eC(\eE)\times\eC(\eF)}$ of \df{product conf} and the
conflict-freeness of $\pi_1(X)$ and $\pi_2(X)$.
\item Let $(d,d') \prec (e,e') \in X$ and $(d,d') \not\in X$.
Then either $d \prec e$ or $d' \prec e'$, say $d \prec e$. In
particular $d,e \neq *$.
We have $e \in \pi_1(X) \in \conf(\eE)$. There are two possibilities for $d$:
\begin{itemize}
\item [\bf --] $d \not\in \pi_1(X)$. Then $\exists f \!\in\! \pi_1(X): d \# f \prec e$.
So $\exists (f,f') \!\in\! X: (d,d') \# (f,f') \!\prec\! (e,e')$.
\item [\bf --] $d \in \pi_1(X)$. Then $\exists (d,d'') \in X$. Hence $d' \neq d''$.
We have $(d,d') \;\#\; (d,d'') \prec (e,e')$.
\end{itemize}
Hence $X$ is left-closed up to conflicts.
\pagebreak[3]
\end{itemise}
Now let $X \in \surd_{\eC(\eE)\times\eC(\eF)}$.
We show that $X \in \surd^\circ (\eE \times \eF)$.
\begin{itemise}
\item []
Let $(d,d') \in E_{\eE \times \eF}$ with $(d,d') \not\in X$. Then
either $d \neq *$ or $d' \neq *$, say $d \neq *$. Again there are
two possibilities for $d$:
\begin{itemize}
\item [\bf --] $d \not\in \pi_1(X)$.
As $\pi_1(X) \in \surd_{\eC(\eE)}$ there must be an $e \in
\pi_1(X)$ with $d \# e$. Hence $\exists (e,e') \in X$ with $(d,d')
\;\#\: (e,e')$.
\item [\bf --] $d \in \pi_1(X)$. Then $\exists (d,d'') \in X$.
Hence $d' \neq d''$. We have $(d,d') \;\#\; (d,d'')$.
\end{itemize}
Hence $X$ is terminating.\kasten
\end{itemise}

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

\begin{lemma}{connected}{Let $\eE \in \db{E}$.}
     Then ${\cal R}(\eC^\circ(\eE))=\eC(\eE)$.
\end{lemma}

\begin{proof}
``$\supseteq$'':
    By definition $\eC(\eE) \subseteq \eC^\circ(\eE)$, so by \pr{connected} and \ob{inclusion}
    $\eC(\eE) = {\cal R}(\eC(\eE)) \subseteq {\cal R}(\eC^\circ(\eE))$.

``$\subseteq$'':
    Let $X \in {\cal R}(\eC^\circ(\eE))$. It suffices to show that $X$
    is cycle-free. Suppose $X$ contains a cycle: $\exists
    e_{1},\ldots,e_{k+1} \in X$ ($k>1$) 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<n: |X_{i+1} - X_{i}| = 1$.
    Let $i < n$ be such that $X_{i+1} \supseteq \{e_{1},\ldots,e_{k}\}$
    and $e_{j} \not\in X_{i}$ for a certain $j \in \{1,\ldots,k\}$.
    As $e_{j} \prec e_{j+1} \in X_{i} \in C_{\eC^\circ(\eE)}$ there must
    be an $f \in X_{i} \subset X_{i+1}$ with $e_{j} \# f \prec
    e_{j+1}$. So $f,e_{j} \in X_{i+1}$, contradicting the
    conflict-freeness of $X_{j+1}$.
\end{proof}

\pagebreak[3]
\begin{corollary}{compositionality}
    {Let $\eE$ and $\eF$ be arbitrary flow event structures.}
    Then $\eC(\eE\times\eF) \supseteq \eC(\eE)\times_\fR \eC(\eF)$.
\end{corollary}

\begin{proof}
$\!\!\! \eC(\eE)\times_\fR \eC(\eF) \stackrel{\it def.}{=}
\fR(\eC(\eE)\!\times\!\eC(\eF))\!\!\! \stackrel{\it \lem{product
acyclic},~Obs.~\ref{obs-inclusion}}{\subseteq}\!\!\! {\cal
R}(\eC^\circ(\eE\!\times\!\eF)) \! \stackrel{\it
\lem{connected}}{=}\! \eC(\eE\!\times\!\eF)$.
\end{proof}
Together, Corollaries \ref{cor-product compositionality} and
\ref{cor-compositionality} say that parallel product is
compositional on any class of flow event structures on which
parallel product is well-behaved.
% : if $\eE,\eF \in \db{E}$ are well-behaved then $\eC(\eE\times\eF) =
% \eC(\eE)\times_{\cal R}\eC(\eF)$.

\newpage
\section{Well-behaved flow event structures}\label{solution}

\newcommand{\fair}[1]{{\rm [}#1{\rm ]}}

In this section we define two subclasses of flow event structures,
both satisfying the requirements of Section \ref{requirements}. To
this end we define two notions of configuration for flow event
structures, the \emph{weak} and the \emph{fairly weak}
configurations,\footnote{We will put the material on {\em fairly}
weak configurations and the related subclass in square brackets.}
that are more liberal than the standard notion of \df{flow-conf}.
The two subclasses of flow event structures will
be the classes on which the weak, resp.\ the fairly weak, notion
of configuration coincides with the standard one. The larger
class, using fairly weak configurations, contains all flow event
structures satisfying $\Delta$.

\begin{definition}{weak configurations}{{Let ${\cal E} \in \db{E}$.}}
$X \subseteq E$ is a {\it \fair{fairly} weak configuration} of
${\cal E}$ iff $X$ is finite, cycle-free, conflict-free and
\emph{\fair{fairly} weakly left-closed up to conflicts}:
\index{weakly 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$ \fair{and $\neg(e
\prec f)$}.\\
\index{configuration!terminated}%
Such a configuration is called {\it terminated} iff $\forall d \in
E: d \notin X\Rightarrow \exists e \in X$ with $d\#e$.\\ ${\it
Conf}_{w} ({\cal E})$ \fair{resp.\ ${\it Conf}_{fw} ({\cal E})$}
denotes the set of all \fair{fairly} weak configurations of ${\cal
E}$, and $\surd_{w}({\cal E})$ \fair{resp.\ $\surd_{fw} ({\cal
E})$} the set of all terminated \fair{fairly} weak configurations
of $\eE$.\linebreak The \emph{\fair{fairly} weak configuration
structure of} ${\cal E}$ is ${\cal C}_{[f]w}({\cal E})
:=(\conf_{[f]w}({\cal E}),\; \surd_{[f]w}({\cal E}))$.

\end{definition}

\begin{observation}{strong-weak}
Note that every strong configuration is certainly fairly weak, and
every fairly weak configuration is certainly weak.
\end{observation}
On the other hand, in \ex{undesired} the set of events $\{a,c\}$
constitutes a \fair{fairly} weak configuration of $\eE$ but not a
strong one. Furthermore, in $\cal G =$ \raisebox{-4mm}[7mm][5mm]{
\begin{picture}(12,0)(10,0)
\put(10,10){\makebox(0,0){$b$}} \put(10,5){\makebox(0,0){$\#$}}
\put(12,10){\line(1,0){6}} \put(12,10){\vector(1,0){4}}
\put(20,10){\makebox(0,0){$c$}} \put(10,0){\makebox(0,0){$a$}}
\put(18,8){\line(-1,-1){6.5}} \put(18,8){\vector(-1,-1){4}}
\end{picture}}
the set of events $\{a,c\}$ constitutes a weak configuration but
not a fairly weak one.

\begin{definition}{well-behaved}{}
A flow event structure is called {\em \fair{fairly} well-behaved}
iff all its \fair{fairly} weak configurations are strong.
\end{definition}
Note that well-behaved flow event structures are certainly fairly
well-behaved. The structure $\cal G$ above is fairly well-behaved,
but not well-behaved. The structure $\eE$ of \ex{undesired} is not
even well-behaved.

In the remainder of this section we will show that\vspace{-1ex}
\begin{itemise}
\item the classes of \fair{fairly} well-behaved flow event structures are closed
under event refinement and parallel product,
\item parallel product is well-behaved on these classes,
\item flow event structures satisfying the $\Delta$-axiom are
fairly well-behaved. \pagebreak
\end{itemise}
The structure $\cal G$ on the previous page satisfies the
$\Delta$-axiom. Hence, flow event structures satisfying the
$\Delta$-axiom are not always well-behaved.

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

\begin{notation} {Let ${\cal E} \in \db{E}$ and let ${\it ref}:
E_{\eE} \rightarrow \db{E} - \{O\}$.}

For any set $\si{X} \subseteq E_{\reff(\eE)}$ of events in
$\reff(\eE)$, define the projections
\begin{center}
$\pi_1(\si{X}) := \{e \mid \exists f: (e,f) \in \si{X}\}~~~~~$ and
$~~~~~\pi_2^e(\si{X}) := \{f \mid (e,f) \in \si{X}\}$.
\end{center}
\end{notation}

Now $\si{X}$ can be written as $\si{X} = \displaystyle
\mathdis{}{\bigcup}{e\in \pi_1(\si{X})} \{e\} \times
\pi_2^e(\si{X})$. \pagebreak[3]

\begin{propositioni}{flow-compositionality weak}{Let ${\cal E} \in \db{E}$,
let ${\it ref}: E_{\eE} \rightarrow \db{E} - \{O\}$ and let
$\si{X} \in \conf_{[f]w}(\reff(\eE))$.}
\item [(i)]   $\pi_1(\si{X}) \in \conf_{[f]w}(\eE)$,
\item [(ii)]  $\pi_2^{e}(\si{X}) \in \conf_{[f]w}(\reff(e))$ for all $e \in
              \pi_{1}(\si{X})$,
\item [(iii)] $\pi_2^{e}(\si{X}) \in \surd_{[f]w}(\reff(e))$ when $e$ not
              maximal in $\pi_{1}(\si{X})$ w.r.t.\ $\prec$.
\end{propositioni}

{\bf Proof}\vspace{-1em}
\begin{enumerate}
\item [(i)]
That $\pi_{1}(X)$ is finite, cycle-free and conflict free follows
from the corresponding properties of $X$. We show that
$\pi_{1}(X)$ is \fair{fairly} weakly left-closed up to conflicts.

Let $e \in \pi_1(X),~ d \in E_{\cal E}$ with $d \prec_{\cal E} e$
and $d \not\in \pi_1(X)$.\\ We have to show that there exists an
$f\in \pi_1(X)$ with $f \#_{\cal E} d$ \fair{and $\neg(e
\prec_{\cal E} f)$}.\\ Since $e \in \pi_1(X)$ there must be some
$(e,e') \in \si{X}.$\\ There exists $(d,d') \in E_{r\!e\!f({\cal
E})},~ (d,d') \not\in \si{X}$ since {\it ref} $(d) \neq O$ and $d
\not\in \pi_1(X)$.\\ Furthermore $(d,d') \prec_{r\!e\!f({\cal E})}
(e,e')$ since $d \prec_{\cal E} e$.\\ So there exists $(f,f') \in
\si{X}$ with $(f,f') \#_{\reff(\eE)}(d,d')$ \fair{and $\neg((e,e')
\prec_{\reff({\cal E})} (f,f'))$}.\\ $f \neq d$ since $f \in
\pi_1(X), d \not\in \pi_1(X)$; hence $f \#_{\cal E} d.$\\ \fair{As
$\neg((e,e') \prec_{\reff({\cal E})} (f,f'))$ we cannot have $e
\prec_{\cal E} f$ and we are done.}
\item [(ii)]
Let $e \in \pi_1(X)$. Obviously $\pi_2^e(\si{X}) \subseteq
E_{\reff(e)}$.\\ $\pi_2^e(\si{X})$ is finite, cycle-free and
conflict-free since $\si{X}$ is finite, cycle-free and
conflict-free. We show that $\pi_2^e(\si{X})$ is \fair{fairly} weakly
left-closed up to conflicts.

Let $d' \in E_{\reff(e)},~ d' \prec_{\reff(e)} e' \in
\pi_2^{e}(X),~ d' \not\in \pi_2^{e}(X)$.\\ Then $(e,d') \in
E_{r\!e\!f({\cal E})},~ (e,d') \prec_{r\!e\!f({\cal E})} (e,e')
\in \si{X}$ and $(e,d') \not\in \si{X}.$\\ So there exists $(f,f')
\in \si{X}$ with $(f,f') \#_{r\!e\!f({\cal E})} (e,d')$ \fair{and
$\neg((e,e') \prec_{r\!e\!f({\cal E})}(f,f'))$}.\\ As $f,e \in
\pi_1(X)$ we have $\neg (f \#_{\cal E} e)$, so $f = e \wedge f'
\#_{\reff(e)} d'$.\\ Thus $f' \in \pi_2^e(X)$ \fair{and $\neg(e'
\prec_{\reff(e)} f')$}.
\item [(iii)]
Suppose $e$ is not maximal in $\pi_1(X)$.\\ Then there exists $f
\in \pi_1(X)$ with $e \prec_{\cal E} f$, so there is an $(f,f')\in
\si{X}$. \\ Let $d'\in E_{\reff(e)}-\pi_2^e(\si{X})$. We have
$(e,d') \prec_{r\!e\!f\,({\cal E})} (f,f')$ and $(e,d') \notin
\si{X}$. \\ Since $\si{X}$ is a \fair{fairly\hspace{-1pt}} weak
configuration, there exists $(g\hspace{-.8pt},\hspace{-1pt}g')\!\in\!
\si{X}$ with $(g\hspace{-.8pt},\hspace{-1pt}g')\#_{\reff({\cal E})}
(e,\hspace{-1pt}d')$.$\hspace{-1.2pt}$
%\fair{and $\neg((f,f') \prec_{\reff({\cal E})} (g,g'))$}.\\
As $g,e \in \pi_1(X)$, we have $\neg (g\#_{\cal E} e)$. Hence $g=e$,
$g'\in \pi_2^e(\si{X})$ and $g'\#_{\reff(e)} d'$. \kasten
\end{enumerate}

\begin{theorem}{closed}{}
{Let $\eE \in \db{E}$ be \fair{fairly} well-behaved and $\reff:
E_{\eE} \rightarrow \db{E}-\{O\}$ such that $\reff(e)$ is
\fair{fairly} well-behaved for all $e\in E_{\eE}$.} Then
$\reff(\eE)$ is \fair{fairly} well-behaved, i.e.\
$\conf_{[f]w}(\reff(\eE)) = \conf(\reff(\eE))$.
\end{theorem}

\begin{trivlist} \item[\hspace{\labelsep}\bf
    Proof\ \ ]
    Let $X \in \conf_{[f]w}(\reff(\eE))$. We have to show that $X$ is
    (strongly) left-closed up to conflicts. Let $(d,d') \prec (e,e') \in
    X$ and $(d,d') \not\in X$. There are three cases to consider.
    \begin{itemise}
        \item Suppose $d \prec e$ and $d \not\in \pi_{1}(X)$.
        We have $\pi_{1}(X) \in \conf_{[f]w}(\eE) = \conf(\eE)$
        by \pr{flow-compositionality weak}(i).
        Hence $\exists f \in \pi_{1}(X)$ such
        that $d \# f \prec e$. So $\exists (f,f') \in X$.
        It follows that $(d,d') \# (f,f') \prec (e,e')$.
        \item Suppose $d \prec e$ and $d \in \pi_{1}(X)$.
        We have $d' \not\in \pi_{2}^d(X) \in \surd_{[f]w}(\reff(d)) =
        \surd(\reff(d))$ by \pr{flow-compositionality weak}(iii).
        Hence $\exists d'' \in \pi_{2}^d(X)$ such that $d' \# d''$.
        So $(d,d'') \in X$. It follows that $(d,d') \# (d,d'') \prec (e,e')$.
        \item Suppose $d = e$ and $d' \prec e'$. We have $d' \not\in
        \pi_{2}^e(X) \in \conf_{[f]w}(\reff(e)) = \conf(\reff(e))$
        by \pr{flow-compositionality weak}(ii). Hence $\exists f' \in
        \pi_{2}^e(X)$ such that $d' \# f' \prec e'$. So $(e,f') \in X$.
        It follows that $(e,d') \# (e,f') \prec (e,e')$.
        \kasten
    \end{itemise}
\end{trivlist}

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

\begin{proposition}{product projection}
    {Let $\eE,\eF \in \db{E}$ and $X \in \conf_{[f]w}(\eE \times \eF)$.}
    Then $\pi_1(X) \in \conf_{[f]w}(\eE)$ and $\pi_2(X) \in \conf_{[f]w}(\eF)$.
\end{proposition}

\begin{proof}
We show that $\pi_1(X) \in \conf_{[f]w}(\eE)$; then $\pi_2(X) \in
\conf_{[f]w}(\eF)$ follows by symmetry. As $X$ is finite,
cycle-free and conflict-free, so is $\pi_1(X)$.\\ Suppose $d \prec
e \in \pi_1(X)$ and $* \neq d \not\in \pi_1(X)$. Then $\exists
(e,e') \in X$, whereas $(d,*) \not\in X$. Moreover $(d,*) \prec
(e,e')$. Thus $\exists (f,f') \in X: (d,*) \;\#\; (f,f')$
\fair{and $\neg ((e,e') \prec (f,f'))$}. \linebreak[3] Now $f \in
\pi_1(X) \cup \{*\}$, so $f \neq d$. It must be that $f \neq *$
and $d \,\#\, f$, since $(d,*) \;\#\; (f,f')$. \fair{In case $e
\prec f$ we would have $(e,e') \prec (f,f')$.} Thus $\pi_1(X)$ is
\fair{fairly} weakly left-closed up to conflicts.
\end{proof}

\ex{undesired} shows that \pr{product projection} does not hold
for strong configurations.

\begin{theorem}{product closed}{Let $\eE,\eF \in \db{E}$ be \fair{fairly} well-behaved.}
    Then $\eE \times \eF$ is \fair{fairly} well-behaved,
    i.e.\ $\conf_{[f]w}(\eE \times \eF) = \conf(\eE \times \eF)$.
\end{theorem}

\begin{trivlist} \item[\hspace{\labelsep}\bf Proof\ \ ]
    Let $X \in \conf_{[f]w}(\eE \times \eF)$.
    We have to show that $X$ is (strongly) left-closed up to conflicts.
    Let $(d,d') \prec (e,e') \in X$ and $(d,d') \not\in X$.
    Then either $d \prec e$ or $d' \prec e'$, say $d \prec e$ (so $d,e
    \neq *$).
    By \pr{product projection} and the well-behavedness of $\eE$ we have
    $\pi_{1}(X) \in \conf_{[f]w}(\eE) = \conf(\eE)$.
    There are two cases to consider.
    \begin{itemise}
        \item Suppose $d \not \in \pi_{1}(X)$.
        Then $\exists f \in \pi_{1}(X)$
        with $d \# f \prec e$. Thus $\exists (f,f') \in X$.
        We have $(d,d') \# (f,f') \prec (e,e')$.
        \item Suppose $d \in \pi_{1}(X)$.
        Then $\exists (d,d'') \in X$.
        Using \df{product} we have $(d,d') \# (d,d'') \prec (e,e')$.
        \kasten
    \end{itemise}
\end{trivlist}

As an immediate consequence of \pr{product projection} we obtain
the result that parallel product is well-behaved on the classes of
\fair{fairly} well-behaved flow event structures.

\begin{theorem}{well-behaved}{Let $\eE,\eF \in \db{E}$ be
\fair{fairly} well-behaved and $X \in \conf(\eE \times \eF)$.}
Then $\pi_1(X) \in \conf(\eE)$ and $\pi_2(X) \in \conf(\eF)$.
\end{theorem}

\begin{proof}
Let $\eE,\eF \in \db{E}$ be \fair{fairly} well-behaved and $X \in
\conf(\eE \times \eF) \stackrel{\it \ob{strong-weak}}{\subseteq}
\conf_{[f]w}(\eE \times \eF)$. With \pr{product projection} and
the \fair{fairly} well-behavedness of $\eE$ and $\eF$ we obtain
$\pi_1(X) \in \conf_{[f]w}(\eE) = \conf(\eE)$ and $\pi_2(X) \in
\conf_{[f]w}(\eF) = \conf(\eF))$.
\end{proof}

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

\begin{theorem}{delta}{Let $\eE \in \db{E}$.}
If $\eE$ satisfies $\Delta$ then $\eE$ is fairly well-behaved.
\end{theorem}
\begin{proof}
Let ${\cal E}$ satisfy $\Delta$. Let $X$ be a fairly weak
configuration of ${\cal E}$. We show that $X$ is strong. It
suffices to show that $X$ is strongly left closed up to
conflicts.\\ Suppose $b \prec c \in X$, $b \notin X$. \\ We have
to show that there exists an $f \in X$ with $f \# b$ and $f \prec
c$. \\ As $X$ is fairly weakly left closed up to conflicts, there
is an $a \in X$ with $a \# b$ and $\neg(c \prec a)$. \\ In case $a
\prec c$, we take $f=a$.
\\ Otherwise, there exists a $d$ as required by the $\Delta$-axiom
($a \not\sim c$ since $a,c \in X$ and $\neg(c \prec a)$). \\ If $d
\in X$ we take $f=d$. \\ Otherwise, as $X$ is fairly weakly left
closed up to conflicts and $d \prec c \in X$, $d \notin X$, there
must be an $f \in X$ with $f \# d$ and $\neg(c \prec f)$. As $b
\notin X$ we have $f \neq b$. \\ Since $\neg(c \prec f)$, $\neg(c
\# f)$ ($c$,$f$ in configuration $X$), the $\Delta$-axiom yields
$b \# f \prec c$.
\end{proof}

\newpage
\section{Concluding remark}

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

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

\subsection*{Acknowledgment}

Arend Rensink challenged our original believe that the $\Delta$-axiom
would be preserved under action refinement in flow event structures
and helped us find Counterexample \ref{ex-delta}.

\newpage
\begin{thebibliography}{1}

\bibitem[BC-a]{BC-b}
{\sc G.~Boudol \& I.~Castellani} (1989):
\newblock {\em Permutation of transitions: an event structure semantics for {CCS} and {SCCS}.}
\newblock In J.W. de~Bakker, W.P.~de Roever \& G.~Rozenberg, editors: {\sl {\rm 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. 411--427.

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

\bibitem[CZ]{CZ}
{\sc I.~Castellani \& G.Q. Zhang} (1997):
\newblock {\em Parallel product of event structures.}
\newblock {\sl Theoretical Computer Science} 179, pp. 203--215.

\bibitem[Costantini]{Costantini}
{\sc R.~Costantini} (1995):
\newblock {\em Abstraktion in ereignisbasierten Modellen verteilter Systeme}.
\newblock Dissertation, Univ. Hildesheim.
\newblock Verlag Dr. Kova\^c.

\bibitem[DD]{DD}
{\sc Ph. Darondeau \& P.~Degano} (1993):
\newblock {\em Refinement of actions in event structures and causal trees.}
\newblock {\sl Theoretical Computer Science} 118, pp. 21--48.

\bibitem[GG]{GG}
{\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[NPW]{NPW}
{\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[PP]{PP}
{\sc G.M. Pinna \& A.~Poign\'e} (1995):
\newblock {\em On the nature of events: another perspective in concurrency.}
\newblock {\sl Theoretical Computer Science} 138(2), pp. 425--454.

\bibitem[Winskel]{Winskel}
{\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; {\rm Proceedings of an Advanced Course, Bad Honnef, September 1986}}, {\sl \rm LNCS} 255, Springer, pp. 325--392.

\end{thebibliography}

\end{document}
