\documentclass{llncs}
\pagestyle{plain}
\usepackage{amssymb}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% New Commands %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\asym}{\rightsquigarrow} % asymmetric conflict
\newfont{\fsc}{eusm10} % frenchscript letters
\newcommand{\pow}{\mbox{\fsc P}} % french P (powerset)
%%%%%%%%%%%%%%%%%%%%%%% end of use amstex packages %%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\monus}{~~\makebox[0pt]{\LARGE$\cdot$}\makebox[0pt]{$-$}~~}
\newcommand{\defeq}{\raisebox{-1pt}[0pt][0pt]
{$\stackrel{\it def}{=}$}} % equal by definition
\newcommand{\Con}{{\it Con}} % consistent set (ES)
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}} % no vertical space
\newcommand{\tuple}[1]{\plat{ % tuple, for structures
\stackrel{\mbox{\tiny $/$}}
{\raisebox{-.3ex}[.3ex]{\tiny $\backslash$}}
\!\!#1\!\!
\stackrel{\mbox{\tiny $\backslash$}}
{\raisebox{-.3ex}[.3ex]{\tiny $/$}} }}
\newcommand{\goto}[1]{\stackrel{#1}{\longrightarrow}} % transition
\newcommand{\rest}{ % restriction operator
\unitlength 1mm
\begin{picture}(2.16,3.2)
\thinlines
\put(1.12,-0.48){\line(0,1){3.52}}
\put(0.8,1.6){\tiny $\backslash$}
\end{picture} }
\spnewtheorem{observation}{Observation}{\bfseries}{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% References %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\df}[1]{Definition~\ref{df-#1}}
\newcommand{\pr}[1]{Prop.~\ref{pr-#1}}
\newcommand{\cor}[1]{Cor.~\ref{cor-#1}}
\newcommand{\obs}[1]{Obs.~\ref{obs-#1}}
\newcommand{\ex}[1]{Example~\ref{ex-#1}}
\newcommand{\fig}[1]{Fig.~\ref{fig-#1}}
\newcommand{\sect}[1]{Sect.~\ref{sec-#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Abbreviations %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\bbbn} % natural numbers
\newcommand{\IQ}{\bbbq} % rational numbers
\newcommand{\fE}{{\cal E}} % function into \IE
\newcommand{\fN}{{\cal N}} % function into nets
\newcommand{\fL}{{\cal L}} % left-closed conf.
\newcommand{\eE}{{\rm E}} % event structure
\newcommand{\eF}{{\rm F}} % event structure
\newcommand{\eN}{{\rm N}} % petri net
\newcommand{\eP}{{\rm P}} % petri net
\newcommand{\eT}{{\rm T}} % propositional theory
\newcommand{\turn}{\vdash} % turnstile
\newcommand{\implies}{\Rightarrow}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\advance\textheight 2.8em
\begin{document}
\advance\textheight -2.8em
\title{Event Structures for Resolvable Conflict\thanks{To appear in:
Vaclav Koubek \& Jan Kratochvil, editors: Proceedings 29$^{th}$
International Symposium on {\sl Mathematical Foundations of
Computer Science} (MFCS 2004), Prague, Czech Republic, LNCS,
Springer, August 2004. ~~~~~~~~~~~ \hfill \copyright\ Springer-Verlag
This work was supported by EPSRC under grant number GR/S22097.}}
\author{Rob van Glabbeek \and Gordon Plotkin}
\institute{Laboratory for Foundations of Computer Science\\
School of Informatics,
University of Edinburgh\\
Edinburgh EH9 3JZ, UK\\
\email{rvg@cs.stanford.edu~~~gdp@inf.ed.ac.uk}}
\maketitle
\begin{abstract}
We propose a generalisation of Winskel's event structures, matching
the expressive power of arbitrary Petri nets. In particular, our
event structures capture resolvable conflict, besides disjunctive
and conjunctive causality.
\end{abstract}
\section{Introduction}\label{sec-introduction}
Event structures were introduced in {\sc Nielsen, Plotkin \& Winskel}
\cite{NPW81} as abstract representations of the behaviour of safe
Petri nets. They describe a concurrent system by means of a set of
events, representing action occurrences, and for every two events $d$
and $e$ it is specified whether one of them is a prerequisite for the
other, whether they exclude each other, or---the remaining
case---whether they may happen concurrently. A formal definition can
be found in \fig{definitions}. The behaviour of an event structure is
formalised by associating to it a family of {\em configurations},
these being sets of events that occur during (partial) runs of the
represented system. A configuration $x$ can also be understood as a
state of the represented system, namely the state reached after
performing all events in $x$.
\begin{figure}\vspace{-2em}
%\input{prime}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
\graphtemp=.5ex\advance\graphtemp by 0.098in
\rlap{\kern 0.098in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 0.098in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
\special{pn 8}%
\special{pa 98 177}%
\special{pa 98 413}%
\special{fp}%
\special{sh 1.000}%
\special{pa 123 374}%
\special{pa 98 413}%
\special{pa 73 374}%
\special{pa 123 374}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 0.295in\lower\graphtemp\hbox to 0pt{\hss $\#$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 0.492in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
\special{ar 2067 98 98 98 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.098in
\rlap{\kern 2.067in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 2067 197}%
\special{pa 2067 394}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2092 354}%
\special{pa 2067 394}%
\special{pa 2042 354}%
\special{pa 2092 354}%
\special{fp}%
\special{pa 1969 591}%
\special{pa 2165 591}%
\special{pa 2165 394}%
\special{pa 1969 394}%
\special{pa 1969 591}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 2.067in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
\special{pa 2067 591}%
\special{pa 2067 787}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2092 748}%
\special{pa 2067 787}%
\special{pa 2042 748}%
\special{pa 2092 748}%
\special{fp}%
\special{ar 2067 886 98 98 0 6.28319}%
\special{pa 2067 984}%
\special{pa 2067 1181}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2092 1142}%
\special{pa 2067 1181}%
\special{pa 2042 1142}%
\special{pa 2092 1142}%
\special{fp}%
\special{pa 1969 1378}%
\special{pa 2165 1378}%
\special{pa 2165 1181}%
\special{pa 1969 1181}%
\special{pa 1969 1378}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 1.280in
\rlap{\kern 2.067in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
\special{ar 2461 886 98 98 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 2.461in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 2461 984}%
\special{pa 2461 1181}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2486 1142}%
\special{pa 2461 1181}%
\special{pa 2436 1142}%
\special{pa 2486 1142}%
\special{fp}%
\special{pa 2362 1378}%
\special{pa 2559 1378}%
\special{pa 2559 1181}%
\special{pa 2362 1181}%
\special{pa 2362 1378}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 1.280in
\rlap{\kern 2.461in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
\special{pa 2391 955}%
\special{pa 2165 1181}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2211 1171}%
\special{pa 2165 1181}%
\special{pa 2176 1136}%
\special{pa 2211 1171}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.098in
\rlap{\kern 1.083in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 1.083in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
\special{pa 1083 177}%
\special{pa 1083 413}%
\special{fp}%
\special{sh 1.000}%
\special{pa 1108 374}%
\special{pa 1083 413}%
\special{pa 1058 374}%
\special{pa 1108 374}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 1.083in\lower\graphtemp\hbox to 0pt{\hss $ab$\hss}}%
\special{pa 1083 571}%
\special{pa 1083 807}%
\special{fp}%
\special{sh 1.000}%
\special{pa 1108 768}%
\special{pa 1083 807}%
\special{pa 1058 768}%
\special{pa 1108 768}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.098in
\rlap{\kern 1.476in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
\special{pa 1161 98}%
\special{pa 1398 98}%
\special{fp}%
\special{sh 1.000}%
\special{pa 1358 73}%
\special{pa 1398 98}%
\special{pa 1358 123}%
\special{pa 1358 73}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 1.476in\lower\graphtemp\hbox to 0pt{\hss $ac$\hss}}%
\special{pa 1476 177}%
\special{pa 1476 413}%
\special{fp}%
\special{sh 1.000}%
\special{pa 1501 374}%
\special{pa 1476 413}%
\special{pa 1451 374}%
\special{pa 1501 374}%
\special{fp}%
\special{pa 1161 492}%
\special{pa 1398 492}%
\special{fp}%
\special{sh 1.000}%
\special{pa 1358 467}%
\special{pa 1398 492}%
\special{pa 1358 517}%
\special{pa 1358 467}%
\special{fp}%
\special{pa 1138 154}%
\special{pa 1421 436}%
\special{da 0.050}%
\special{sh 1.000}%
\special{pa 1411 391}%
\special{pa 1421 436}%
\special{pa 1375 426}%
\special{pa 1411 391}%
\special{fp}%
\graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
\advance\graphtemp by .5ex\advance\graphtemp by 1.083in
\rlap{\kern 0.295in\lower\graphtemp\hbox to 0pt{\hss $b\implies a$\hss}}%
\graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
\advance\graphtemp by .5ex\advance\graphtemp by 1.083in
\rlap{\kern 0.295in\lower\graphtemp\hbox to 0pt{\hss $\neg(b \wedge c)$\hss}}%
\hbox{\vrule depth1.378in width0pt height 0pt}%
\kern 2.559in
}%
}%
\begin{minipage}[t]{2in}
\caption{
An event structure as in~\cite{NPW81} and its family of
configurations, together with a transition relation between the
configurations indicating how one can move from one state to another
by concurrently performing some events. The same system is also
represented by means of a pro-positional theory \cite{GP95} and a
Petri net.}
\end{minipage}
\hfill\raise -1em\box\graph
\label{fig-prime}
\\[1.2em]\normalsize
{\sc Winskel} later proposed a variety of other notions of event
structure. In \mbox{\cite{Wi87a,Wi89}} he presented event structures
where instead of indicating which events are prerequisites of other
events, it is indicated which {\em sets} of events $X$ are {\em
possible} prerequisites of events $e$, written $X\turn e$. This
enables one to model {\em disjunctive causality} (cf.\
\fig{disjunctive}), the phenomenon that an event is causally dependent
on a disjunction of other events occurring in the same system run.
The event struc-\linebreak~\vspace{-3.4em}
\end{figure}
\begin{figure}
The event structures of {\sc Nielsen, Plotkin \& Winskel} are triples
$\eE = \tuple{E,\leq,\#}$ where\vspace{-2ex}
\begin{itemize}
\item $E$ is a set of {\it events},
\item $\leq \;\subseteq E \times E$ is a partial order,
the {\em causality relation},
\item $\# \subseteq E\times E$ is an irreflexive, symmetric relation,
the {\em conflict relation}, satisfying
the {\em principle of conflict heredity}:
$\forall d,e,f \in E.~ d \leq e \wedge d \# f \Rightarrow e \# f.$
\end{itemize}\vspace{-1ex}
The set $L(\eE)$ of configurations of such a structure
consists of those $X \subseteq E$ which are\vspace{-2ex}
\begin{itemize}
\item {\em conflict-free}: $\# \rest (X \times X) = \emptyset$,
\item and {\em left-closed}: $\forall d,e \in E.~ d \leq e \in X
\Rightarrow d \in X$.
\end{itemize}
The prime event structures of {\sc Winskel} \cite{Wi89} are defined
likewise, but additionally requiring the {\em principle of finite causes}:
$\{d \in E \mid d \leq e\} \mbox{ is finite for all } e \in E.$
\\[1em]
The event structures of {\sc Winskel} \cite{Wi87a} are defined as
triples $\eE = \tuple{E,Con,\turn\;}$ where\vspace{-2ex}
\begin{itemize}
\item $E$ is a set of {\em events},
\item $Con \subseteq \pow_{\it fin}(E)$, satisfying
% is a nonempty {\em consistency predicate} such that
$\emptyset\in Con$ and
$Y \subseteq X \in Con \Rightarrow Y\in Con$, and
\item $\turn\, \subseteq Con \times E$ is the {\em
enabling relation}, which satisfies $X \turn e \wedge X
\subseteq Y\in Con \Rightarrow Y\turn e$.
\end{itemize}\vspace{-2ex}
Such a structure is {\em stable} if
$X \turn e \wedge Y \turn e \wedge \Con(X \cup Y \cup \{e\})
\Rightarrow X\cap Y \turn e.$\\[1ex]
The set $S(\eE)$ of configurations of such a structure consists of
those $X \subseteq E$ which are\vspace{-2ex}
\begin{itemize}
\item {\em consistent}: every finite subset of $X$ is in $Con$,
\item and {\em secured}: $\forall e \in X.~\exists e_0, \ldots,e_n \in X.~
e_n=e \wedge \forall i\leq n.~ \{e_0,...,e_{i-1}\}\turn e_{i}$.
\end{itemize}
The event structures of {\sc Winskel} \cite{Wi89} are defined
likewise, except that the consistency predicate $\Con$ is generated by
a given symmetric, irreflexive {\em conflict relation} $\# \subseteq E
\times E$, through $\Con(X) \Leftrightarrow (X\mbox{ finite})\wedge
\forall d,e \in X.~\neg (d \# e).$
\\[1em]
The prime event structures of {\sc Winskel} \cite{Wi87a} are defined as
triples $\eE = \tuple{E,Con,\leq\;}$ combining the requirements for
$\Con$ from \cite{Wi87a} with those for $\leq$ from \cite{Wi89}, and
additionally satisfying $\{e\} \in \Con$ for all $e \in E$ and
$d \leq e \in X \in \Con \Rightarrow X \cup \{d\} \in \Con$.
\caption{Formal definitions of 5 types of event structures}
\label{fig-definitions}
\vspace{1.9em}\normalsize tures in \cite{Wi87a} moreover allow one to
express for any finite set of events whether it is {\em in conflict},
i.e.\ can not happen in full in the same run; in \cite{NPW81,Wi89}
this can only be specified for sets with two events.
~~~~However, not every Petri net can be faithfully represented as an
event structure from \cite{NPW81,Wi87a,Wi89}, due to the phenomenon of
{\em resolvable conflict} illustrated in \fig{resolvable}. In order to
capture this type of behaviour, we simply extend the notion of event
structure from \cite{Wi87a,Wi89} by allowing enablings of the form $X
\turn Y$, with $X$ and $Y$ sets of events. The enablings $X \turn Y$
do not place any restrictions on the occurrence of individual events
in $Y$, but say that for {\em all} events in $Y$ to occur, for some
set $X$ with $X \turn Y$ the events in $X$ have to happen first.
\begin{definition}\rm\label{df-event structure}
An {\em event structure} is a pair $\eE = \tuple{E,\turn\;}$ with
\vspace{-1ex}
\begin{itemize}
\item $E$ a set of {\em events},
\item $\turn \; \subseteq \pow(E) \times \pow(E)$, the {\em
enabling relation}.
\end{itemize}
\end{definition}
With this type of event structure we do not need a separate conflict
or consistency relation; that a set $X$ of events is in irresolvable
conflict can be expressed by not
\end{figure}
\begin{figure}
\vspace{-1em}
%\input{disjunctive}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
\special{pn 8}%
\special{ar 3543 886 98 98 0 6.28319}%
\special{pa 3543 984}%
\special{pa 3543 1181}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3568 1142}%
\special{pa 3543 1181}%
\special{pa 3518 1142}%
\special{pa 3568 1142}%
\special{fp}%
\special{pa 3445 1378}%
\special{pa 3642 1378}%
\special{pa 3642 1181}%
\special{pa 3445 1181}%
\special{pa 3445 1378}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 1.280in
\rlap{\kern 3.543in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
\special{ar 3150 98 98 98 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.098in
\rlap{\kern 3.150in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 3150 197}%
\special{pa 3150 394}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3175 354}%
\special{pa 3150 394}%
\special{pa 3125 354}%
\special{pa 3175 354}%
\special{fp}%
\special{pa 3051 591}%
\special{pa 3248 591}%
\special{pa 3248 394}%
\special{pa 3051 394}%
\special{pa 3051 591}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 3.150in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
\special{pa 3248 591}%
\special{pa 3474 816}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3464 771}%
\special{pa 3474 816}%
\special{pa 3428 806}%
\special{pa 3464 771}%
\special{fp}%
\special{ar 3937 98 98 98 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.098in
\rlap{\kern 3.937in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 3937 197}%
\special{pa 3937 394}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3962 354}%
\special{pa 3937 394}%
\special{pa 3912 354}%
\special{pa 3962 354}%
\special{fp}%
\special{pa 3839 591}%
\special{pa 4035 591}%
\special{pa 4035 394}%
\special{pa 3839 394}%
\special{pa 3839 591}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 3.937in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
\special{pa 3839 591}%
\special{pa 3613 816}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3658 806}%
\special{pa 3613 816}%
\special{pa 3623 771}%
\special{pa 3658 806}%
\special{fp}%
\special{ar 3150 886 98 98 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 3.150in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 3219 955}%
\special{pa 3445 1181}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3435 1136}%
\special{pa 3445 1181}%
\special{pa 3399 1171}%
\special{pa 3435 1136}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.098in
\rlap{\kern 1.969in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 1.575in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
\special{pa 1913 154}%
\special{pa 1630 436}%
\special{fp}%
\special{sh 1.000}%
\special{pa 1676 426}%
\special{pa 1630 436}%
\special{pa 1641 391}%
\special{pa 1676 426}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 1.575in\lower\graphtemp\hbox to 0pt{\hss $ac$\hss}}%
\special{pa 1575 571}%
\special{pa 1575 807}%
\special{fp}%
\special{sh 1.000}%
\special{pa 1600 768}%
\special{pa 1575 807}%
\special{pa 1550 768}%
\special{pa 1600 768}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 1.280in
\rlap{\kern 1.969in\lower\graphtemp\hbox to 0pt{\hss $abc$\hss}}%
\special{pa 1630 942}%
\special{pa 1913 1224}%
\special{fp}%
\special{sh 1.000}%
\special{pa 1903 1178}%
\special{pa 1913 1224}%
\special{pa 1867 1214}%
\special{pa 1903 1178}%
\special{fp}%
\special{pa 1628 598}%
\special{pa 1916 1174}%
\special{da 0.050}%
\special{sh 1.000}%
\special{pa 1920 1127}%
\special{pa 1916 1174}%
\special{pa 1876 1150}%
\special{pa 1920 1127}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 1.969in\lower\graphtemp\hbox to 0pt{\hss $ab$\hss}}%
\special{pa 1630 548}%
\special{pa 1913 830}%
\special{fp}%
\special{sh 1.000}%
\special{pa 1903 785}%
\special{pa 1913 830}%
\special{pa 1867 820}%
\special{pa 1903 785}%
\special{fp}%
\special{pa 1969 217}%
\special{pa 1969 768}%
\special{da 0.050}%
\special{sh 1.000}%
\special{pa 1994 728}%
\special{pa 1969 768}%
\special{pa 1944 728}%
\special{pa 1994 728}%
\special{fp}%
\special{pa 1969 965}%
\special{pa 1969 1201}%
\special{fp}%
\special{sh 1.000}%
\special{pa 1994 1161}%
\special{pa 1969 1201}%
\special{pa 1944 1161}%
\special{pa 1994 1161}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 2.362in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
\special{pa 2024 154}%
\special{pa 2307 436}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2296 391}%
\special{pa 2307 436}%
\special{pa 2261 426}%
\special{pa 2296 391}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 2.362in\lower\graphtemp\hbox to 0pt{\hss $bc$\hss}}%
\special{pa 2307 548}%
\special{pa 2024 830}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2070 820}%
\special{pa 2024 830}%
\special{pa 2034 785}%
\special{pa 2070 820}%
\special{fp}%
\special{pa 2362 571}%
\special{pa 2362 807}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2387 768}%
\special{pa 2362 807}%
\special{pa 2337 768}%
\special{pa 2387 768}%
\special{fp}%
\special{pa 2309 598}%
\special{pa 2021 1174}%
\special{da 0.050}%
\special{sh 1.000}%
\special{pa 2061 1150}%
\special{pa 2021 1174}%
\special{pa 2017 1127}%
\special{pa 2061 1150}%
\special{fp}%
\special{pa 2307 942}%
\special{pa 2024 1224}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2070 1214}%
\special{pa 2024 1224}%
\special{pa 2034 1178}%
\special{pa 2070 1214}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 0.394in\lower\graphtemp\hbox to 0pt{\hss $\begin{array}{c@{~}c@{~}c}E&=&\{a,b,c\}\!\!\!\!\!\!\!\\ \# &=& \emptyset\\ \emptyset & \turn & a \\ \emptyset & \turn & b \\ a & \turn & c \\ b & \turn & c \\ \end{array}$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 1.280in
\rlap{\kern 0.394in\lower\graphtemp\hbox to 0pt{\hss $c \implies (a\vee b)$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 4.331in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 1.280in
\rlap{\kern 4.331in\lower\graphtemp\hbox to 0pt{\hss $c_1$\hss}}%
\special{pa 4331 965}%
\special{pa 4331 1201}%
\special{fp}%
\special{sh 1.000}%
\special{pa 4356 1161}%
\special{pa 4331 1201}%
\special{pa 4306 1161}%
\special{pa 4356 1161}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 1.280in
\rlap{\kern 4.528in\lower\graphtemp\hbox to 0pt{\hss $\#$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 4.724in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 1.280in
\rlap{\kern 4.724in\lower\graphtemp\hbox to 0pt{\hss $c_2$\hss}}%
\special{pa 4724 965}%
\special{pa 4724 1201}%
\special{fp}%
\special{sh 1.000}%
\special{pa 4749 1161}%
\special{pa 4724 1201}%
\special{pa 4699 1161}%
\special{pa 4749 1161}%
\special{fp}%
\hbox{\vrule depth1.378in width0pt height 0pt}%
\kern 4.823in
}%
}%
\centerline{\raise 1em\box\graph}
\caption{A system with {\em disjunctive causality} represented as an
event structure of \cite{Wi89}, a family of configurations with
transition relation, a propositional theory and a Petri net.
The last picture is the best representation of the same system as an
event structure from \cite{NPW81}. It requires the decomposition of
the event $c$, which is causally dependent on the disjunction of $a$
and $b$, into two events $c_1$ and $c_2$, only one of which may happen:
$c_1$ being causally dependent only on $a$, and $c_2$ on $b$.
Antoni Mazurkiewicz argued against the accuracy of this representation
by letting $a$ and $b$ be $\pounds 1$ contributions of two school
children to buy a present for their teacher. The act of buying the
present, which only costs $\pounds 1$, is represented by $c$. Now the
event structure from \cite{NPW81} has two maximal runs, representing
that the present is bought from the contribution from either one child
or the other. The event structure from \cite{Wi89} on the other hand
has only one possible run, in which the buying of the present is
caused by the disjunction of the two contributions. The latter would
be a fairer description of the intended state of affairs.}
\label{fig-disjunctive}
\vspace{1.9em}\normalsize
having any enabling of the form $Y\turn X$. When describing an event
structure of \cite{Wi87a,Wi89} as one of ours, we have to omit
enablings $X\turn e$ with $\{e\}\not\in \Con$ and add enablings
$\emptyset\turn X$ for sets $X$ with $|X|\neq 1$ and $\Con(X)$, and
also for infinite $X$.
~~~~In \sect{configurations} we discuss various forms of behavioural
equivalence on these new event structures.
In \sect{brands} we show how they include the classical event
structures, thereby establishing their {\em generality}.
In \sect{nets} we consider the relation\linebreak~\vspace{-1em}
\end{figure}
\begin{figure}
%\input{resolvable}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
\special{pn 8}%
\special{ar 551 98 98 98 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.098in
\rlap{\kern 0.551in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 551 197}%
\special{pa 551 394}%
\special{fp}%
\special{sh 1.000}%
\special{pa 576 354}%
\special{pa 551 394}%
\special{pa 526 354}%
\special{pa 576 354}%
\special{fp}%
\special{pa 453 591}%
\special{pa 650 591}%
\special{pa 650 394}%
\special{pa 453 394}%
\special{pa 453 591}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 0.551in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
\special{pa 551 591}%
\special{pa 551 787}%
\special{fp}%
\special{sh 1.000}%
\special{pa 576 748}%
\special{pa 551 787}%
\special{pa 526 748}%
\special{pa 576 748}%
\special{fp}%
\special{ar 551 886 98 98 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 0.551in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{ar 157 886 98 98 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 0.157in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 157 984}%
\special{pa 157 1181}%
\special{fp}%
\special{sh 1.000}%
\special{pa 182 1142}%
\special{pa 157 1181}%
\special{pa 132 1142}%
\special{pa 182 1142}%
\special{fp}%
\special{pa 59 1378}%
\special{pa 256 1378}%
\special{pa 256 1181}%
\special{pa 59 1181}%
\special{pa 59 1378}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 1.280in
\rlap{\kern 0.157in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
\special{pa 482 955}%
\special{pa 256 1181}%
\special{fp}%
\special{sh 1.000}%
\special{pa 301 1171}%
\special{pa 256 1181}%
\special{pa 266 1136}%
\special{pa 301 1171}%
\special{fp}%
\special{ar 945 886 98 98 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 0.945in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 945 984}%
\special{pa 945 1181}%
\special{fp}%
\special{sh 1.000}%
\special{pa 970 1142}%
\special{pa 945 1181}%
\special{pa 920 1142}%
\special{pa 970 1142}%
\special{fp}%
\special{pa 846 1378}%
\special{pa 1043 1378}%
\special{pa 1043 1181}%
\special{pa 846 1181}%
\special{pa 846 1378}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 1.280in
\rlap{\kern 0.945in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
\special{pa 621 955}%
\special{pa 846 1181}%
\special{fp}%
\special{sh 1.000}%
\special{pa 836 1136}%
\special{pa 846 1181}%
\special{pa 801 1171}%
\special{pa 836 1136}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.098in
\rlap{\kern 3.386in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 2.992in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
\special{pa 3330 154}%
\special{pa 3048 436}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3093 426}%
\special{pa 3048 436}%
\special{pa 3058 391}%
\special{pa 3093 426}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 2.992in\lower\graphtemp\hbox to 0pt{\hss $ac$\hss}}%
\special{pa 2992 571}%
\special{pa 2992 807}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3017 768}%
\special{pa 2992 807}%
\special{pa 2967 768}%
\special{pa 3017 768}%
\special{fp}%
\special{pa 3333 204}%
\special{pa 3045 780}%
\special{da 0.050}%
\special{sh 1.000}%
\special{pa 3085 756}%
\special{pa 3045 780}%
\special{pa 3040 734}%
\special{pa 3085 756}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 1.280in
\rlap{\kern 3.386in\lower\graphtemp\hbox to 0pt{\hss $abc$\hss}}%
\special{pa 3048 942}%
\special{pa 3330 1224}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3320 1178}%
\special{pa 3330 1224}%
\special{pa 3285 1214}%
\special{pa 3320 1178}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 3.386in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
\special{pa 3386 177}%
\special{pa 3386 413}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3411 374}%
\special{pa 3386 413}%
\special{pa 3361 374}%
\special{pa 3411 374}%
\special{fp}%
\special{pa 3386 610}%
\special{pa 3386 1161}%
\special{da 0.050}%
\special{sh 1.000}%
\special{pa 3411 1122}%
\special{pa 3386 1161}%
\special{pa 3361 1122}%
\special{pa 3411 1122}%
\special{fp}%
\special{pa 3330 548}%
\special{pa 3048 830}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3093 820}%
\special{pa 3048 830}%
\special{pa 3058 785}%
\special{pa 3093 820}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 3.780in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
\special{pa 3442 154}%
\special{pa 3724 436}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3714 391}%
\special{pa 3724 436}%
\special{pa 3678 426}%
\special{pa 3714 391}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 3.780in\lower\graphtemp\hbox to 0pt{\hss $bc$\hss}}%
\special{pa 3780 571}%
\special{pa 3780 807}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3805 768}%
\special{pa 3780 807}%
\special{pa 3755 768}%
\special{pa 3805 768}%
\special{fp}%
\special{pa 3439 204}%
\special{pa 3727 780}%
\special{da 0.050}%
\special{sh 1.000}%
\special{pa 3731 734}%
\special{pa 3727 780}%
\special{pa 3687 756}%
\special{pa 3731 734}%
\special{fp}%
\special{pa 3442 548}%
\special{pa 3724 830}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3714 785}%
\special{pa 3724 830}%
\special{pa 3678 820}%
\special{pa 3714 785}%
\special{fp}%
\special{pa 3724 942}%
\special{pa 3442 1224}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3487 1214}%
\special{pa 3442 1224}%
\special{pa 3452 1178}%
\special{pa 3487 1214}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.295in
\rlap{\kern 1.890in\lower\graphtemp\hbox to 0pt{\hss $\begin{array}{c@{~}c@{~}l@{~}l}E&=&\{a,b,c\}\!\!\!\!\!\!\!\\ c &\turn& \{a, b\}\\\emptyset &\turn& X& \mbox{for }X\neq\{a,b\}\end{array}$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 1.083in
\rlap{\kern 1.890in\lower\graphtemp\hbox to 0pt{\hss $(a\wedge b)\implies c$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 4.409in\lower\graphtemp\hbox to 0pt{\hss $a_1$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.689in
\rlap{\kern 4.409in\lower\graphtemp\hbox to 0pt{\hss $\#$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 4.606in\lower\graphtemp\hbox to 0pt{\hss $\#$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 4.409in\lower\graphtemp\hbox to 0pt{\hss $a_2$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 4.606in\lower\graphtemp\hbox to 0pt{\hss $\#$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.098in
\rlap{\kern 4.606in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
\special{pa 4571 169}%
\special{pa 4445 422}%
\special{fp}%
\special{sh 1.000}%
\special{pa 4485 398}%
\special{pa 4445 422}%
\special{pa 4440 375}%
\special{pa 4485 398}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.492in
\rlap{\kern 4.803in\lower\graphtemp\hbox to 0pt{\hss $b_1$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.689in
\rlap{\kern 4.803in\lower\graphtemp\hbox to 0pt{\hss $\#$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.886in
\rlap{\kern 4.803in\lower\graphtemp\hbox to 0pt{\hss $b_2$\hss}}%
\special{pa 4642 169}%
\special{pa 4750 386}%
\special{fp}%
\special{sh 1.000}%
\special{pa 4755 340}%
\special{pa 4750 386}%
\special{pa 4710 362}%
\special{pa 4755 340}%
\special{fp}%
\hbox{\vrule depth1.378in width0pt height 0pt}%
\kern 4.902in
}%
}%
\centerline{\raise 1em\box\graph}
\caption{A system with {\em resolvable conflict} represented as a Petri
net, an event structure as introduced here, a family of
configurations with transition relation, and a propositional theory.
The events $a$ and $b$ are initially in conflict (only one of them
may happen), but as soon as $c$ occurs this conflict is resolved.
The last picture is the best representation of the same system as an
event structure from \cite{NPW81}, again with arguable accuracy. It
yields a system with two maximal runs, in one of which $c$ causes
just $a$, and in the other just $b$.}
\label{fig-resolvable}
\vspace{-1em}
\end{figure}
\noindent
between event structures and Petri nets, making use of infinitary
propositional theories to translate between them. We show that our
new event structures enable us to represent any Petri net, thereby
establishing their {\em universality}.
\section{Configurations and Transitions}\label{sec-configurations}
We formalise the dynamic behaviour of an event structure by defining a
transition relation between sets of events. The idea here is that
when $X$ is the set of events that have happened so far, an additional set
$U$ of events can happen (concurrently) iff every subset of $X \cup U$
is enabled by a set of events that have happened before, i.e.\ a
subset of $X$.
\begin{definition}\rm\label{df-transitions-ES}
The {\em step transition relation} $\goto{}_\eE$ between sets
of events $X,Y \!\subseteq\! E$ of an event structure
$\eE=\tuple{E,\turn\;}$ is given by
$${X\goto{}_\eE Y \Leftrightarrow (X\subseteq Y \wedge
\forall Z \subseteq Y.~\exists W \subseteq X.~ W\turn Z)}.$$
For the {\em single action} transition relation we
also require that $|Y-X| \leq 1$.
\noindent
The set $L(\eE)$ of {\em (left-closed) configurations} of E is
$L(\eE)=\{ X \subseteq E \mid X \goto{}_\eE X \}.$
Two event structures $\eE$ and $\eF$ are {\em transition equivalent}
if they have the same events and $\goto{}_\eE = \goto{}_\eF$.
\end{definition}
Thus, $X \in L(\eE) \Leftrightarrow \forall Y\subseteq X.~ \exists Z
\subseteq X.~ Z \turn Y$ and if $X \goto{}_\eE Y$ then $X, Y \!\in\!
L(\eE)$. In Figs.~\ref{fig-prime},~\ref{fig-disjunctive}
and~\ref{fig-resolvable} we have indicated the single action
transition relation with solid arrows, and the rest of the step
transition relation with dashed ones.\linebreak[3]
Figure~\ref{fig-mutex} shows that the step transition relation can
provide important information about an event structure which is
included neither in its family of configurations nor in its single
action transition relation.
\begin{figure}[t]
%\input{mutex}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
\graphtemp=.5ex\advance\graphtemp by 0.089in
\rlap{\kern 0.000in\lower\graphtemp\hbox to 0pt{\hss P:\hss}}%
\special{pn 8}%
\special{ar 250 89 89 89 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.089in
\rlap{\kern 0.250in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 250 179}%
\special{pa 250 357}%
\special{fp}%
\special{sh 1.000}%
\special{pa 275 321}%
\special{pa 250 357}%
\special{pa 225 321}%
\special{pa 275 321}%
\special{fp}%
\special{pa 161 536}%
\special{pa 339 536}%
\special{pa 339 357}%
\special{pa 161 357}%
\special{pa 161 536}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.446in
\rlap{\kern 0.250in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
\special{pa 250 536}%
\special{pa 250 714}%
\special{fp}%
\special{sh 1.000}%
\special{pa 275 679}%
\special{pa 250 714}%
\special{pa 225 679}%
\special{pa 275 679}%
\special{fp}%
\special{ar 250 804 89 89 0 6.28319}%
\special{ar 607 89 89 89 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.089in
\rlap{\kern 0.607in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 607 179}%
\special{pa 607 357}%
\special{fp}%
\special{sh 1.000}%
\special{pa 632 321}%
\special{pa 607 357}%
\special{pa 582 321}%
\special{pa 632 321}%
\special{fp}%
\special{pa 518 536}%
\special{pa 696 536}%
\special{pa 696 357}%
\special{pa 518 357}%
\special{pa 518 536}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.446in
\rlap{\kern 0.607in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
\special{pa 607 536}%
\special{pa 607 714}%
\special{fp}%
\special{sh 1.000}%
\special{pa 632 679}%
\special{pa 607 714}%
\special{pa 582 679}%
\special{pa 632 679}%
\special{fp}%
\special{ar 607 804 89 89 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.089in
\rlap{\kern 2.714in\lower\graphtemp\hbox to 0pt{\hss M:\hss}}%
\special{ar 2964 89 89 89 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.089in
\rlap{\kern 2.964in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 2964 179}%
\special{pa 2964 357}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2989 321}%
\special{pa 2964 357}%
\special{pa 2939 321}%
\special{pa 2989 321}%
\special{fp}%
\special{pa 2875 536}%
\special{pa 3054 536}%
\special{pa 3054 357}%
\special{pa 2875 357}%
\special{pa 2875 536}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.446in
\rlap{\kern 2.964in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
\special{pa 2964 536}%
\special{pa 2964 714}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2989 679}%
\special{pa 2964 714}%
\special{pa 2939 679}%
\special{pa 2989 679}%
\special{fp}%
\special{ar 2964 804 89 89 0 6.28319}%
\special{ar 3321 446 89 89 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.446in
\rlap{\kern 3.321in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{ar 3143 468 143 143 -2.250941 -0.636548}%
\special{sh 1.000}%
\special{pa 3257 340}%
\special{pa 3258 383}%
\special{pa 3217 369}%
\special{pa 3257 340}%
\special{fp}%
\special{ar 3143 425 143 143 0.636548 2.250941}%
\special{sh 1.000}%
\special{pa 3066 578}%
\special{pa 3054 536}%
\special{pa 3097 539}%
\special{pa 3066 578}%
\special{fp}%
\special{ar 3679 89 89 89 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.089in
\rlap{\kern 3.679in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 3679 179}%
\special{pa 3679 357}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3704 321}%
\special{pa 3679 357}%
\special{pa 3654 321}%
\special{pa 3704 321}%
\special{fp}%
\special{pa 3589 536}%
\special{pa 3768 536}%
\special{pa 3768 357}%
\special{pa 3589 357}%
\special{pa 3589 536}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.446in
\rlap{\kern 3.679in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
\special{pa 3679 536}%
\special{pa 3679 714}%
\special{fp}%
\special{sh 1.000}%
\special{pa 3704 679}%
\special{pa 3679 714}%
\special{pa 3654 679}%
\special{pa 3704 679}%
\special{fp}%
\special{ar 3679 804 89 89 0 6.28319}%
\special{ar 3499 468 143 143 -2.505044 -0.890651}%
\special{sh 1.000}%
\special{pa 3426 369}%
\special{pa 3385 383}%
\special{pa 3386 340}%
\special{pa 3426 369}%
\special{fp}%
\special{ar 3499 425 143 143 0.890651 2.505044}%
\special{sh 1.000}%
\special{pa 3546 539}%
\special{pa 3589 536}%
\special{pa 3577 578}%
\special{pa 3546 539}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.446in
\rlap{\kern 1.321in\lower\graphtemp\hbox to 0pt{\hss $\begin{array}{ccl}E&=&\{a,b\}\\ \emptyset &\turn& \emptyset \\ \emptyset &\turn& \{a\} \\ \emptyset &\turn& \{b\} \\ \emptyset &\turn& \{a,b\}\end{array}$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.446in
\rlap{\kern 4.393in\lower\graphtemp\hbox to 0pt{\hss $\begin{array}{ccl}E&=&\{a,b\}\\ \emptyset &\turn& \emptyset \\ \emptyset &\turn& \{a\} \\ \emptyset &\turn& \{b\} \\ \{a\} &\turn& \{a,b\} \\ \{b\} &\turn& \{a,b\} \end{array}$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.089in
\rlap{\kern 2.179in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.446in
\rlap{\kern 1.821in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
\special{pa 2128 140}%
\special{pa 1872 396}%
\special{fp}%
\special{sh 1.000}%
\special{pa 1915 388}%
\special{pa 1872 396}%
\special{pa 1880 353}%
\special{pa 1915 388}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.804in
\rlap{\kern 2.179in\lower\graphtemp\hbox to 0pt{\hss $ab$\hss}}%
\special{pa 1872 497}%
\special{pa 2128 753}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2120 710}%
\special{pa 2128 753}%
\special{pa 2085 745}%
\special{pa 2120 710}%
\special{fp}%
\special{pa 2179 196}%
\special{pa 2179 696}%
\special{da 0.050}%
\special{sh 1.000}%
\special{pa 2204 661}%
\special{pa 2179 696}%
\special{pa 2154 661}%
\special{pa 2204 661}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.446in
\rlap{\kern 2.536in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
\special{pa 2229 140}%
\special{pa 2485 396}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2478 353}%
\special{pa 2485 396}%
\special{pa 2442 388}%
\special{pa 2478 353}%
\special{fp}%
\special{pa 2485 497}%
\special{pa 2229 753}%
\special{fp}%
\special{sh 1.000}%
\special{pa 2272 745}%
\special{pa 2229 753}%
\special{pa 2237 710}%
\special{pa 2272 745}%
\special{fp}%
\hbox{\vrule depth0.893in width0pt height 0pt}%
\kern 4.679in
}%
}%
\centerline{\raise 1em\box\graph}
\caption{Two systems P ({\em parallelism}) and M ({\em mutual
exclusion}) represented as a Petri net and an event structure.
The figure in the middle describes the configurations of P and M, as
well as the transition relation of P\@. The dashed transition is
lacking in Q\@. Even though P and M have the same configurations
and single action transition relations, their behaviour is
different, as witnessed by the transition $\emptyset \goto{}_\eP \{a,b\}$.}
\label{fig-mutex}\vspace{-.6em}
\end{figure}
\subsection{Purity}
We now introduce an important class of event structures whose step
transition relation is completely determined by their family of
configurations.
\begin{definition}\rm\label{df-pure-ES}
An event structure is {\em pure} if $X \turn Y$ only if $X \cap Y =
\emptyset$.\pagebreak[3]
\end{definition}
\begin{proposition}\label{pr-transitions-ES}
Let $\eE=\tuple{E,\turn\;}$ be a pure event structure, and $x,y\in L(\eE)$.
Then
\begin{center}
$x \goto{}_\eE y~$ iff $~x\subseteq y \wedge
\forall Z (x \subseteq Z \subseteq y \Rightarrow Z\in L(\eE))$.
\end{center}
\end{proposition}
\begin{proof}
``Only if'' follows immediately from the definitions.
For ``if'' let $x\subseteq y$ and $\forall Z (x \subseteq Z \subseteq y
\Rightarrow Z\in L(\eE))$. Let $Z\subseteq y$.
Then $x \subseteq x\cup Z \subseteq y$, so $x\cup Z\in L(\eE)$.
Hence, by \df{transitions-ES}, $\exists W \subseteq x\cup Z.~W\turn Z$.
As $\eE$ is pure, $W \cap Z = \emptyset$, hence $W \subseteq x$, which
had to be proved.
\qed\end{proof}
\begin{corollary}\label{cor-pure}
Two pure event structures $\eE$ and $\eF$ are transition equivalent
iff they have the same events and $L(\eE)=L(\eF)$.
\end{corollary}
\subsection{Reachability}
It can be argued that only the reachable configurations and the
reachable part of the step transition relation are semantically relevant.
\begin{definition}\rm\label{reachable}
A configuration $x$ of an event structure $\eE$ is {\em reachable}
if there is a sequence $\emptyset = x_0 \goto{}_\eE x_1 \goto{}_\eE \ldots
\goto{}_\eE x_n = x$.
Let $R(\eE)$ denote the set of reachable configurations of $\eE$.
Two event structures $\eE$ and $\eF$ are {\em reachable transition
equivalent} if they have the same events and $\goto{}_\eE \!\!\rest
R(\eE)= \goto{}_\eF \!\!\rest R(\eF)$.
\end{definition}
Clearly, transition equivalence is finer than reachable transition
equivalence. The following example shows that this is strictly so.
\begin{example}\label{ex-continuous}
Take as events of $\eE$ the set $\IQ$ of rational numbers and define
$\turn$ by $\emptyset \turn X$ for any $X$ with $|X|\neq 1$, and $X
\turn \{e\}$ iff $X=\{d \in \IQ \mid d2 \Rightarrow \emptyset \turn X$.
\end{itemize}
\end{definition}
Clearly, conjunctivity implies local conjunctivity, $\cal R$-irredundancy
implies $\fL$-irredundancy and cycle-freeness, and binary conflict
implies finite conflict.
\subsection{Correspondence through Left-closed Configurations}
For singular event structures, our notion of a left-closed
configuration can be simplified as follows:
\begin{observation}\label{obs-Wi87a}
Let $\eE$ be a singular event structure. Then
$$X \in L(\eE) \Leftrightarrow \Con(X) \wedge \forall e \in X.~\exists
Z \subseteq X.~ Z \turn \{e\}.$$
\end{observation}
When $d \leq e$, any configuration containing $e$ also contains $d$.
When $\eE=\tuple{E,\turn\;}$ is conjunctive, for any consistent event
$e \in E$ there is a smallest set $X \subseteq E$ with $X \turn \{e\}$.
Therefore, the part of the enabling relation consisting of enablings $X
\turn \{e\}$ is in essence completely determined by the causality relation
$\leq$.
\begin{observation}\label{obs-prime-Wi87a}
Let $\eE$ be a singular, conjunctive event structure. Then
$$X \in L(\eE) \Leftrightarrow
\Con(X) \wedge \forall d,e \in E.~ d \leq e \in X \Rightarrow d \in X.$$
\end{observation}
An event structure as in \cite{NPW81}, or a prime event structure as
in \cite{Wi87a,Wi89}, can be translated into our framework by defining
enablings $\{d \mid dn$).
\begin{observation}\label{obs-SinL}
Any event structure $\eE$ with finite conflict satisfies $S(\eE)
\!\subseteq\! L(\eE)$.
\end{observation}
For the event structures that result from mapping prime event
structures as in \cite{Wi87a,Wi89} into our framework we find, using the
principle of finite causes, that all left-closed configurations are secured.
It follows that both the secured and the left-closed configurations
can be understood as generalisations of the notion of configuration
for prime event structures from \cite{Wi87a,Wi89}.
\begin{proposition}\label{pr-secured}
Two singular event structures with finite conflict $\eE$ and $\eF$ are
reachable transition equivalent iff they have the same events and
$S(\eE)=S(\eF)$.
\end{proposition}
\begin{proof}
``only if'' follows immediately from \df{secured}.
``if'': Singular event structures are always reachably pure.
Using the proof of \pr{pure}, we can restrict attention to the case
that $\eE$ and $\eF$ are pure. For $\cal F$ one of $L$, $R$ or $S$
we define $\goto{}_{{\cal F}(\eE)}$ by
\begin{center}
$x \goto{}_{{\cal F}(\eE)} y~$ iff $~x\subseteq y \wedge
\forall Z (x \subseteq Z \subseteq y \Rightarrow Z\in {\cal F}(\eE))$.
\end{center}
By \df{secured} and \obs{SinL} we have
$R(\eE) \subseteq S(\eE) \subseteq L(\eE)$, hence
\begin{center}
$\goto{}_{\eE} \!\!\rest R(\eE) ~=~ \goto{}_{R(\eE)} ~\subseteq~
\goto{}_{S(\eE)} ~\subseteq~ \goto{}_{L(\eE)} ~=~ \goto{}_{\eE}.$
\end{center}
As the reachable part of both $\goto{}_{R(\eE)}$ and
$\goto{}_{L(\eE)}$ (defined the obvious way) is
$\goto{}_{\eE} \!\!\rest R(\eE)$, the reachable part of
$\goto{}_{S(\eE)}$ must also be $\goto{}_{\eE} \!\!\rest R(\eE)$, and
so the latter is fully determined by $S(\eE)$.
\end{proof}
Using the translation given at the end of \sect{introduction}, an
event structure as in \cite{Wi87a,Wi89} maps to an event structure in
our sense that is singular and with finite causes and finite conflict.
Hence the dynamic behaviour of such an event structure, as given by
the reachable part of its step transition relation, is fully
determined by its secured configurations.
\pagebreak[3]
The next proposition says that for such event structures the secured
configurations in turn are completely determined by the finite secured ones.
In addition, it provides a simplification of the notion of a secured
configuration.
\begin{proposition}\label{pr-Wi87a}
Let $\eE$ be a singular event structure with finite conflict and
finite causes. Then
$$X \in S(\eE) \Leftrightarrow \forall Y \subseteq_{\it fin} X.~
\exists Z \in S(\eE).~ Z \mbox{ is finite} \wedge Y \subseteq Z
\subseteq X,$$
i.e.\ the secured configurations are the {\em directed unions} over the
set of finite secured configurations. Moreover,\vspace{-1em}
$$X \in S(\eE) \Leftrightarrow \left\{\begin{array}{@{}l@{}}
\Con(X) \, \wedge\\
\forall e \in X.~ \exists e_0, \ldots, e_n \in X.~ e=e_n \,\wedge\\
\forall k\leq n.~\exists Y\subseteq\{e_0,...,e_{k-1}\}.~Y\turn \{e_k\}.
\end{array}\right.$$
\end{proposition}
The proof of this proposition will appear in \cite{GP04}.
It follows that our secured configurations
generalise the configurations of \mbox{\cite{Wi87a,Wi89}}.
Table~\ref{tab-subclasses} tells exactly how the various event structures of
\cite{NPW81,Wi87a,Wi89} can be regarded as subclasses of our event structures.
Again, the proofs of the claims therein will be provided in \cite{GP04}.
\begin{table}[t]
\caption{This table indicates in which way the event structures from
\cite{NPW81,Wi87a,Wi89} correspond with subclasses of our event
structures. In all 7 cases we have that any event structure from
\cite{NPW81,Wi87a,Wi89} translates into one
of ours with the listed properties, that has the same events and
configurations; and vice versa, that for each of our event
structures with the required properties an event structure from
\cite{NPW81,Wi87a,Wi89} can be found that has the same events and
configurations. As indicated, we use the left-closed configurations
for the event structures from \cite{NPW81}, and the secured
configurations for the ones from \cite{Wi87a,Wi89}. For the prime
event structures from \mbox{\cite{Wi87a,Wi89}} the two notions of
configuration coincide.}
\begin{center}
\begin{tabular}{@{}|@{~}lr@{~}|@{~}l@{~}|@{~}r@{~}|@{}}
\hline
ev.\ str.\ &\cite{Wi87a} & rooted, singular, finite causes \& finite conflict& $S$\\
stable &\cite{Wi87a} & same \& locally conjunctive& $S$\\
prime &\cite{Wi87a} & same \& conjunctive \& $\cal R$-irredundant& $S,L$\\
ev.\ str.\ &\cite{Wi89} & rooted, singular, finite causes \& binary conflict& $S$\\
stable &\cite{Wi89} & same \& locally conjunctive& $S$\\
prime &\cite{Wi89} & same \& conjunctive \& $\cal R$-irredundant& $S,L$\\
ev.\ str.\ &\cite{NPW81}& rooted, singular, binary conflict, conjunctive, $\fL$-irr. \& cycle-free& $L$\\
\hline
\end{tabular}
\end{center}
\label{tab-subclasses}
\vspace{-1em}
\end{table}
\section{Petri Nets and Propositional Theories}\label{sec-nets}
In this section we describe how any Petri net can be represented, in a
behaviour preserving way, by a rooted event structure with finite
conflict, and vice versa.
We also show how to represent an event structure as a propositional theory.
\subsection{From Nets to Event Structures}
\begin{definition}\rm\label{petri}
A {\em Petri net} is a tuple $\eN = \tuple{S,T,F,I}$ with\vspace{-1ex}
\begin{itemize}
\item $S$ and $T$ two disjoint sets of {\em places} ({\em Stellen} in German)
and {\em transitions},
\item $F \subseteq S \times T \cup T\times S$, the {\em flow relation},
\item and $I:S \rightarrow \IN$, the {\em initial marking}.
\pagebreak[3]
\end{itemize}
\end{definition}
% Petri nets are pictured by drawing the places as circles, the
% transitions as boxes, and the elements of $F$ as arrows between places
% and transitions.
%
In \cite{GP95} we described how any Petri net can be transformed, in a
behaviour preserving way, into a {\em 1-occurrence net}, this being a
Petri net with the property that in any run each transition can fire
at most once. The transformation replaces any transition by countably
many copies, each of which is connected to the places of the net
(through the flow relation) in the same way as the original
transition. Each of the obtained transitions gets a private preplace,
initially marked with 1 token. This ensures that whenever a transition
could fire in the original net, one of its copies can fire in the
transformed net---but each of the new transitions can fire only once.
A formal account of the way in which this transformation is behaviour
preserving would require the use of labelled Petri nets.
We now show how any 1-occurrence net can be represented as an event
structure. Let $\eN=\tuple{S,E,F,I}$ be a 1-occurrence net. For any
place $s \in S$ let $s^\bullet = \{t \!\in\! E \mid (s,t)\!\in\!F\}$ be its
set of {\em posttransitions} and $^\bullet\! s = \{t \!\in\! E \mid
(t,e)\!\in\!F\}$ its set of {\em pretransitions}. For any finite set $Y
\subseteq s^\bullet$ of posttransitions of $s$, $|Y|$ is the number of
tokens needed in place $s$ for all transitions in $Y$ to fire, so
$|Y|\monus I(s)$ is the number of tokens that have to arrive in place
$s$ before all transitions in $Y$ can fire.
% Here $x\monus y ~\defeq~\left\{
% \begin{array}{@{}ll@{}}x-y&\mbox{if }x>y\\0&\mbox{otherwise}.
% \end{array}\right.$
Furthermore, let $^n\!s = \{X \!\subseteq
\mbox{$^\bullet\!s$} \mid |X| = n\}$ be the collection of sets $X$
of pretransitions of $s$, such that if all transitions in $X$ fire,
$n \!\in\! \IN$ tokens will arrive in $s$.\linebreak[3]
Write $^Y\!\!s$ for \plat{^{|Y|\!\!\monus\!\!I(s)}\!s}. One of the sets of
transitions in $^Y\!\!s$ has to fire entirely before all transitions
in $Y$ can fire.
For any finite set of transitions $Y \subseteq E$, let $S_Y$ be the
set of places $s$ with $Y \subseteq s^\bullet$ and $|Y|-I(s)>0$. Now
write $X \turn_\eN Y$ whenever $X = \bigcup_{s \in S_Y} X_s$ with
$X_s\!\in \mbox{$^Y\!\!s$}$. We also write $\emptyset \turn_\eN Y$
whenever $Y$ is infinite. The {\em event structure associated to}
$\eN$ is defined as $\fE(\eN)=\tuple{E,\turn_\eN\;}$.
Note that $\fE(\eN)$ is rooted and with finite conflict. It can be
shown that this event structure has the same {\em step transition
relation} as $\eN$, at least when restricting to steps of
finitely many events, although we didn't have space to formalise the
latter notion for Petri nets here.
It is not hard to extend the above construction to nets with
{\em arcweights} \cite{GP04}.
\subsection{From Event Structures to Propositional Theories}
With any event structure $\eE=\tuple{E,\turn\;}$ we associate the
(infinitary) propositional theory
$$T(\eE) = \textstyle\{ \bigwedge X \Rightarrow \bigvee \{\bigwedge Y \mid Y
\turn X \} \mid X \subseteq E \}.$$
In this context, an event is regarded as the proposition that it has
happened. The propositional formulae generated above give necessary
and sufficient conditions for a set of events to be a left-closed
configuration; it is not hard to see that $L(\eE)$ is exactly the set
of models of $T(\eE)$ in the sense of propositional logic.
A propositional theory provides a pleasant alternative representation of
an event structure; examples of this can be found in the figures of
\sect{introduction}.
For any two subsets $X$,$Y$ of $E$, let the {\em clause} $X
\Rightarrow Y$ abbreviate the implication $\bigwedge X \implies
\bigvee Y$. A theory consisting of a set of clauses is said to be in
{\em conjunctive normal form}. Using the distributivity of $\bigvee$
over $\bigwedge$, and that $\varphi \Rightarrow \bigwedge_{i\in I}
\psi_i$ is equivalent to $\bigwedge_{i\in I}(\varphi \Rightarrow
\psi_i)$, the theory $T(\eE)$ can be turned into the conjunctive
normal form $T_{\rm CNF}(\eE)$. We say that a propositional theory in
conjunctive normal form is {\em rooted} if it has no clauses of the
form $\emptyset\Rightarrow X$, and that it has {\em finite conflict}
if there are no clauses $X\Rightarrow Y$ with $X$ infinite. Clearly,
if $\eE$ is a rooted and with finite conflict, then so is $T_{\rm
CNF}(\eE)$.
\subsection{From Propositional Theories to Petri nets}
Let $\eT=\tuple{E,T}$ be a propositional theory in conjunctive normal
form that is rooted and with finite conflict. As in \cite{GP95}, we
define the associated Petri net $\fN(\eT)$ as follows. As transitions
of the net we take the events from $E$. For every transition we add
one place, containing one initial token, that has no incoming arcs,
and with its only outgoing arc going to that transition. These {\em
1-occurrence places} make sure that every transition fires at most
once. For every clause $X \Rightarrow Y$ in $T$, we introduce a place
in the net. This place has outgoing arcs to each of the transitions in
$X$, and incoming arcs from each of the places in $Y$. Let $n$ be the
cardinality of $X$. As $\eT$ is rooted and with finite conflict, $n
\neq 0$ and $n$ is finite. We finish the
construction by putting $n-1$ initial tokens in the created place:
\vspace{-.7ex}
%\input{../conf/clause}
\expandafter\ifx\csname graph\endcsname\relax \csname newbox\endcsname\graph\fi
\expandafter\ifx\csname graphtemp\endcsname\relax \csname newdimen\endcsname\graphtemp\fi
\setbox\graph=\vtop{\vskip 0pt\hbox{%
\special{pn 8}%
\special{ar 866 610 98 98 0 6.28319}%
\graphtemp=.5ex\advance\graphtemp by 0.583in
\rlap{\kern 0.831in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.583in
\rlap{\kern 0.902in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\graphtemp=.5ex\advance\graphtemp by 0.650in
\rlap{\kern 0.866in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
\special{pa 0 157}%
\special{pa 157 157}%
\special{pa 157 0}%
\special{pa 0 0}%
\special{pa 0 157}%
\special{fp}%
\special{ar 293 654 591 591 -1.802089 -0.242404}%
\special{sh 1.000}%
\special{pa 202 94}%
\special{pa 157 79}%
\special{pa 190 45}%
\special{pa 202 94}%
\special{fp}%
\special{pa 0 433}%
\special{pa 157 433}%
\special{pa 157 276}%
\special{pa 0 276}%
\special{pa 0 433}%
\special{fp}%
\special{ar 295 1130 787 787 -1.746343 -0.862746}%
\special{sh 1.000}%
\special{pa 201 372}%
\special{pa 157 354}%
\special{pa 192 323}%
\special{pa 201 372}%
\special{fp}%
\special{pa 0 709}%
\special{pa 157 709}%
\special{pa 157 551}%
\special{pa 0 551}%
\special{pa 0 709}%
\special{fp}%
\special{ar 472 1273 787 787 -1.982313 -1.159279}%
\special{sh 1.000}%
\special{pa 204 558}%
\special{pa 157 551}%
\special{pa 184 513}%
\special{pa 204 558}%
\special{fp}%
\special{pa 0 984}%
\special{pa 157 984}%
\special{pa 157 827}%
\special{pa 0 827}%
\special{pa 0 984}%
\special{fp}%
\special{ar 703 1395 787 787 -2.335515 -1.488036}%
\special{sh 1.000}%
\special{pa 203 818}%
\special{pa 157 827}%
\special{pa 169 781}%
\special{pa 203 818}%
\special{fp}%
\special{pa 1575 157}%
\special{pa 1732 157}%
\special{pa 1732 0}%
\special{pa 1575 0}%
\special{pa 1575 157}%
\special{fp}%
\special{pa 936 541}%
\special{pa 1280 138}%
\special{pa 1575 79}%
\special{sp}%
\special{sh 1.000}%
\special{pa 980 527}%
\special{pa 936 541}%
\special{pa 942 494}%
\special{pa 980 527}%
\special{fp}%
\special{pa 1575 433}%
\special{pa 1732 433}%
\special{pa 1732 276}%
\special{pa 1575 276}%
\special{pa 1575 433}%
\special{fp}%
\special{ar 1069 -169 787 787 0.872902 1.703581}%
\special{sh 1.000}%
\special{pa 1000 640}%
\special{pa 965 610}%
\special{pa 1007 591}%
\special{pa 1000 640}%
\special{fp}%
\special{pa 1654 433}%
\special{pa 1654 827}%
\special{dt 0.079}%
\special{pa 1575 984}%
\special{pa 1732 984}%
\special{pa 1732 827}%
\special{pa 1575 827}%
\special{pa 1575 984}%
\special{fp}%
\special{ar 1492 122 787 787 1.465367 2.355163}%
\special{sh 1.000}%
\special{pa 946 725}%
\special{pa 936 680}%
\special{pa 981 690}%
\special{pa 946 725}%
\special{fp}%
\graphtemp=.5ex\advance\graphtemp by 0.827in
\rlap{\kern 0.728in\lower\graphtemp\hbox to 0pt{\hss $X \implies Y$\hss}}%
\hbox{\vrule depth0.984in width0pt height 0pt}%
\kern 1.732in
}%
}%
$$X \left\{\raisebox{1.3cm}[1.5cm][0pt]{\raise .5 mm \box\graph}\right\}Y\vspace{-.7ex}$$
The place belonging to the clause $X \Rightarrow Y$ does not place any
restrictions on the firing of the first \mbox{$n-1$} transitions in $X$.
However, the last one can only fire after an extra token arrives in
the place.
This can happen only if one of the transitions in $Y$ fires first.
The firing of more transitions in $Y$ has no adverse
effects, as each of the transitions in $X$ can fire only once.
Thus this place imposes the same restriction on the occurrence of
events as the corresponding clause.
It should be intuitively clear that the dynamic behaviour of
$\fN(T_{\rm CNF}(\eE))$ strongly resembles that of $\eE$, although
it should be admitted that in the standard semantics of Petri nets
only finitely many transitions may fire in one step, whereas
\df{transitions-ES} allows infinite steps. Nevertheless, we have
\begin{theorem}\label{main}
Let $\eE$ be a rooted event structure with finite conflict. Then\linebreak
$\fE(\fN(T_{\rm CNF}(\eE)))$ is transition equivalent to $\eE$.
\end{theorem}
\begin{trivlist}\item[\hspace{\labelsep}{\it Proof sketch.}]
It is straightforward to find mappings $\cal T$ from nets to
propositional theories \cite{GP04} and $\fE'$ from propositional
theories of the form ${\cal T}(\eN)$ with $\eN$ a net to event
structures, such that $\fE(\eN) = \fE'({\cal T}(\eN))$ for all
Petri nets, ${\cal T}(\fN(\eT))=\eT$ for all propositional theories
$\eT$ in conjunctive normal form, and $\fE'(T_{\rm CNF}(\eE)) \equiv
\eE$ for all event structures $\eE$, where $\equiv$ denotes transition
equivalence.
\end{trivlist}
In general this theorem depends intrinsically on the specific form of
$T_{\rm CNF}(\eE)$; however, for pure event structures any conjunctive
normal form of $T(\eE)$ (up to {\em logical equivalence}, i.e.\ having the
same models) will do, as shown in \cite{GP04}.
Also note that the construction $\fN \circ T_{\rm CNF} \circ \fE$ converts
any 1-occurrence net into an equivalent net without arcweights.
\subsection{Comparing Models}\label{EvsC}
\begin{table}[t]
\caption{Corresponding properties\label{correspondence}}
\begin{center}
\begin{tabular}{@{}|@{~}l@{~}|@{~}l@{~}|@{~}l@{~}|@{}}
\hline
Event structures & Propositional theories and nets & Petri nets \\
\hline\hline
rooted & ($>\!0$, any) & (any, any) \\
singular & (1, any), (any, 0)& ($\leq\!1$, any), (any, 0) \\
manifestly conjunctive & (any, $\leq\!1$) & (any, $\leq\!1$) \\
finite conflict & (finite, any) & (any, any) \\
binary conflict & ($\leq\!2$, any) & ($\leq\!2$, any) \\
\hline
\end{tabular}
\end{center}
\vspace{-1em}
\end{table}
It is interesting to see how three important properties of event
structures correspond with structural properties of Petri nets.
Call an event structure {\em manifestly conjunctive} if for every set
of events $Y$ there is at most one set $X$ with $X \turn Y$.
Every conjunctive event structure can be made manifestly conjunctive
by deleting, for every set $Y$, all but the smallest $X$ for which $X
\turn Y$. The property of conjunctivity implies that such a smallest
$X$ exists. This normalisation preserves transition equivalence, and
all properties of \df{event-properties}.
When $\eE$ is an event structure satisfying any of the properties from
the left column of Table~\ref{correspondence}, then $T_{\rm CNF}(\eE)$
satisfies the corresponding properties from the middle column. These
are to be read as cardinality restrictions on the sets $X$ and $Y$,
respectively, in each of its clauses $X \Rightarrow Y$. For instance,
if $\eE$ is singular, $T_{\rm CNF}(\eE)$ has only clauses $X
\Rightarrow Y$ with $|X|= 1$ or $|Y|=0$. Furthermore, if $T$ is a
rooted propositional theory with finite conflict satisfying any of the
properties of the middle column, then $\fN(T)$ satisfies these same
properties, but now they are cardinality restrictions on the number of
outgoing and incoming arcs, respectively, for every place in $\fN(T)$.
Finally, any net satisfying some of the restrictions from the middle
column, or even the weaker variants from the right column, translates
to an event structure satisfying the corresponding restrictions on the
left. This remains true if any place with $n$ incoming arcs and $k$
initial tokens is deemed to satisfy the restriction
``($\leq\! k\!+\!n$, $\leq\!n$) or ($k\!+\!n\!+\!1$, 0)''.
\section{Related Work}
A {\em bundle event structure}, as studied in {\sc Langerak}
\cite{Lk92}, can in our framework best be understood as a
propositional theory. Using the translation of \sect{nets} it maps to
a special kind of stable event structure \cite{Wi89}. Langerak's
notion of an {\em extended} bundle event structure on the other hand
does not correspond to an event structure as in \cite{Wi87a,Wi89}.
Here the symmetric binary conflict relation $\#$ is replaced by an
asymmetric counterpart $\asym$. When $a \asym b$, the event $b$ can
happen regardless of $a$, and $a$ is initially enabled as well;
however, as soon as $b$ happens, $a$ is blocked. Asymmetric conflict
$a \asym b$ can be translated into our framework as $\{b\} \turn
\{a,b\}$. (As this translation introduces impurity, for its
correctness it is necessary to consider the transition relation of
\df{transitions-ES}.) Thus, extended bundle event structures are
subsumed by our event structures too.
The same can be said for the {\em extended dual event structures} of
{\sc Katoen} \cite{Ka96}.
Here the crucial feature is the symmetric
and irreflexive {\em interleaving relation}, modelling mutual
exclusion of events, i.e.\ disallowing them to overlap in time. As in
\fig{mutex}, this can be modelled in our framework as
$~~~\{a\} \turn \{a,b\}~~~\{b\} \turn \{a,b\}.$\\
Using similar techniques, we believe it is also possible to embed the
causal automata of {\sc Gunawardena} \cite{Gun92b} in our framework.
{\sc Boudol} \cite{Bo90} provides translations between a class of
1-occurrence nets, the {\em flow nets}, and a class of {\em flow event
structures} that fall in expressive power between the prime and the
stable event structures of \cite{Wi89}. His correspondence extends the
correspondence between safe occurrence nets and prime event structures
due to \cite{NPW81}. As Boudol's translations preserve the notions of
event (=transition) and configuration, they are consistent with our
approach. Our translations can be regarded as an extension of the work
of \cite{Bo90} to general Petri nets.
Another translation between Petri nets and a new model of event
structures has been provided in {\sc Hoogers, Kleijn \& Thiagarajan}
\cite{HKT96}, albeit for systems without autoconcurrency only. Their
event structures are essentially families of configurations with a
step transition relation between them. The translations of
\cite{HKT96} are quite different from ours: even on 1-occurrence nets
an individual transition may correspond to multiple events. We
conjecture the two approaches are equivalent under a suitable notion
of history preserving bisimulation.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thebibliography}{10}
\small
\bibitem{Bo90}
{\sc G.~Boudol} (1990):
\newblock {\em Flow event structures and flow nets.}
\newblock In I.~Guessarian, editor: {\sl Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science, {\rm La Roche Posay, France}}, {\sl \rm LNCS} 469, %Springer
pp. 62--95.
\bibitem{GP95}
{\sc R.J.~van Glabbeek \& G.D. Plotkin} (1995):
\newblock {\em Configuration structures (extended abstract).}
\newblock In D.~Kozen, editor: Proc. LICS'95, San Diego, USA, pp. 199--209.
\bibitem{GP04}
{\sc R.J.~van Glabbeek \& G.D.~Plotkin} (2004):
\newblock {\em Configuration structures, event structures and {Petri} nets.}
Draft at {\tt http://theory.stanford.edu/\~{}rvg/event/}.
\bibitem{Gun92b}
{\sc J.~Gunawardena} (1992):
\newblock {\em Causal automata.}
\newblock {TCS} 101, pp. 265--288.
\bibitem{HKT96}
{\sc P.W. Hoogers, H.C.M. Kleijn \& P.S. Thiagarajan} (1996):
\newblock {\em An event structures semantics for general {Petri} nets.}
\newblock {TCS} 153, pp. 129--170.
\bibitem{Ka96}
{\sc J.-P. Katoen} (1996):
{\it Quantitative and Qualitative Extensions of Event Structures},
\newblock PhD thesis, Department of Computer Science, University of Twente.
\bibitem{Lk92}
{\sc R.~Langerak} (1992):
\newblock {\em Transformations and Semantics for LOTOS}.
\newblock PhD thesis, Department of Computer Science, University of Twente.
\bibitem{NPW81}
{\sc M.~Nielsen, G.D. Plotkin \& G.~Winskel} (1981):
\newblock {\em Petri nets, event structures and domains, part {I}.}
\newblock {TCS} 13(1), pp. 85--108.
\bibitem{Wi87a}
{\sc G.~Winskel} (1987):
\newblock {\em Event structures.}
\newblock In W.~Brauer, W.~Reisig \& G.~Rozenberg, editors: {\sl Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, {\rm Bad Honnef, September 1986}}, {\sl \rm LNCS} 255, Springer, pp. 325--392.
\bibitem{Wi89}
{\sc G.~Winskel} (1989):
\newblock {\em An introduction to event structures.}
\newblock In J.W. de~Bakker, W.P.~de Roever \& G.~Rozenberg, editors: {\sl REX School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, {\rm Noordwijkerhout, The Netherlands, May/June 1988}}, {\sl \rm LNCS} 354, Springer, pp. 364--397.
\end{thebibliography}
\end{document}