%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Springer-Verlag compatible format. After reducing to 13.5x %%%%
%%%% 20cm the fontsize is exactly 10pt. -Rob van Glabbeek %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentstyle[12pt]{article} % Fontsize 12 point %
\textwidth 16.2 cm % A4 width is 21cm %
\textheight 24 cm % A4 height is 29.7cm %
\oddsidemargin -0.14cm % +1 inch = 2.4cm %
\evensidemargin -0.14cm % +1 inch = 2.4cm %
\topmargin -0.14cm % +1 inch = 2.4cm %
\headheight 0 cm % foot with pagenumber 1.06cm %
\headsep 0 cm % thus 2.24cm left at bottom. %
\parindent 0 cm % Paragraphs not indented ... %
\parskip 6pt plus 2pt minus 1 pt % but some space between them %
\unitlength 1 mm % This is used in pictures %
\thinlines % alternative: Thicklines %
\renewcommand{\baselinestretch}{1.1} % More space between the lines%
\frenchspacing % No larger distance after a .%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% On American paper the right margin is 6 mm larger, whereas %%%%
%%%% the bottom margin is 17.6 mm shorter. -Rob van Glabbeek %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newlength{\shiftside} \newlength{\shifttop}
\setlength{\shiftside}{3mm} \setlength{\shifttop}{-8.8mm}
\typeout{On what kind of paper are you going to print this?}
\typein[\paper]{Enter 0 for A4 or 1 for American paper.}
\addtolength\oddsidemargin{\paper\shiftside}
\addtolength\evensidemargin{\paper\shiftside}
\addtolength\topmargin{\paper\shifttop}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% 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 separately 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{lem}{Lemma}[section]
\newtheorem{cor}{Corollary}[section]
\newtheorem{exam}{Example}[section]
\newenvironment{Definition}[2]{\begin{defi} \rm \label{def-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{defi}}
\newenvironment{Theorem}[2]{\begin{theo} \rm \label{#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{theo}}
\newenvironment{Proposition}[2]{\begin{prop} \rm \label{#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{prop}}
\newenvironment{Lemma}[2]{\begin{lem} \rm \label{#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{lem}}
\newenvironment{Corollary}[2]{\begin{cor} \rm \label{#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{cor}}
\newenvironment{Example}[2]{\begin{exam} \rm \label{ex-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{exam}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\mbox{\rm I\hspace{-0.8mm}N}}
\newcommand{\IE}{\mbox{\rm I\negthinspace E}}
\newcommand{\qed}{\hfill $\Box$ \par \vskip 0.25cm}
\newcommand{\conf}{{\it Conf\/}}
\newcommand{\reff}{{\it ref\/}}
\newcommand{\Act}{{\it Act\/}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\mbox{\ }\vspace{3em}
\begin{center}
{\LARGE\bf Interleaving Semantics \\
and Action Refinement with Atomic Choice\\}
\end{center}
\vskip 1cm
\begin{center}
{\large Ingo Czaja}\\
{\small Gesellschaft f\"ur Mathematik und Datenverarbeitung\\
Postfach 1316, D-5205 Sankt Augustin, Germany}
\vspace{2ex}
{\large Rob J. van Glabbeek}\\
{\small Computer Science Department, Stanford University\\
Stanford, CA 94305, USA\\
\tt rvg@cs.stanford.edu}
\vspace{2ex}
{\large Ursula Goltz}\\
{\small Gesellschaft f\"ur Mathematik und Datenverarbeitung\\
Postfach 1316, D-5205 Sankt Augustin, Germany\\
\tt goltz@gmdzi.gmd.de}
\end{center}
\vskip 1.5cm
We investigate how to restrict the concept of {\it action refinement} such that
established interleaving equivalences for concurrent systems are preserved under
these restricted refinements. We show that {\it interleaving bisimulation} is
preserved under refinement if we do not allow to refine action occurrences
deciding choices and action occurrences involved in autoconcurrency.
On the other hand, {\it interleaving trace equivalence} is
still not preserved under these restricted refinements.
\vspace{2em minus .6em}
{\bf Keywords\ } Concurrency, action refinement, atomicity, flow event
structures, semantic equivalences, interleaving vs. partial orders,
bisimulation.
\vspace{1em minus .3em}
{\bf Notes\ } This paper appeared as Arbeitspapiere der GMD 594, Sankt
Augustin 1991.
The work presented here has partly been carried out
within the Esprit Basic Research Action 3148 (DEMON) and the
Sonderforschungsbereich 182 of the University of Erlangen-N\"urnberg.
\section{Introduction}
For the design of concurrent systems, it can be useful to consider a
hierarchy of representations, which allows refinement of unstructured
entities on a more abstract design level by complex structures on a
lower level. One approach which is being investigated is {\it action
refinement} where the entities being refined are the actions
which a system may perform. A single action in an abstract view may
correspond to a process consisting of many actions in a more concrete representation.
Action refinement is being investigated in process algebras [Aceto, AH, NEL] and in
semantic models of concurrent systems [GG a/b/c, Vogler a/b, BDKP, Devillers, DD a/b,
BGV].
Action refinement can be modelled as an operator, taking a system description $P$ on a
given level of abstraction as well as a refinement function \reff\ associating processes
with actions, and yielding a system description $\reff (P)$ on a lower level, obtained
by replacing action occurrences by occurrences of the associated processes. It differs
from many other operators that are considered for concurrent systems in that applying it
on a representation of a system does not yield a representation of a different system,
but a different representation of the same system.
An important question being considered is the following: Which
equivalence notions for concurrent systems are {\it preserved under
refinement\/}? Taking two system representations, $P,Q$, which are equivalent for some
equivalence notion $\sim$, we would expect that $\reff (P) \sim \reff (Q)$ for any
refinement function $\reff $. This expectation indicates a big difference between
action refinement and many other approaches for moving to a lower level of abstraction,
in which adding more information about the precise implementation of systems makes it
more likely that systems turn out to be different that were indistinguishable
on the higher level of abstraction. Our expectation is based on the idea that in the original
system representations $P$ and $Q$ it is not known how the actions will be implemented.
However, it is decided that different occurrences of the same action will be
implemented in the same way, so that any difference between $P$ and $Q$ that could arise
after refinement is already visible in the abstract representations, namely through
the use of different action names for corresponding events.
The preservation question has been addressed in
the papers mentioned above. The usual approach to this problem is: Take some
well-established equivalence notion. If it is not preserved under refinement, try to
find the coarsest equivalence notion contained in it which has this property (see e.g.
[Vogler a/b]).
What has not been considered so far is the following question. Given a
well-established equivalence notion which is not preserved under
refinement, is there a way of restricting either the allowed refinements or the class
of system representations under consideration such that preservation of this equivalence
in the restricted setting is obtained? This question is addressed in the present paper
for two of the most basic equivalences.
We consider system descriptions in which the basic building blocks are the actions
which may occur in a system. In our approach an action can be any activity which is
considered as a conceptual entity on a chosen level of abstraction. Now we distinguish
{\it atomic} actions that cannot be refined, and compound ones that can. One can
think of atomic actions as being instantaneous and of compound actions as durational.
Many approaches to concurrency in which actions are not supposed to be refined, in
particular the {\it interleaving} approaches, in which parallelism is equated with
arbitrary interleaving of action occurrences, can be thought of as dealing exclusively
with the subclass of system representations were all actions in a system are atomic. On
the other hand the action refinement approaches cited above take the possibility into
account that {\it any} action can be refined. In this paper we look at systems in which
some actions are atomic, and others can be refined. In particular we consider systems in
which all action occurrences deciding choices, as well as all actions that can occur
concurrently with themselves are atomic. These restrictions turn out to be sufficient to
apply action refinement in certain interleaving semantics, while preserving semantic
equivalence. Although the distinction between atomic and compound actions may be useful
for motivating this research, technically one may just as well drop this distinction and
restrict the class of allowed refinement functions to a class of what
we call {\it safe} refinements. Those refinements
do not refine action occurrences deciding choices and actions involved in autoconcurrency.
It turns out that the {\it branching structure} (i.e. the relative order of action
occurrences and choices between different courses of action) of concurrent systems plays
a r\^{o}le in our results. We show that {\it interleaving bisimulation}, where the
branching structure between alternative executions is taken into account, is preserved
under safe refinements. On the other hand, we show that {\it interleaving trace
equivalence} (where the branching structure is fully neglected) is still not preserved
under these restricted refinements. To investigate safe refinements for equivalence notions between
these two extremes in the linear time -- branching time spectrum has to be left for future research.
\section{Basic Notions}
We consider systems which are capable of performing actions from a
given set {\it Act} of action names. By an action we understand here any
activity which is considered as an conceptual entity on a chosen level
of abstraction. We will not distinguish external and internal actions;
we do not consider abstraction by hiding of actions in this paper.
We will sometimes give process algebra terms for examples to make them
easier to understand: $+$ will denote choice (as in CCS), $\mid$ will denote
parallel composition (without communication), $a,b,...\in Act$ denote
actions, and ; denotes a general sequential composition operator (like
the one of ACP). The semicolon will sometimes be omitted and we use the
usual precedence rule that ; binds stronger than the other operators.
However this notation is only used for intuition; formally our results
are established for {\it event structures}.
We will describe a concurrent system by a set of events where each
event corresponds to an occurrence of some action. Therefore, events are
labelled by action names.
The simplest form of event structures has been introduced in [NPW]
and is usually referred to as {\it prime event structures} with binary
conflicts. A labelled prime event structure is a tuple $(E,<,\#,l)$ where
$E$ is the set of events, $<~ \subseteq E \times E$ is an (irreflexive)
partial order (the {\it causality relation}), $~\#~ \subseteq E \times E$ is
the so-called {\it conflict relation}, and $l : E \rightarrow Act$ specifies
the labelling of events by action names.
As usual, we require $<$ to satisfy the {\it axiom of finite causes}\/; that is,
any event may have only finitely many predecessors. Furthermore, $\#$ is
required to be irreflexive and symmetric and to respect the axiom of conflict
heredity: $\forall d,e,f \in E : d~\#~e \wedge d < f \Longrightarrow e~\#~f.$
A prime event structure represents a concurrent system in the following way:
action names $a \in Act$ represent actions the system may perform, an event
$e \in E$ labelled with $a$ represents an occurrence of $a$ during a possible
run of the system, $d < e$ means that $d$ is a prerequisite for $e$ and
$d~\#~e$ means that $d$ and $e$ cannot happen both in the same run.
The behaviour of a prime event structure is described by explaining which
subsets of events constitute possible runs of the represented system. These
subsets are called {\it configurations}. They have to be conflict-free and they
must be left-closed with respect to $<$ (all prerequisites for any event
occurring in the run must also occur).
As shown in [GG a], prime event structures are well suited to define a notion
of action refinement, as long as actions are not refined by behaviours
containing conflicts.
But as a consequence of the axioms explained above, it is cumbersome to define
a more general notion of refinement directly for prime event structures.
Whenever a given event occurs, it has to be ``enabled" by a unique set of events
that is independent of the particular run of the system, namely by all its
predecessors according to the causality relation. However, when refining
$a$ by $a_1 + a_2$ in $a\,;b$, $b$ should occur alternatively caused by $a_1$ or
by $a_2$. In prime event structures, this may only be modelled by duplicating the
$b$-event, leading to complicated definitions and proofs. Hence more expressive event
structure representations are being used for refinement. {\it Free event structures}\/
as defined in [DD a] seem to be weakest extension of prime event structures to allow
refinements with conflicts in a straightforward way. However, difficulties with the
interpretation of the notion of causality in this model lead in [DD b] to a restriction
such that prime event structures are no longer a subclass. In [GG a, GG b], {\it flow
event structures} [BC] have been used which are also a convenient model for CCS. This
is the model we have chosen here as well, in order to establish our results also for
refinements with conflicts.
We will now introduce the main concepts of flow event structures following
closely [Boudol].
\pagebreak
\begin{Definition}{flow-es} { }
A {\it (labelled) flow event structure (over an
alphabet \Act)} is a 4-tuple \\ ${\cal E} = (E,\prec,\#,l)$, where
\begin{itemize}
\item $ E $ is a set of {\it events},
\item $ \prec~\subseteq E \times E $ is an irreflexive relation, the
{\it flow relation},
\item $ \# \subseteq E \times E $ is a symmetric relation, the
{\it conflict relation},
\item $l: E \longrightarrow $\Act\ is the {\it labelling function}.
\end{itemize}
\end{Definition}
Let \IE\ denote the domain of flow event structures labelled over {\it Act}.
The components of ${\cal E} \in$ \IE\ will be denoted by
$E_{\cal E}, \prec_{\cal E}, \#_{\cal E}$ and $l_{\cal E}$. The index ${\cal E}$
will be omitted if clear from the context.
% ${\cal E}$ is {\it conflict-free} if $\# = \emptyset$.\\
% For $X \subseteq E_{\cal E}$, ${\cal E} \lceil X =
% (X, \prec_{\cal E}\hspace{-2mm}\lceil X, \#_{\cal E} \lceil X, l_{\cal E} \lceil X)$
% is the {\it restriction of ${\cal E}$ to $X$}.
Two flow event structures ${\cal E}$ and ${\cal F}$ are {\it isomorphic}
(${\cal E} \cong {\cal F}$) iff there exists a bijection between their
sets of events preserving $\prec,\#$ and labelling.
Often, we will not distinguish isomorphic event structures; the names of events
are not important for us.
The interpretation of the conflict and the flow relation is formalised by
defining configurations of flow event structures. Configurations must be
conflict free; in particular, self-conflicting events will never occur in any
configuration. $d \prec e$ will mean that $d$ is a {\it possible immediate cause}
for $e$. For an event to occur it is necessary that a {\it complete}
non-conflicting set of its causes has occurred. Here a set of causes is complete
if 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.
We will only consider finite configurations here. As usual, we assume
that in a finite period of time only finitely many actions may be
performed. Now the requirement says that we only consider runs which
are executable in a finite period of time. This is no restriction since
the infinite configurations which are usually considered are completely
determined by the finite ones (see e.g. [Boudol]).
\begin{Definition}{configurations} {Let ${\cal E} \in $ \IE.}
\begin{itemize}
\item [(i)] $X \subseteq E$ is {\it left-closed up to conflicts} iff
$\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 $f \prec e$ and $d~\#~f$.
$X \subseteq E$ is {\it conflict-free} iff $\#_{\cal E} \lceil
X = \emptyset$.
\item [(ii)]
$X \subseteq E$ is a {\it (finite) configuration} of ${\cal E}$ iff
$X$ is finite, left-closed up to conflicts and conflict-free and does
not contain a
causality cycle: $<_X~ := (\prec \cap(X \times X))^+$ is irreflexive.
$\conf ({\cal E})$ denotes the set of all (finite) configurations of
${\cal E}$.
\item[(iii)]
A configuration $X \in \conf ({\cal E})$ is called {\it maximal}
iff $X \subseteq Y \in \conf ({\cal E})$ implies $X = Y$.
It is {\it complete} iff
$\forall d \in E : d \not\in X \Rightarrow \exists e \in X$ with $d~\#~e$.
\end{itemize}
\end{Definition}
The relation $<_X$ expresses causal dependence in the configuration $X$.
Note that prime event structures are special flow event structures
defining $d \prec e$ iff $d < e$. In prime event structures, the
requirement of left-closedness up to conflicts for configurations
reduces to left-closedness: $\forall d,e \in E :$ if $e \in X \wedge d <
e$ then $d \in X$; furthermore, in each configuration $X$, the relation
$<_X$ coincides with $<$.
However in prime event structures every maximal configuration is complete,
whereas in flow event structures this need not be the case (although every
complete configuration must be maximal). In [GG c] the difference between
complete and maximal configurations is used to model deadlock behaviour:
complete configurations indicate successful termination, whereas incomplete
maximal configurations model deadlocks.
The following observations may offer some additional motivation for the
definition of configurations above.
\begin{Definition}{enabling}{Let ${\cal E} \in$ \IE, $X \in \conf ({\cal
E})$.}
\begin{itemize}
\item[(i)]
$X$ {\it enables} $e \in E$ iff $e\notin X$ and $X \cup \{e\} \in \conf ({\cal
E})$. \item[(ii)]
A subset $Y \subseteq X$ is a {\em
prefix} of $X$ iff $\forall d \in X,\ e \in Y:\ d <_X e \Rightarrow d
\in Y$ (i.e. $Y$ is left-closed in $X$ w.r.t. $<_X$).
\end{itemize}
\end{Definition}
\begin{Proposition}{enabling}{Let ${\cal E} \in$ \IE, $X \in \conf ({\cal
E})$.} \begin{itemize}
\item[(i)] $X$ enables $e$ iff $e \not\in X, \neg(\exists d \in X$ with $d \#
e)$ and $\forall d \prec e$ we have $d \in X \vee \exists f \in X$ with $f \prec
e$ and $d\# f$. \item[(ii)] $X$ can be written as $X = \{e_1, \dots , e_n\}$ such
that for $k < n: \{e_1, \dots ,e_k\} $ enables $e_{k+1}$. \item[(iii)] For $Y
\subseteq X$, $Y \in \conf ({\cal E})$ iff $Y$ is a prefix of $X$.
\end{itemize} \end{Proposition}
{\bf Proof\ \ } See [Boudol]. \qed
We now define transition relations between configurations, describing which
event or which action may occur in a configuration and which configuration
may then be obtained.
\begin{Definition}{transitions}{Let ${\cal E} \in $ \IE.}
$ X \buildrel {e} \over \longrightarrow_{\cal E} X' $ iff
$X$ enables $e$ and $X'=X\cup\{e\}$.\\
$ X \buildrel {a} \over \longrightarrow_{\cal E} X' $ iff
$ X \buildrel {e} \over \longrightarrow_{\cal E} X'$ and $ l(e) = a\in\Act$.
\end{Definition}
The index ${\cal E}$ is omitted if clear from the context.
Next we introduce a relation $co_X$ expressing when two events are
{\it concurrent} (independent) within a configuration $X$, as well as a global
relation $co$, expressing {\it possible concurrency}, and show that the
relations correspond. Furthermore we define when there is a {\it choice}
between two events.
\begin{Definition}{choice}
{Let ${\cal E} \in$ \IE.}
\begin{itemize}
\item[(i)]
For $X \in \conf ({\cal E})$, let $co_X \subseteq X \times X$ be defined by \\
$d~co_X~e $ iff $\neg(d <_X e \vee e <_X d) $ .
\item[(ii)] $co \subseteq E \times E$ is defined by \\
$d~co~e$ iff $\exists X \in \conf ({\cal E})$, $X$ enables both $d$ and $e$
and $X \cup \{d,e\} \in \conf ({\cal E})$.
\item[(iii)] $ch \subseteq E \times E$ is defined by \\
$d~ch~e$ iff $\exists X \in \conf ({\cal E})$, $X$ enables both $d$ and $e$
and $X \cup \{d,e\} \not\in \conf ({\cal E})$.
\end{itemize}
\end{Definition}
\begin{Proposition}{choice}
{Let ${\cal E} \in$ \IE, $d ,e \in E$.}
\begin{itemize}
\item[(i)]
$d~co~e~\Leftrightarrow ~\exists X \in \conf ({\cal E})$ with $d~co_X~e$.
\item[(ii)]
$d~ch~e~\Rightarrow~d~\#~e$.
\end{itemize}
\end{Proposition}
{\bf Proof\ \ } \\
(i): \\
``$\Rightarrow$":
Let $d~co~ e$. Then there exists $X\in\conf({\cal E})$ with $d,e$ both enabled
by $X$. \\ Let $Y:=X\cup \{d,e\}$. We show that $d~co_Y~ e$.\\
Assume $d<_Y e$. Then $X \cup \{e\}$ would not be a prefix of $Y$, hence $X \cup
\{e\}$ would not be a configuration and $e$ not enabled by $X$.
Thus $\neg (d<_Y e)$ and by symmetry $\neg (e<_Y d)$.
``$\Leftarrow$":
Let $X \in \conf ({\cal E})$ with $d~co_X~e$.
Let $X' = X - \{f \in X \mid d <_X f \vee e <_X f\}$.\\
$d,e \in X'$, since $d,e \in X$ and $d$ and $e$ are not in $<_X$-relation. \\
Moreover $d$ and $e$ are maximal in $X'$ w.r.t. $<_X$.\\
Let $X_1 := X'-\{d\}$, $X_2 := X'-\{e\}$, $X'' := X' - \{d,e\}$.\\
Then $X',X_1,X_2,X'' \in \conf ({\cal E})$ with proposition \ref{enabling}(iii)
and $d ~co~e$.
(ii):\\
Suppose $d~ch~e$, but $\neg(d~\#~e)$.
We show that for each configuration $X$ enabling $d$ and $e$, also $X' := X \cup
\{d,e\}$ is a configuration.\\
Let $X \in \conf ({\cal E})$, with
$X \buildrel {d} \over \longrightarrow X_1$ and
$X \buildrel {e} \over \longrightarrow X_2$.
Let $X' := X \cup \{d,e\}$.
$X'$ is finite, since $X \in \conf ({\cal E})$.
$X'$ is conflict-free, since $X_1, X_2 \in \conf ({\cal E})$ and
$\neg(d~\#~e)$.
$X'$ is left-closed up to conflicts:\\
Suppose $f \in X'$, $g \in E-X'$ and $g \prec f$. Then $f \in X_i$ for $i=1$ or
$i=2$ and $g \not\in X_i$, so $\exists h \in X_i \subseteq X'$ with $h \prec f$
and $g \# h$, since $X_i \in \conf ({\cal E})$.
$X'$ contains no cycles w.r.t. $\prec$:\\
Suppose $X'$ contains a causality cycle. Since $X_2 \in \conf ({\cal E})$ this
cycle must contain $d$. However, we will show that there is no $c \in X'$ with
$d \prec c$. Since $X,X_1 \in \conf ({\cal E})$, $X$ must be a prefix of $X_1$
by proposition \ref{enabling}(iii), implying that $d$ is maximal in $X_1$.
Thus the only candidate for $c$ is $e$. So suppose $d \prec e$. Since
$d \not\in X_2$ and $e
\in X_2 \in \conf ({\cal E})$ there must be an $f \in X_2 \subseteq X'$ with $f
\prec e$ and $d \# f$, contradicting the conflict-freeness of $X'$.
Thus $X' \in \conf ({\cal E})$.
\qed
For prime event structures, the choice relation coincides with the
non-inherited conflicts.
\begin{Definition}{immediate-conflict}{Let ${\cal E}\in$ \IE\ be a prime
event structure.}
$\#^1\subseteq E\times E$ ({\it immediate conflict}) is defined by\\
$d~\#^1 e$ iff $d~\#~e$, $f < d \Rightarrow \neg(f~\#~e) $ and $f < e
\Rightarrow \neg(f~\#~d) $. \end{Definition}
\begin{Proposition}{immediate-conflict}{Let ${\cal E}\in$ \IE\ be a prime
event structure, $d,e\in E$.} Then $d~ch~e ~\Leftrightarrow ~ d~\#^1 e$.
\end{Proposition}
{\bf Proof\ \ } \\
``$\Rightarrow$": Let $d~ch~e$. Then there exists $X\in \conf ({\cal E})$
enabling both $d$ and $e$. \\ $d\#e$ by proposition \ref{choice}.\\
Assume there is an $f$ with $f