\documentstyle[twocolumn]{article}
\newcommand{\ams}[1]{#1}      % delete "#1" if you miss fonts smbm10 or eusm10
\newcommand{\Afour}[1]{}      % add "#1" for formating on A4 paper
\setlength{\textwidth}{6.875in}
\setlength{\columnsep}{0.375in}
\setlength{\oddsidemargin}{-.1875in}
\setlength{\textheight}{8.875in}
\setlength{\topmargin}{0in}
\setlength{\headheight}{0in}
\setlength{\headsep}{0in}
\setlength{\parindent}{12pt}
\makeatletter
\def\section{\@startsection {section}{1}{0pt}{-3.25ex plus -1ex minus 
   -.2ex}{1.5ex plus .2ex}{\large\bf}}
\def\subsection{\@startsection {subsection}{2}{0pt}{-2ex plus -1ex minus 
   -.2ex}{1.5ex plus .2ex minus .3ex}{\xipt\bf}}
\def\paragraph{\@startsection
   {paragraph}{4}{\z@}{2ex plus 1ex minus .2ex}{-1em}{\normalsize\bf}}
\long\def\@makecaption#1#2{
   \vskip 10pt 
   \setbox\@tempboxa\hbox{\sf #1: #2}
   \ifdim \wd\@tempboxa >\hsize   % IF longer than one line:
       \sf #1: #2\par             %   THEN set as ordinary paragraph.
     \else                        %   ELSE  center.
       \hbox to\hsize{\hfil\box\@tempboxa\hfil}  
   \fi}
\makeatother
\unitlength             .8 mm   % This is used in pictures
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%		On A4 paper the right margin is 6 mm smaller,		  %%%%
%%%%		whereas the bottom margin is 17.6 mm longer.		  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\Afour{
\newlength{\shiftside}			 \newlength{\shifttop}
\setlength{\shiftside}{-3mm}		 \setlength{\shifttop}{8.8mm}
\addtolength\oddsidemargin{\shiftside}
\addtolength\evensidemargin{\shiftside}
\addtolength\topmargin{\shifttop}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%                    Theorem-like environments                         %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{defi}{Definition}
\newtheorem{theo}{Theorem}
\newtheorem{prop}{Proposition}
\newtheorem{lemm}{Lemma}
\newtheorem{coro}{Corollary}
\newtheorem{exam}{Example}

\newenvironment{definition}[1]{\begin{defi} \rm \label{df-#1} }{\end{defi}}
\newenvironment{theorem}[1]{\begin{theo} \rm \label{th-#1} }{\end{theo}}
\newenvironment{proposition}[1]{\begin{prop} \rm \label{pr-#1} }{\end{prop}}
\newenvironment{lemma}[1]{\begin{lemm} \rm \label{lem-#1} }{\end{lemm}}
\newenvironment{corollary}[1]{\begin{coro} \rm \label{cor-#1} }{\end{coro}}
\newenvironment{example}[1]{\begin{exam} \rm \label{ex-#1} }{\end{exam}}
\newenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}{\hfill $\Box$\end{trivlist}}

\newcommand{\df}[1]{Definition~\ref{df-#1}}
\newcommand{\th}[1]{Theorem~\ref{th-#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}}

\newenvironment{itemise}{\begin{list}{$\bullet$}{\leftmargin 18pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 4pt \itemsep 2pt \parsep 2pt}}{\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%                            New Commands                              %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\bbigcup}{\overline{\bigcup}}
\newcommand{\bbigcap}{\overline{\bigcap}}
\newcommand{\nbbigcup}{\bbigcup_{\bullet}}
\newcommand{\nbbigcap}{\bbigcap_{\bullet}}
\newcommand{\dbigcup}{\bigcup_{\uparrow}}
\newcommand{\nbigcup}{\bigcup_{\bullet}}
\newcommand{\nbigcap}{\bigcap_{\bullet}}
\newcommand{\bigdvee}{$~\makebox[0pt]{\Huge$\cdot$}\makebox[0pt]{$\bigvee$}~$}
\newcommand{\dcup}{\stackrel{\cdot}{\cup}}              % disjoint union
\newcommand{\dl}[1]{\mbox{\rm I\hspace{-0.75mm}#1}}     % openface letter
\newcommand{\dc}[1]{\mbox{\rm {\raisebox{.4ex}{\makebox % openface character
        [0pt][l]{\hspace{.2em}\scriptsize $\mid$}}}#1}}
\newcommand{\IZ}{\mbox{\bf Z}}                          % boldface Z (integers)
\newcommand{\pow}{{\cal P}}                             % caligrf. P (powerset)
\ams{\newfont{\open}{msbm10}                            % openface letters
\renewcommand{\IZ}{\mbox{\open Z}}                      % openface Z (integers)
\newfont{\fsc}{eusm10}                                  % frenchscript letters
\renewcommand{\pow}{\mbox{\fsc P}}}                     % french P (powerset)
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}   % no vertical space
\newcommand{\Id}[1]{[\hspace{-1.4pt}[#1]\hspace{-1.2pt}]} % denotation
\newcommand{\goto}[1]{\stackrel{#1}{\longrightarrow}}   % transition
\newcommand{\gonotto}[1]{\hspace{4pt}\not\hspace{-4pt}  % no transition
        \stackrel{#1\ }{\longrightarrow}}
\newcommand{\trans}{\mbox{$\longrightarrow
        \hspace{-.8em}\rightarrow$}}                    % transitive transition
\newcommand{\bis}[1]{ \;                                % bisimulation
        \raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,}
\newcommand{\nobis}[1]{\mbox{$\,\not\hspace{-2.5pt}     % no bisimulation
        \raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
                  \,_{#1}\,$}}
\newcommand{\pf}{{\bf Proof:\ }}                        % beginning of proof
\newcommand{\rest}{                                     % restriction operator
	\unitlength 1   mm 
        \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} }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%Tex macro package by Vaughan Pratt for drawing character-sized objects%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcount\PLv\newcount\PLw\newcount\PLx\newcount\PLy\newdimen\PLyy\newdimen\PLX
\newbox\PLdot \setbox\PLdot\hbox{\tiny.} \def\scl{.08} % resettable scale
\def\PLot#1{\PLx`#1\advance\PLx-42\PLy\PLx\PLv\PLx\divide\PLy9\PLw\PLy\multiply
\PLw9\advance\PLx-\PLw\advance\PLx-4\PLy-\PLy\advance\PLy4\PLX=\the\PLx pt
\advance\PLyy\the\PLy pt\wd\PLdot=\scl\PLX\raise\scl\PLyy\copy\PLdot}
\def\draw#1{\ifx#1\end\let\next=\relax\else\PLot#1\let\next=\draw\fi\next}
%%%%%%%%%%%%%%%%%%%%%%%%%Polish a by Rob van Glabbeek%%%%%%%%%%%%%%%%%%%%%%%%%
\def\pa{\mbox{a\hspace{-2pt}\raisebox{-.7pt}%     \pa   Polish a
        {\draw Wabcdefgh_VVM\end}\hspace{1pt}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%                            Abbreviations                             %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\dl{N}}                            % natural numbers
\newcommand{\IC}{\dc{C}}                            % configuration structures
\newcommand{\IE}{\dl{E}}                            % event structures
\newcommand{\IG}{\dc{G}}                            % graphs
\newcommand{\fC}{{\cal C}}                          % function into \IC
\newcommand{\fE}{{\cal E}}                          % function into \IE
\newcommand{\fF}{{\cal F}}                          % family f configurations
\newcommand{\fG}{{\cal G}}                          % function into \IG
\newcommand{\fS}{{\cal S}}                          % secured configurations
\newcommand{\fR}{{\cal R}}                          % reachable configurations
\newcommand{\fL}{{\cal L}}                          % left-closed conf.
\newcommand{\eC}{{\rm C}}                           % conf. structure
\newcommand{\eD}{{\rm D}}                           % conf. structure
\newcommand{\eE}{{\rm E}}                           % event structure
\newcommand{\eF}{{\rm F}}                           % event structure
\newcommand{\eG}{{\rm G}}                           % process graph
\newcommand{\eH}{{\rm H}}                           % process graph
\newcommand{\turn}{\vdash}                          % turnstile

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%                               Titel                                  %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\bibliographystyle{plain}

\title{\Large\bf Configuration Structures\\
       \small\bf (extended abstract)}
\author{R.J. van Glabbeek\thanks{This work was supported by ONR under
                        grant number N00014-92-J-1974.}\\
 \normalsize Computer Science Department\\[-3pt]
 \normalsize Stanford University\\[-3pt]
 \normalsize Stanford, CA 94305, USA\\[-3pt]
 \normalsize \tt rvg@cs.stanford.edu
\and    G.D. Plotkin\makebox[0pt][l]{$^*$}\\
 \normalsize Department of Computer Science\\[-3pt]
 \normalsize University of Edinburgh\\[-3pt]
 \normalsize Edinburgh EH9 3JZ, UK\\[-3pt]
 \normalsize \tt gdp@dcs.ed.ac.uk}
\date{}
\maketitle
%\thispagestyle{empty}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection*{\centering Abstract}
{\em Configuration structures provide a model of concurrency
generalising the families of configurations of event structures. They
can be considered logically, as classes of propositional models; then
sub-classes can be axiomatised by formulae of simple prescribed forms.
Several equivalence relations for event structures
are generalised to configuration structures, and also to general Petri nets.
Every configuration structure is shown to be ST-bisimulation
equivalent to a prime event structure with binary conflict;
this fails for the tighter history preserving bisimulation.
Finally, Petri nets without self-loops under the collective token
interpretation are shown behaviourally equivalent to configuration
structures, in the sense that there are translations in both
directions respecting history preserving bisimulation. This fails for
nets with self-loops.}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}

The aim of this paper is to connect several models of concurrency, by
providing translations between them and studying which notions of
behavioural equivalence these translations preserve.


In {\sc Nielsen, Plotkin \& Winskel} \cite{NPW81} {\em event
structures} were introduced as a stepping stone between {\em Petri
nets} and {\em Scott domains}. It was established that every {\em
safe} Petri net can be unfolded into an {\em occurrence net}; the
occurrence nets are then in correspondence with
\begin{figure}[thb]\vspace{-2ex}
%\input{families}
\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{pa 125 1100}%
    \special{pa 875 1100}%
    \special{pa 875 600}%
    \special{pa 125 600}%
    \special{pa 125 1100}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.850in
    \rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss Occurrence\hss}}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.850in
    \rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss nets\hss}}%
    \special{pa 1125 1100}%
    \special{pa 1925 1100}%
    \special{pa 1925 600}%
    \special{pa 1125 600}%
    \special{pa 1125 1100}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -2\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.850in
    \rlap{\kern 1.525in\lower\graphtemp\hbox to 0pt{\hss Prime event\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.850in
    \rlap{\kern 1.525in\lower\graphtemp\hbox to 0pt{\hss structures\hss}}%
    \graphtemp=\baselineskip\multiply\graphtemp by 2\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.850in
    \rlap{\kern 1.525in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize w.\ bin.\ conflict}\hss}}%
    \special{pa 2125 1100}%
    \special{pa 3225 1100}%
    \special{pa 3225 600}%
    \special{pa 2125 600}%
    \special{pa 2125 1100}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.850in
    \rlap{\kern 2.675in\lower\graphtemp\hbox to 0pt{\hss Prime algebraic\hss}}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.850in
    \rlap{\kern 2.675in\lower\graphtemp\hbox to 0pt{\hss coherent domains\hss}}%
    \special{pa 1575 400}%
    \special{pa 2475 400}%
    \special{pa 2475 0}%
    \special{pa 1575 0}%
    \special{pa 1575 400}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.200in
    \rlap{\kern 2.025in\lower\graphtemp\hbox to 0pt{\hss Families of\hss}}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.200in
    \rlap{\kern 2.025in\lower\graphtemp\hbox to 0pt{\hss configurations\hss}}%
    \special{pa 875 700}%
    \special{pa 1125 700}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1055 675}%
    \special{pa 1125 700}%
    \special{pa 1055 725}%
    \special{pa 1055 675}%
    \special{fp}%
    \special{pa 1125 1000}%
    \special{pa 875 1000}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 945 1025}%
    \special{pa 875 1000}%
    \special{pa 945 975}%
    \special{pa 945 1025}%
    \special{fp}%
    \special{pa 1825 600}%
    \special{pa 1825 400}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1800 470}%
    \special{pa 1825 400}%
    \special{pa 1850 470}%
    \special{pa 1800 470}%
    \special{fp}%
    \special{pa 2225 400}%
    \special{pa 2225 600}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2250 530}%
    \special{pa 2225 600}%
    \special{pa 2200 530}%
    \special{pa 2250 530}%
    \special{fp}%
    \special{pa 2125 1000}%
    \special{pa 1925 1000}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1995 1025}%
    \special{pa 1925 1000}%
    \special{pa 1995 975}%
    \special{pa 1995 1025}%
    \special{fp}%
    \special{ar 500 850 500 500 0 6.28319}%
    \special{pa 500 350}%
    \special{pa 500 600}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 525 530}%
    \special{pa 500 600}%
    \special{pa 475 530}%
    \special{pa 525 530}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.475in
    \rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize unfol ding\ }\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.250in
    \rlap{\kern 0.500in\lower\graphtemp\hbox to 0pt{\hss Safe Petri Nets\hss}}%
    \hbox{\vrule depth1.350in width0pt height 0pt}%
    \kern 3.225in
  }%
}%

\centerline{\raise 1em\box\graph}\vspace{-4ex}
\end{figure}
\pagebreak
event structures; and they in turn correspond bijectively with {\em
prime algebraic coherent Scott domains}.

In {\sc Winskel} \cite{Wi87a} a more general notion of event structure
was proposed, corresponding to a more general kind of Scott domain.
The event structures from \cite{NPW81} are now called {\em prime event
structures with binary conflict}. The translation from event
structures to domains passes through a stage of {\em families of
configurations of event structures}. {\sc Van Glabbeek \& Goltz}
\cite{GG90} found it convenient to use such families as a model of
concurrency in their own right. In this context the families were called
{\em configuration structures}.\vspace{-2ex}

\begin{figure}[htb]
%\input{structures}
\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 571 1429 381 381 0 6.28319}%
    \graphtemp=\baselineskip\multiply\graphtemp by -2\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.429in
    \rlap{\kern 0.571in\lower\graphtemp\hbox to 0pt{\hss  \hss}}%
    \graphtemp=.5ex\advance\graphtemp by 1.429in
    \rlap{\kern 0.571in\lower\graphtemp\hbox to 0pt{\hss 1-occurrence\hss}}%
    \graphtemp=\baselineskip\multiply\graphtemp by 2\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.429in
    \rlap{\kern 0.571in\lower\graphtemp\hbox to 0pt{\hss nets\hss}}%
    \special{ar 1524 476 476 476 0 6.28319}%
    \graphtemp=\baselineskip\multiply\graphtemp by -2\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.476in
    \rlap{\kern 1.524in\lower\graphtemp\hbox to 0pt{\hss  \hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.476in
    \rlap{\kern 1.524in\lower\graphtemp\hbox to 0pt{\hss Configuration\hss}}%
    \graphtemp=\baselineskip\multiply\graphtemp by 2\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.476in
    \rlap{\kern 1.524in\lower\graphtemp\hbox to 0pt{\hss structures\hss}}%
    \special{ar 2476 1429 333 333 0 6.28319}%
    \graphtemp=\baselineskip\multiply\graphtemp by -2\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.429in
    \rlap{\kern 2.476in\lower\graphtemp\hbox to 0pt{\hss Event\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 1.429in
    \rlap{\kern 2.476in\lower\graphtemp\hbox to 0pt{\hss structures\hss}}%
    \graphtemp=\baselineskip\multiply\graphtemp by 2\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.429in
    \rlap{\kern 2.476in\lower\graphtemp\hbox to 0pt{\hss  \hss}}%
    \special{ar 2476 1429 476 476 -0.052500 0.052500}%
    \special{ar 2476 1429 476 476 -0.248850 -0.143850}%
    \special{ar 2476 1429 476 476 -0.445199 -0.340199}%
    \special{ar 2476 1429 476 476 -0.641549 -0.536549}%
    \special{ar 2476 1429 476 476 -0.837898 -0.732898}%
    \special{ar 2476 1429 476 476 -1.034248 -0.929248}%
    \special{ar 2476 1429 476 476 -1.230597 -1.125597}%
    \special{ar 2476 1429 476 476 -1.426947 -1.321947}%
    \special{ar 2476 1429 476 476 -1.623296 -1.518296}%
    \special{ar 2476 1429 476 476 -1.819646 -1.714646}%
    \special{ar 2476 1429 476 476 -2.015995 -1.910995}%
    \special{ar 2476 1429 476 476 -2.212345 -2.107345}%
    \special{ar 2476 1429 476 476 -2.408694 -2.303694}%
    \special{ar 2476 1429 476 476 -2.605044 -2.500044}%
    \special{ar 2476 1429 476 476 -2.801394 -2.696394}%
    \special{ar 2476 1429 476 476 -2.997743 -2.892743}%
    \special{ar 2476 1429 476 476 -3.194093 -3.089093}%
    \special{ar 2476 1429 476 476 -3.390442 -3.285442}%
    \special{ar 2476 1429 476 476 -3.586792 -3.481792}%
    \special{ar 2476 1429 476 476 -3.783141 -3.678141}%
    \special{ar 2476 1429 476 476 -3.979491 -3.874491}%
    \special{ar 2476 1429 476 476 -4.175840 -4.070840}%
    \special{ar 2476 1429 476 476 -4.372190 -4.267190}%
    \special{ar 2476 1429 476 476 -4.568539 -4.463539}%
    \special{ar 2476 1429 476 476 -4.764889 -4.659889}%
    \special{ar 2476 1429 476 476 -4.961239 -4.856239}%
    \special{ar 2476 1429 476 476 -5.157588 -5.052588}%
    \special{ar 2476 1429 476 476 -5.353938 -5.248938}%
    \special{ar 2476 1429 476 476 -5.550287 -5.445287}%
    \special{ar 2476 1429 476 476 -5.746637 -5.641637}%
    \special{ar 2476 1429 476 476 -5.942986 -5.837986}%
    \special{ar 2476 1429 476 476 -6.139336 -6.034336}%
    \special{ar 1524 2381 476 476 0 6.28319}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 2.381in
    \rlap{\kern 1.524in\lower\graphtemp\hbox to 0pt{\hss Propositional\hss}}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 2.381in
    \rlap{\kern 1.524in\lower\graphtemp\hbox to 0pt{\hss theories\hss}}%
    \special{pa 333 1310}%
    \special{pa 810 1310}%
    \special{pa 810 1167}%
    \special{pa 333 1167}%
    \special{pa 333 1310}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.238in
    \rlap{\kern 0.571in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize occ.\ nets}\hss}}%
    \special{ar 2667 476 333 333 -0.075000 0.075000}%
    \special{ar 2667 476 333 333 -0.336799 -0.186799}%
    \special{ar 2667 476 333 333 -0.598599 -0.448599}%
    \special{ar 2667 476 333 333 -0.860398 -0.710398}%
    \special{ar 2667 476 333 333 -1.122198 -0.972198}%
    \special{ar 2667 476 333 333 -1.383997 -1.233997}%
    \special{ar 2667 476 333 333 -1.645796 -1.495796}%
    \special{ar 2667 476 333 333 -1.907596 -1.757596}%
    \special{ar 2667 476 333 333 -2.169395 -2.019395}%
    \special{ar 2667 476 333 333 -2.431194 -2.281194}%
    \special{ar 2667 476 333 333 -2.692994 -2.542994}%
    \special{ar 2667 476 333 333 -2.954793 -2.804793}%
    \special{ar 2667 476 333 333 -3.216593 -3.066593}%
    \special{ar 2667 476 333 333 -3.478392 -3.328392}%
    \special{ar 2667 476 333 333 -3.740191 -3.590191}%
    \special{ar 2667 476 333 333 -4.001991 -3.851991}%
    \special{ar 2667 476 333 333 -4.263790 -4.113790}%
    \special{ar 2667 476 333 333 -4.525590 -4.375590}%
    \special{ar 2667 476 333 333 -4.787389 -4.637389}%
    \special{ar 2667 476 333 333 -5.049188 -4.899188}%
    \special{ar 2667 476 333 333 -5.310988 -5.160988}%
    \special{ar 2667 476 333 333 -5.572787 -5.422787}%
    \special{ar 2667 476 333 333 -5.834587 -5.684587}%
    \special{ar 2667 476 333 333 -6.096386 -5.946386}%
    \graphtemp=.5ex\advance\graphtemp by 0.476in
    \rlap{\kern 2.667in\lower\graphtemp\hbox to 0pt{\hss \footnotesize \begin{tabular}{c}history\\ preserving\\ process\\ graphs\end{tabular}\hss}}%
    \special{pa 1286 357}%
    \special{pa 1762 357}%
    \special{pa 1762 214}%
    \special{pa 1286 214}%
    \special{pa 1286 357}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.286in
    \rlap{\kern 1.524in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize families}\hss}}%
    \special{pa 2286 1690}%
    \special{pa 2667 1690}%
    \special{pa 2667 1548}%
    \special{pa 2286 1548}%
    \special{pa 2286 1690}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.619in
    \rlap{\kern 2.476in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize prime}\hss}}%
    \special{pa 841 1159}%
    \special{pa 1187 813}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1122 842}%
    \special{pa 1187 813}%
    \special{pa 1158 878}%
    \special{pa 1122 842}%
    \special{fp}%
    \special{pa 1187 2044}%
    \special{pa 841 1698}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 870 1763}%
    \special{pa 841 1698}%
    \special{pa 906 1727}%
    \special{pa 870 1763}%
    \special{fp}%
    \special{pa 1429 943}%
    \special{pa 1429 1914}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1454 1848}%
    \special{pa 1429 1914}%
    \special{pa 1404 1848}%
    \special{pa 1454 1848}%
    \special{fp}%
    \special{pa 1619 1914}%
    \special{pa 1619 943}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1594 1010}%
    \special{pa 1619 943}%
    \special{pa 1644 1010}%
    \special{pa 1594 1010}%
    \special{fp}%
    \special{pa 1429 943}%
    \special{pa 1429 1914}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1454 1848}%
    \special{pa 1429 1914}%
    \special{pa 1404 1848}%
    \special{pa 1454 1848}%
    \special{fp}%
    \special{pa 1619 1914}%
    \special{pa 1619 943}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1594 1010}%
    \special{pa 1619 943}%
    \special{pa 1644 1010}%
    \special{pa 1594 1010}%
    \special{fp}%
    \special{pa 2302 1140}%
    \special{pa 1913 751}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1942 816}%
    \special{pa 1913 751}%
    \special{pa 1978 780}%
    \special{pa 1942 816}%
    \special{fp}%
    \special{pa 2188 1255}%
    \special{pa 1799 865}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1828 930}%
    \special{pa 1799 865}%
    \special{pa 1863 895}%
    \special{pa 1828 930}%
    \special{fp}%
    \special{pa 2188 1602}%
    \special{pa 1799 1992}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1863 1962}%
    \special{pa 1799 1992}%
    \special{pa 1828 1927}%
    \special{pa 1863 1962}%
    \special{fp}%
    \special{pa 1913 2106}%
    \special{pa 2201 1818}%
    \special{da 0.050}%
    \special{sh 1.000}%
    \special{pa 2137 1847}%
    \special{pa 2201 1818}%
    \special{pa 2172 1882}%
    \special{pa 2137 1847}%
    \special{fp}%
    \special{ar 571 1429 571 571 0 6.28319}%
    \special{pa 571 857}%
    \special{pa 571 1167}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 596 1100}%
    \special{pa 571 1167}%
    \special{pa 546 1100}%
    \special{pa 596 1100}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.012in
    \rlap{\kern 0.571in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize\raisebox{2pt}{\hspace*{1pt}unfold\hspace{1pt}ing}\cite{MMS92}}\hss}}%
    \special{pa 0 1429}%
    \special{pa 190 1429}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 124 1404}%
    \special{pa 190 1429}%
    \special{pa 124 1454}%
    \special{pa 124 1404}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.429in
    \rlap{\kern 0.095in\lower\graphtemp\hbox to 0pt{\hss \footnotesize 1-\hss}}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 1.429in
    \rlap{\kern 0.095in\lower\graphtemp\hbox to 0pt{\hss {\footnotesize unf}\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.762in
    \rlap{\kern 0.571in\lower\graphtemp\hbox to 0pt{\hss Pure Petri Nets\hss}}%
    \special{pa 1990 571}%
    \special{pa 2343 571}%
    \special{da 0.050}%
    \special{sh 1.000}%
    \special{pa 2276 546}%
    \special{pa 2343 571}%
    \special{pa 2276 596}%
    \special{pa 2276 546}%
    \special{fp}%
    \graphtemp=\baselineskip\multiply\graphtemp by -1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.571in
    \rlap{\kern 2.167in\lower\graphtemp\hbox to 0pt{\hss \raisebox{1pt}{\footnotesize\cite{vG95c}}\hss}}%
    \graphtemp=\baselineskip\multiply\graphtemp by 1\divide\graphtemp by 2
    \advance\graphtemp by .5ex\advance\graphtemp by 0.571in
    \rlap{\kern 2.167in\lower\graphtemp\hbox to 0pt{\hss  \hss}}%
    \special{pa 2343 381}%
    \special{pa 1990 381}%
    \special{da 0.050}%
    \special{sh 1.000}%
    \special{pa 2057 406}%
    \special{pa 1990 381}%
    \special{pa 2057 356}%
    \special{pa 2057 406}%
    \special{fp}%
    \hbox{\vrule depth2.857in width0pt height 0pt}%
    \kern 3.000in
  }%
}%
\centerline{\raise 1em\box\graph}\vspace{-4em}
\end{figure}

\noindent
The present paper   \hfill generalises the cor-\\
respondence between \hfill safe \,Petri \,nets \,and\\
configuration structures to unsafe nets. For this purpose we
use a more general kind of configuration structure, the {\em set
systems}. These have an attractive alternative presentation as
propositional theories.  As event structures are insufficiently
expressive, they are skipped as an intermediate step
in the translation. In the full version of this paper they will be
generalised to match all configuration structures. The connection
between configuration structures and Scott domains is generalised in
{\sc Van Glabbeek} \cite{vG95c}, where {\em history preserving process
graphs} are considered as an alternative presentation of (labelled)
domains.

\paragraph{Configuration structures}

A {\em set system} is given by a set $E$ and a collection $C$ of
subsets of $E$.  When a set system is used to represent a concurrent
system, we call it a {\em configuration structure}. The elements of
$E$ are then {\em events} and the elements of $C$ {\em
configurations}. An event represents an occurrence of an action the
system may perform; a configuration $X$ represents a state of the
system, namely the state in which the events in $X$ have occurred.
The configuration structures of \cite{GG90} were required 
to satisfy several requirements, due to \cite{Wi87a}, ensuring that
they could be obtained as the families of finite configurations of
event structures, namely
\begin{itemise}
\item all configurations are finite ({\em finitariness}),
\item $C$ contains the empty configuration ({\em rootedness}),
\item $C$ is closed under nonempty bounded unions ($\nbbigcup$),
\item and for any two distinct events occurring in a configuration there
is a subconfiguration containing one but not the other ({\em
coincidence-freeness}).
\end{itemise}
In the present paper a more expressive kind of configuration
structure is considered, not bound by these requirements. Many of our
results however concern finitary rooted configuration structures.  A
further generalisation of this model was previously proposed by {\sc
Pinna \& Poign\'e} \cite{PP95}. Their {\em event automata} are rooted
finitary configuration structures together with a transition relation
between the configurations.

Our configuration structures are, up to isomorphism, the {\em
extensional Chu spaces} of {\sc Gupta \& Pratt} \cite{GP93,Gup94,Pr94a}. It
was in their work that the idea arose of using the full generality of such
structures in modelling concurrency. It should be noted however
that the computational interpretation in \cite{GP93,Gup94,Pr94a}
differs slightly from that in \cite{NPW81,Wi87a,GG90,PP95}.

\paragraph{Formulae}

In Section \ref{formulae} we consider set systems from the point of
view of (infinitary) propositional logic: $E$ is now thought of as the
set of {\em propositions} and $C$ as the set of {\em models}.
Following {\sc Pratt} \cite{Pr94a} we observe a bijective
correspondence between configuration structures and infinitary
propositional theories up to logical equivalence.
We give a number of results equating the closure of $C$ under certain
operations with its axiomatisation by formulae of certain simple forms.

\paragraph{Event structures}

The behaviour of event structures is traditionally described in
terms of their configurations: the consistent and secured sets of
events.  In Section \ref{events} we relate this description with one
in terms of consistent and left-closed set of events. The later
corresponds with a {\em logical} view of event structures as
propositional theories.  A somewhat different logical view was
presented in {\sc Gunawardena} \cite{Gun92b}. The\pagebreak[4]
precise relations with ours are yet to be investigated.

In Section \ref{classification} we classify event
structures along three lines and discuss the characterisation of the
associated classes of configuration structures.

\paragraph{Equivalences}

A model of computation should have a notion of behaviour, and the
possibility of comparing behaviours with respect to suitable
equivalence relations.  To this end, in
Section~\ref{computational}, we equip configuration structures with
functions $l: E \rightarrow Act$ {\em labelling} events with {\em
actions}, and derive associated {\em asynchronous} labelled transition
relations.  We consider {various} {\em bisimulation} relations,
adapted for concurrency, between the resulting labelled transition
graphs. Section \ref{event-equiv}
considers several classes of event structures within this framework.
Whether previously known classes of event structures are as general as
arbitrary configuration structures depends on the notion of
equivalence used for the comparison.  Theorems~\ref{th-prime} and
\ref{th-conflict} are noteworthy in this respect; they imply that the
original event structures of \cite{NPW81} are {\em ST-bisimulation}
universal.

\paragraph{Petri nets}

In {\sc Meseguer, Montanari \& Sassone} \cite{MMS92}, arbitrary
(non-safe) Petri nets are unfolded into occurrence nets. Their
unfolding generalises the one of \cite{NPW81} and preserves the
behaviour of nets under a particular interpretation
due to {\sc Goltz \& Reisig} \cite{GR83}. We call this interpretation
the {\em individual token interpretation}. An alternative way of
understanding the behaviour of nets is the {\em collective token
interpretation}.  In the latter view there are nets which cannot be
represented by an event structure, let alone by a prime one with
binary conflict, or an occurrence net.

In Section \ref{nets} we establish a connection between {\em pure
nets} and configuration structures. Pure nets are nets without {\em
self-loops}. We {\em 1-unfold} pure nets into {\em pure 1-occurrence
nets}, which generalise the occurrence nets of \cite{NPW81}. These
pure 1-occurrence nets are shown to correspond with rooted finitary
configuration structures.

Through the translation into configuration structures the equivalence
notions on such structures are inherited by pure 1-occurrence nets;
we generalise them to all nets. The correspondence between pure
1-occurrence nets and configuration structures preserves the identity of
events and configurations ({\em configuration equivalence}). The
1-unfolding preserves any reasonable form of {\em history preserving
bisimulation equivalence} \cite{GG89ea} on nets, thus making any pure
net history preserving equivalent to a configuration structure.
Moreover, {\em any} net is ST-bisimulation equivalent to such a
structure (and hence to a prime event structure with binary conflict).
In contrast, we find a Petri net {\em not} history preserving
equivalent (in an appropriate sense) to any configuration structure. 
\\[2ex]
In future work we would like to connect our models with appropriate versions
of {\em higher dimensional automata} \cite{Pr91a}.
One could also consider other equivalence
relations appropriate for the study of concurrency, such as those based on
notions of multiple observers \cite{PP}.
In work on event structures {\sc Winskel} and others have employed
various notions of morphism~\cite{Wi87a};
yet another notion occurs in the category of Chu spaces. It seems likely
to be of importance to understand the relation with the present
equivalence-based approach.

\paragraph{Acknowledgment} We thank Vladimiro Sassone for helpful comments.

\section{The computational interpretation of configuration structures}
\label{computational}

In order to interpret a configuration structure as a concurrent
system, it is necessary to know, not only what are the admissible
states, but also how the system can evolve from one state to the
other.

\begin{definition}{transitions}
Let $(E,C)$ be a configuration structure. For $X,Y$ in $C$ write
$X \goto{} Y$ if
$X \subset Y$,
$Y-X$ is finite,
and $\forall Z (X \subset Z \subset Y \Rightarrow Z\in C)$.
The relation $\goto{}$ is called the {\em step transition relation}.
\end{definition}
Here $X\goto{}Y$ indicates that the represented system can go from
state $X$ to state $Y$ by concurrently performing a number of events
(namely the ones in $Y-X$). The first requirement is unavoidable. The
second one represents our assumption that in a finite time only
finitely many events can happen.  The last requirement says that a
number of events can be performed concurrently, or simultaneously,
only if they can be performed in any order. This requirement
represents our postulate that different events do not synchronise in
any way; they can happen in one step only if they are causally
independent. Hence our transition relation $\goto{}$ and the corresponding
computational interpretation of configuration structures could be called
{\em asynchronous}. 
It should be noted that other computational interpretations of
configuration structures are possible. The one of {\sc Gupta \& Pratt}
\cite{GP93,Gup94,Pr94a} is obtained by dropping the last two
requirements in \df{transitions}.
%
By labelling the events, we may observe transitions:
\begin{definition}{labelled}
A {\em labelled} configuration structure (over an alphabet $Act$) is a
triple $\eC = (E,C,l)$ with $(E,C)$ a configuration structure and $l:E
\rightarrow Act$.
\end{definition}
The components of such a structure C are denoted
$E_\eC$, $C_\eC$ and $l_\eC$ respectively (a convention that also
applies to other structures given as tuples).
The {\em labelled transition relation} \plat{X \goto{L} Y}, with $L$
a finite multiset of labels, holds iff $X \goto{} Y$ and $L =
\sum\{l(e)|{e\in (Y - X)}\}$.

\begin{example}{transitions}
These are the labelled transition relations for
$\eD = (\{d,e\},\{ \emptyset,
\{d\}, \{e\}, \{d,e\}\}, l)$ and $\eE = (\{d,e,f\},\{ \emptyset,
\{d\}, \{e\}, \{d,f\}, \{e,f\}, \{d,e,f\}\}, l)$, both
with $l(d)=a$, $l(e)=b$ and $l(f)=c$, and for a structure F.
\begin{center}
\begin{picture}(23,25)(-13,-5)
\put(0,0){\makebox[0pt]{$\emptyset$}} \put(-2,3){\vector(-1,1){5}}
\put(-10,10){\makebox[0pt]{$\{d\}$}}  \put(2,3){\vector(1,1){5}}
\put(10,10){\makebox[0pt]{$\{e\}$}}   \put(-8,13){\vector(1,1){5}}
\put(0,20){\makebox[0pt]{$\{d,e\}$}}  \put(8,13){\vector(-1,1){5}}
\put(0,4){\vector(0,1){13}}
\put(-7,3){\makebox[0pt]{\small $a$}}
\put(7,3){\makebox[0pt]{\small $b$}}
\put(-7,16){\makebox[0pt]{\small $b$}}
\put(7,16){\makebox[0pt]{\small $a$}}
\put(0,10){\makebox[0pt]{\small $ab$}}
\put(-13,-5){\makebox[0pt][l]{$\eD$}}
\end{picture}
\hfill
\begin{picture}(22,30)(-10,0)
\put(0,0){\makebox[0pt]{$\emptyset$}} \put(-2,3){\vector(-1,1){5}}
\put(-10,10){\makebox[0pt]{$\{d\}$}}  \put(2,3){\vector(1,1){5}}
\put(10,10){\makebox[0pt]{$\{e\}$}}   \put(-8,23){\vector(1,1){5}}
\put(-10,20){\makebox[0pt]{$\{d,f\}$}}  \put(-10,14){\vector(0,1){5}}
\put(10,20){\makebox[0pt]{$\{e,f\}$}}   \put(10,14){\vector(0,1){5}}
\put(0,30){\makebox[0pt]{$\{d,e,f\}$}}  \put(8,23){\vector(-1,1){5}}
\put(-7,3){\makebox[0pt]{\small $a$}}
\put(7,3){\makebox[0pt]{\small $b$}}
\put(-12,15){\makebox[0pt]{\small $c$}}
\put(12,15){\makebox[0pt]{\small $c$}}
\put(-7,26){\makebox[0pt]{\small $b$}}
\put(7,26){\makebox[0pt]{\small $a$}}
\put(-15,0){\makebox[0pt]{$\eE$}}
\end{picture}
\hfill
\begin{picture}(28,30)(-10,0)
\put(0,0){\makebox[0pt]{$\emptyset$}} \put(-2,3){\vector(-1,1){5}}
\put(-10,10){\makebox[0pt]{$\{d\}$}}  \put(2,3){\vector(1,1){5}}
\put(10,10){\makebox[0pt]{$\{e\}$}}   \put(-10,24){\vector(0,1){5}}
\put(-10,20){\makebox[0pt]{$\{d,f\}$}}  \put(-10,14){\vector(0,1){5}}
\put(10,20){\makebox[0pt]{$\{e,f'\}$}}   \put(10,14){\vector(0,1){5}}
\put(-10,30){\makebox[0pt]{$\{d,e,f\}$}} \put(10,24){\vector(0,1){5}}
\put(10,30){\makebox[0pt]{$\{d,e,f'\}$}} 
\put(-7,3){\makebox[0pt]{\small $a$}}   
\put(7,3){\makebox[0pt]{\small $b$}}    
\put(-12,15){\makebox[0pt]{\small $c$}} 
\put(12,15){\makebox[0pt]{\small $c$}}  
\put(-12,25){\makebox[0pt]{\small $b$}} 
\put(12,25){\makebox[0pt]{\small $a$}}
\put(-15,0){\makebox[0pt]{$\eF$}}
\end{picture}
\end{center}
\end{example}
Such pictures of configuration structures are somewhat misleading
representations, as they suggest a notion of global time, under which
at any time the represented system is in one of its states, moving
from one state to another by following the transitions. Although this
certainly constitutes a valid interpretation, we favour a more truly
concurrent view, in which all events can be performed independently,
unless the absence of certain configurations indicates otherwise.
Under this interpretation, the configurations can be thought of as
{\em possible} states the system can be in, {\em from the point of
view of a possible observer}. They are introduced only to indicate (by
their absence) the dependencies between events in the represented system.

In particular, in the structure D above, the events $d$
and $e$ are completely independent, and there is no need to assume
that they are performed either simultaneously or in a particular
order.  The ``diagonal'' in the picture serves merely to remind us of
the independence of these events.  In terms of higher dimensional
automata \cite{Pr91a} it indicates that ``the square is filled in''.

On the other hand, the absence of any ``diagonals'' in
E indicates two distinct linearly ordered computations. In one the event
$f$ can only happen after event $d$, and $e$ in turn has to wait for
$f$; the other has a causal ordering $e<f<d$. There is no way to
view $d$ and $e$ as independent; if there were, there should be a
transition \plat{\emptyset \goto{ab} \{d,e\}}.

If we do not care about the order of events $d$ and $e$ in
configuration structure D, we can say that the
configuration $\{d,e\}$ has only one {\em (concurrent) history}. The
configuration $\{d,e,f\}$ of structure E has two histories. In order
to count these histories formally, we introduce a concept of
(monoidal) {\em homotopy} between the paths in the graph
representations of configuration structures.

\begin{definition}{homotopy}
A {\em path} in a configuration structure C is a non-empty sequence of
configurations $X_0 X_1 \cdots X_n$, such that there is a transition
\plat{X_{i-1}\goto{} X_i} for $i=1,...,n$.
{\em Homotopy} is the smallest equivalence on the paths of C
such that if a path $\pi$ can be obtained by deleting a configuration
from another path $\rho$ (this not being the first or the last one in
$\rho$) then $\pi$ is equivalent to $\rho$.  A configuration $X$ is
{\em reachable} if there is a path $\emptyset X_1 \cdots X_n$ with
$X_n=X$. A {\em history} of a configuration is a homotopy class of
such paths.  
\end{definition}
Let $\fR$ be the operation that deletes all unreachable
configurations from configuration structures. The {\em reachable part}
$\fR(\eC)$ of structure $\eC$ is always finitary and coincidence-free.
Under the computational interpretation of \df{transitions} this is the
only part that matters. But, when possible, we will also take
unreachable configurations into account in connecting models of
concurrency, in order to accommodate computational interpretations such
as the one of Gupta and Pratt.

\paragraph{Equivalence relations}

In order to abstract from certain details in the representation of
concurrent systems we consider a range of equivalence relations on
configuration structures.
{\sc Van Glabbeek \& Goltz} \cite{GG89ea} suggest {\em history
preserving bisimulation equivalence}, defined on event structures in
terms of their configurations, as the coarsest equivalence completely
capturing the interplay of causality and branching. The most
straightforward generalisation of this notion to general configuration
structures is the following.

\begin{definition}{bisimulation}
Two rooted labelled conf.\ structures C and D are
{\em configuration preserving bisimulation equivalent} if
there is a relation $B \subseteq C_\eC \times C_\eD \times
2^{E_\eC \times E_\eD}$ such that $(\emptyset,\emptyset,\emptyset)
\!\in\! B$ and whenever $(X\!,Y\!,f) \!\in\! B$ then
\begin{list}{\bf -}{\leftmargin 12pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 4pt \itemsep 2pt \parsep 2pt}
\item $f$ is a bijection between $X$ and $Y$ preserving labelling and
subconfigurations (an {\em isomorphism}),
\item $X \goto{L} X' \in C_\eC \Rightarrow \exists Y',f'.
\left\{\begin{array}{@{}l@{}}
Y \goto{L} Y' \wedge f'\rest X \!=\! f\\ \wedge (X',Y',f')\in B,
\end{array}\right.$
\item \mbox{$Y \goto{L} Y' \in C_\eC \Rightarrow \exists X',f'. 
\left\{\begin{array}{@{}l@{}}
X \goto{L} X' \wedge f'\rest X \!=\! f\\ \wedge (X',Y',f')\in B.
\end{array}\right.$}
\end{list}
\end{definition}
However, this equivalence makes more
distinctions than necessary to capture causality and branching: it
distinguishes structures E and F above.  Therefore, in the full
version, we define {\em history preserving bisimulation equivalence}
to be a coarser equivalence, also generalising the relation from
\cite{GG89ea}, which identifies systems like E and F. Its definition is
similar, but with histories playing the r\^ole of configurations.  Even
coarser equivalences are {\em step-bisimulation} (as above, but
without the isomorphisms $f$) and {\em interleaving bisimulation
equivalence} (similar, but using only {\em single-action} transitions,
in which $L$ is a singleton). Between step and history preserving
bisimulation we have {\em ST-bisimulation equivalence} \cite{GV87},
based on a notion of state in which events may have been partly
executed.

\begin{definition}{ST}
An {\em ST-configuration} is a pair $(S,T)$ of configurations with $T
\goto{} S$. The elements of $S$ are the events that have {\em
started}, whereas $T$ contains the ones that have {\em terminated}.
The transition relation between configurations extends to one between
ST-configurations by putting \plat{(S,T) \goto{L,K} (S',T')} iff
\plat{S \goto{L} S'}, \plat{T \goto{K} T'} and $T \goto{} S'$. An {\em
ST-map} between $(S,T)$ and $(U,V)$ is a bijection $f:S \rightarrow U$
with $f(T)=V$.
ST-bisimulation equivalence is now defined as in \df{bisimulation},
but using ST-configurations and transitions instead of ordinary ones,
and letting the $f$'s be ST-maps.
\end{definition}

\paragraph{Process graphs}

In \cite{vG95c} rooted finitary configuration structures are
represented as labelled transition systems, or {\em process graphs},
by taking the configurations as states, the empty configuration as
initial state, and the single-action transitions as transitions. In
the graph representation of structure D from \ex{transitions} the two
$a$-transitions can be recognised as stemming from the same event
($d$) because they are opposites in a square. This cannot be said for
structure E and certainly not for F.  Let $\sim$ be the least
equivalence on single-action transitions such that if \plat{X \goto{a}
U \goto{b} Y}, \plat{X\goto{b} V \goto{a} Y} and $U \neq V$, then
$(X\goto{a}U) \sim (V\goto{a}Y)$. We say that a configuration
structure has {\em recognisable} events if the evident map from
equivalence classes to events is a bijection.  If this is the case,
the configuration structure, up to isomorphism, is completely
determined by its graph.

\section{Axiomatisation of set systems}\label{formulae}

In this section we consider set systems $\eC=(E,C)$ from a logical point of
view: $E$ is thought of as a collection of {\em propositions} and $C$ as
the collection of {\em models}. Connecting with the computational
point of view, we associate with an event the proposition that it has happened.
There is an associated theory $\Phi_\eC$ of all  valid sentences, those holding
in all models; these are the laws of $\eC$.

To make this precise, we choose a language: infinitary propositional logic
with $E$ as the set of propositional variables, and closed under negation
and all conjunctions of sets of formulae.
A formula $\phi$ is {\em valid} in $(E,C)$ iff it is true in all elements
of $C$;
$\Phi_{\eC}$ denotes the class of formulae valid in $\eC$.
Equally, given a class $\Phi$ of formulae over a set $E$,
we can define a configuration structure $\eC_{\Phi} =  (E,{\cal M}(\Phi))$,
where ${\cal M}(\Phi)$ is the set of {\em models} of $\Phi$, those
interpretations making every formula in $\Phi$ true.
We say that $\Phi$ {\em axiomatises} $\eC_{\Phi}$.
In particular $\Phi_\eC$ axiomatises C for any set system C.

This point of view is due to Pratt~\cite{GP93,Pr94a}. He noted a natural
``conjunctive  normal form.'' For any two subsets $X$,$Y$ of $E$, let
$X \Rightarrow Y$ abbreviate the ``propositional sequent''
$\bigwedge X \Rightarrow \bigvee Y$.
Then for any $(E,C)$, if $\Phi$ is the collection of sequents valid in
$(E,C)$ then $(E,C) = \eC_{\Phi}$.
Thus any configuration
structure can be axiomatised by a set of propositional sequents.

We now consider correspondences between axiomatisations by classes of
formulae and closure conditions on set systems.  First, there is
logical interest in {\em Scott sequents} where both antecedent and
consequent are finite, and also in {\em Tarski sequents} where,
further, the consequent is a singleton~\cite{Ga81,Sc74}.
\begin{proposition}{Scott}
A set system $(E,C)$ is Scott sequent axiomatisable  iff $C$ is
closed in the product topology on $2^E$.
It is Tarski sequent axiomatisable iff
$C$ is closed under intersections and directed unions.
\end{proposition}
Next we consider closure conditions that arise naturally when considering
configuration structures.
We denote closure under non-empty intersections by $\nbigcap$, under
bounded non-empty intersections by $\nbbigcap$, under bounded
non-empty unions by $\nbbigcup$ and under directed unions by
$\dbigcup$. 
The results appear below.
\begin{table}[htb]\vspace{-3ex}
\begin{center}
\begin{tabular}{|l|l|l| l|}
\hline
\rule{0pt}{12pt}stable & $\nbbigcap$ & $\equiv$ & $(\mbox{any},\mbox{ddc})$\\
 \cline{1-1}           & $\nbbigcap,\; \dbigcup$ & $\equiv$ &
$(\mbox{finite},\mbox{ddc})$\\
                                                 & $\nbbigcap,\; \nbbigcup$
& $\equiv$ & $(1, \mbox{ddc}),(\mbox{any},0)$\\
                                                 & $\nbbigcap,\;
\dbigcup,\; \nbbigcup$         & $\equiv$ &
$(1,\mbox{ddc}),(\mbox{finite},0)$\\
\hline
\rule{0pt}{12pt}prime    & $\nbigcap$
& $\equiv$ &  $(\mbox{any},\leq 1)$\\ \cline{1-1}
        & $\nbigcap,\; \dbigcup$
& $\equiv$ & $(\mbox{finite},\leq 1)$\\
         & $\nbigcap,\; \nbbigcup$
& $\equiv$ &  $(1, 1),(\mbox{any},0)$\\
         & $\nbigcap,\; \dbigcup,\; \nbbigcup$                  & $\equiv$
&  $(1, 1),(\mbox{finite},0)$\\
\hline
\rule{0pt}{12pt}union  & $\nbbigcup$

& $\equiv$ & $(1,\mbox{any}), (\mbox{any},0)$\\ \cline{1-1}
                                                 & $\nbbigcup,\dbigcup$

& $\Leftarrow$ & $  (1,\mbox{any}), (\mbox{finite},0)$\\
                                                 & $\dbigcup$

& $\Leftarrow$ & $ (\mbox{finite},\mbox{any})$ \\
\hline
\end{tabular}
\end{center}\vspace{-2ex}
\end{table}
The last column indicates the form of the allowed formulae which are
all implications. For example: $(\mbox{any}, \leq 1)$ indicates a
sequent with no restriction on the antecedent and whose consequent has
at most one element; and $(\mbox{any},\mbox{ddc})$ indicates an
implication whose antecedent can be any conjunction of propositional
letters, and whose consequent has the form $\bigdvee_{\; j\in J}\bigwedge
Z_{j}$ where the $Z_{j}$ are sets of letters, and we write $\bigdvee
\;\Phi$ for $(\bigvee \Phi) \wedge \bigwedge \{ \neg(\phi \wedge
\phi') \mid \phi,\phi' \in \Phi, \phi \neq \phi'\}$,
the {\em disjoint disjunction} of $\Phi$. So, for example the sixth
entry states that a configuration structure is axiomatisable by
sequents of the form $(\mbox{finite},\leq 1)$ iff it is closed under
non-empty bounded intersections and directed unions; this is
---essentially--- due to Larsen and Winskel~\cite{LW91} as
axiomatisations of the form $(\mbox{finite},\leq 1)$ correspond to
Scott information systems. The entries with $\Leftarrow$'s indicate
that only the implication from right to left holds; a counterexample
is provided by the collection of all co-finite proper subsets of the
natural numbers. A minor, but useful, variation, is to restrict to
rooted configuration structures (i.e.\ containing $\emptyset$); then
in the last column one changes ``any'' to ``non-empty,'' and ``finite''
to ``finite and non-empty'' on the left of the implications (but not
the right).

\section{Event structures}\label{events}

Event structures were introduced by {\sc Winskel}~\cite{Wi87a}:
\begin{definition}{event}
A {\em (general) event structure} is a triple $\eE = (E,Con,\turn)$ where
\begin{itemise}
\item $E$ is a set of {\em events},
\item $Con \subseteq \pow_f(E)$ is a nonempty {\em consistency
      predicate} such that:
      $Y \subseteq X \in Con \Rightarrow Y\in Con$,
\item and $\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{itemise}
\end{definition}
The idea behind the enabling relation is that an event $e$ can happen
only if a set $X$ of events enabling $e$ occurred previously; $Con$
consists of the finite sets of events that, potentially, can occur
during a single run of the system.  Winskel explained the behaviour of
event structures by associating with each E a family of configurations
$\fS(\eE)$, the possible states or runs of the system:
\begin{definition}{secured}
The set $\fS(\eE)$\footnote{We also write $\fS(\eE)$ for the
structure $(E,\fS(\eE))$.}
of {\em (secured) configurations} of an event
structure $\eE=(E,Con,\turn)$ consists of those $X \subseteq E$ which are
\begin{itemise}
\item {\em consistent}: every finite subset of $Y$ 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{itemise}
\end{definition}
Winskel \cite{Wi87a} gave an {\em intrinsic} characterisation of the
configuration structures of event structures.  A
family of configurations $C$ is of the form $\fS(\eE)$ iff $C$ is
non-empty and has the properties of {\em finite-completeness}, {\em
finiteness} and {\em coincidence-freeness}.  Here a family of
configurations is
finitely-complete iff it is closed under directed unions and bounded
unions (or equivalently bounded finite unions);
finiteness means that if an event occurs in a configuration, then it
occurs in a finite subconfiguration. The properties of finiteness and
closure under directed unions together say that the infinite
configurations are precisely the directed unions of the finite ones;
let us call this property {\em $\dbigcup$-finitary}. Furthermore, the
properties of non-emptiness and closure under bounded unions are
equivalent to rootedness and closure under nonempty bounded unions
($\nbbigcup$). It follows that a set of configurations is the
$\fS$-image of an event structure iff it is $\dbigcup$-finitary,
rooted, $\nbbigcup$-closed and coincidence-free.

Instead of using all configurations to describe the behaviour of an
event structure E, one can just as well restrict attention to the
finite ones, $\fS_{f}(\eE)$ (for $\fS(\eE)$ can be
recovered from $\fS_{f}(\eE)$ by means of closure under directed unions).
The corresponding characterisation has already been mentioned in the
introduction. Note that finitariness and coincidence-freeness come for
free when considering reachable parts of configuration structures.

We consider yet another interpretation of event structures as
configuration structures, namely by using the {\em left-closed}
configurations. These are the consistent sets of events $X$ that satisfy
$\forall e \in X.~\exists Y \subseteq X.~Y\turn e$.

We show that the left-closed interpretation of event structures is
almost the same as the secured interpretation. In order to rule out a
pathological case where this does not hold, we define the {\em irreflexive}
event structures to be the ones satisfying
$X \turn e \Rightarrow X-\{e\} \turn e$.
Note that every event structure E can be transformed into an irreflexive
one with the same secured configurations by deleting unwanted
enablings $X \turn e$ with $e \in X$. Such a transformation preserving
the left-closed configurations $\fL(\eE)$ is obtained by adding the missing
enablings $X-\{e\} \turn e$ (when $X \turn e$). Thus under both
interpretations it is no essential limitation to consider irreflexive
event structures only. The following proposition says that for such
structures the left-closed interpretation contains more
information than the secured interpretation.
\begin{proposition}{irreflexive}
Let E be an irreflexive event structure. Then $\fS_{f}(\eE) =
\fR(\fL(\eE))$.
\end{proposition}
Under the computational interpretation of \df{transitions} any such extra
information is irrelevant and $\fL$ and $\fS$ can be regarded as equivalent.

With any event structure $\eE=(E,Con,\turn)$ we also associate the
propositional theory\vspace{-2ex} 
$$\Phi(\eE) = \{ \bigwedge X \Rightarrow \bot \mid X \in \pow_f(E) - Con \} 
\vspace{-2ex}$$
$$\cup\; \textstyle\{ e \Rightarrow \bigvee \{\bigwedge Y \mid Y \turn e \}\}.\vspace{-1ex}$$
This logical view of event structures
corresponds exactly with the left-closed interpretation:
\begin{proposition}{logical} $\eC_{\Phi(\eE)} = \fL(\eE)$ for any E.
\end{proposition}
We have no exact characterisation of the structures of
the form $\fL(\eE)$; however, a structure is of the form $\fL_f(\eE)$
(the {\em finite} left-closed configurations of an event structure)
iff it is finitary, rooted and $\nbbigcup$-closed.

\subsection{Other brands of event structures}\label{classification}

One can classify general event structures along three dimensions:
stability, having recognisable events and degree of conflict.
A further subclass of {\em synchronisation trees}~\cite{Mi80}
will also be considered. Yet other classes have been considered in the
literature, for example {\em bundle} event structures~({\sc
Langerak}~\cite{Lk92}) and {\em flow} event structures ({\sc
Boudol}~\cite{Bo90} and Castellani).

\begin{definition}{stable}
$\eE$ is {\em stable} iff $X \turn_{\eE} e$, $Y \turn_{\eE} e$ and\\
$X \cup Y \cup \{e\} \in Con_{\eE}$ imply $X\cap Y \turn_{\eE} e$.
\end{definition}
Winskel defined the stable event structures in~\cite{Wi87a}.  The
causal dependencies between the events in a configuration of such a
structure can be given by a partial order. The
intrinsic characterisation of the configuration structures of
stable event structures consists of the same requirements as above,
together with closure under nonempty bounded intersections ({\em
stability}). Stability is equivalent to an interesting {\em local completion
principle}: if $X \subseteq Y \in C$ then there is a least $Y'$ in $C$
with $X \subseteq Y' \subseteq Y$.

Say that an event structure E has recognisable events iff the associated
configuration structure $\fS(\eE)$ does.
We do not possess a particularly pleasing description of those event
structures with recognisable events, or of their associated
configuration structures.  However, we do in the case where they are
stable.

\begin{definition}{prime}
${\eE}$ is {\em prime} iff for all $e$ in $E$, $e$ occurs in an
$\fS$-configuration, and there is a least $X$ with $X \turn e$.
\end{definition}
This is (configuration) equivalent to the original definition in \cite{Wi87a}.
 Prime event structures possess a transitive
{\em global causal dependency} relation, where $e \leq e'$ iff
$e\!\in\! X$ where $X$ is the least configuration containing $e'$.
\begin{proposition}{prime=stable+persistent}
An event structure has the same configurations as a prime event structure
iff it has the same configurations as a stable one with recognisable events.
\end{proposition}
The configuration structures associated to prime event structures can be
characterised by strengthening
stability to the requirement that  $(E,C)$ be {\em prime}, meaning that
$C$ is closed under non-empty intersections.
Primality is equivalent to a {\em global} completion principle: if $X
\subseteq Y \in C$ then there is a least $Y'$ in $C$ with $X \subseteq
Y'$.

\pagebreak[3]
The other dimension of variation is the degree of consistency. We consider
one possibility:

\begin{definition}{binary conflict}
${\eE}$  has {\em binary conflict} if every $X$ not in
$Con$ has a subset not in $Con$ with two elements.
\end{definition}
See~\cite{Wi89} for a direct definition, and also  for the stable case.
The prime event structures with binary conflict are (equivalent to)
the original event structures from {\sc Nielsen, Plotkin and
Winskel}~\cite{NPW81}.
They are characterised by the requirements for general event structures
plus primality and {\em coherence}, that for all $X,Y,Z$ in $C$ if each of
$X\cup Y,Y\cup Z,Z\cup X$ is in $C$, then $X\cup Y\cup Z$ is too. It was noted
by Arend Rensink that this does not extend to stable event structures.

Finally we consider {\em synchronisation trees}.  These are the prime
event structures with binary conflict such that for any two
consistent events $e$,$e'$ either $e \leq e'$ or $e' \leq e$.
This is equivalent to the definition in \cite{Mi80}.  Their
configuration structures can be characterised by the extra
requirement of linearity: if $X$ and $Y$ are a bounded pair of
configurations, then $X \subseteq Y$ or $Y \subseteq X$.

Up to configuration equivalence, the classes of structures of this section
are related by inclusion as indicated below.
For the sake of completeness, the flow and bundle event structures are
indicated as well.
\begin{figure}[htb]
\begin{center}
\unitlength 1   mm 
\begin{picture}(20,40)(-10,-10)
\put(0,-10){\makebox(0,0){$\bullet$}}  \put(0,-10){\line(0,1){10}}
\put(0,0){\makebox(0,0){$\bullet$}}    \put(0,0){\line(-1,1){10}}
\put(-10,10){\makebox(0,0){$\bullet$}} \put(0,0){\line(0,1){10}}
\put(0,10){\makebox(0,0){$\bullet$}}   \put(0,0){\line(1,1){10}}
\put(10,10){\makebox(0,0){$\bullet$}}  \put(-10,10){\line(0,1){10}}
\put(-10,20){\makebox(0,0){$\bullet$}} \put(-10,10){\line(1,1){10}}
\put(0,20){\makebox(0,0){$\bullet$}}   \put(0,10){\line(-1,1){10}}
\put(10,20){\makebox(0,0){$\bullet$}}  \put(0,10){\line(1,1){10}}
\put(0,30){\makebox(0,0){$\bullet$}}   \put(10,10){\line(-1,1){10}}
\put(10,10){\line(0,1){10}}            \put(-10,20){\line(1,1){10}}
\put(10,20){\line(-1,1){10}}           \put(0,20){\line(0,1){10}}
\put(0,3.33){\makebox(0,0){$\bullet$}}
\put(0,6.67){\makebox(0,0){$\bullet$}}
\put(-2,-10){\makebox(0,0)[r]{\small (synchronisation)}}
\put(2,-10){\makebox(0,0)[l]{\small trees \cite{Mi80}}}
\put(-2,0){\makebox(0,0)[tr]{\small prime}}
\put(2,0){\makebox(0,0)[tl]{\small with binary conflict \cite{NPW81}}}
\put(12,10){\makebox(0,0)[l]{\small prime \cite{Wi87a}}}
\put(12,20){\makebox(0,0)[l]{\small stable \cite{Wi87a}}}
\put(-2,30){\makebox(0,0)[br]{\small general}}
\put(2,30){\makebox(0,0)[bl]{\small event structures \cite{Wi87a}}}
\put(-12,22){\makebox(0,0)[r]{\small event structures \cite{Wi89}}}
\put(-12,18.5){\makebox(0,0)[r]{\small with binary conflict}}
\put(-12,11.5){\makebox(0,0)[r]{\small binary conflict and}}
\put(-12,8){\makebox(0,0)[r]{\small recognisable events}}
\put(-1.5,3.3){\makebox(0,0)[r]{\scriptsize bundle}}
\put(2,3.3){\makebox(0,0)[l]{\scriptsize \cite{Lk92}}}
\put(-1.5,6.7){\makebox(0,0)[r]{\scriptsize flow}}
\put(2,6.7){\makebox(0,0)[l]{\scriptsize \cite{Bo90}}}
\put(2,10){\makebox(0,0)[l]{\scriptsize \cite{Wi89}}}
\put(-1.5,20){\makebox(0,0)[r]{\scriptsize rec.}}
\put(1.5,20){\makebox(0,0)[l]{\scriptsize ev.}}
\end{picture}
\end{center}
\end{figure}\vspace{-1.5em}

\subsection{The difference between the brands of structures up to
equivalence notions}\label{event-equiv}

One defines {\em labelled} event structures, and their associated
labelled configuration structures, in the evident way.  From here
onwards we assume all structures to be labelled. The equivalence
relations from Section~\ref{computational} are inherited by (labelled)
irreflexive event structures via $\fL$.
We now turn to comparing classes of event structures and configuration
structures with respect to our ``test range'' of equivalences.  We
only state our results; the proofs will appear in the full version of
this paper.

\begin{proposition}{tree}
Every rooted configuration structure is interleaving bisimulation
equivalent to a synchronisation tree.
\end{proposition}
Since interleaving bisimulation and synchronisation trees were
introduced when considering concurrency as interleaving, this
proposition may not be surprising.
More of a surprise may be that, as regards ST-bisimulation,
the prime event structures are universal.
\begin{theorem}{prime}
Every rooted configuration structure is ST-bisimulation equivalent to a
prime event structure.
\end{theorem}
We can reduce yet further, to {\em binary} conflict:

\begin{theorem}{conflict}
Every (prime) event structure is history preserving bisimulation
equivalent to 
an event structure (resp., prime event structure) with binary conflict.
\end{theorem}
Putting these together, we see that every configuration structure is
ST-bisimulation equivalent to a prime event structure with
binary conflict. On the other hand, there is a configuration structure
not history-preserving bisimulation equivalent to any event structure.
In the terminology of the Section~\ref{formulae}, it is the one with three
events $a$,$b$,$c$ axiomatised by $a \wedge b \Rightarrow c$.

\section{Petri nets}\label{nets}

\begin{definition}{petri}\hfill\mbox{}\\
A (labelled) {\em Petri net} is a tuple $(S,T,F,K,M_0,l)$ with
\begin{itemise}\vspace{-1ex}
\item $S$ and $T$ two disjoint sets of {\em places} 
and {\em transitions},%
\vspace{-1ex}\item $F: (S \times T \cup T\times S)\rightarrow \IN$,
the {\em flow relation},
\vspace{-1ex}\item $K: S \rightarrow \IN \cup \{\infty\}$, the {\em capacity
allocation},
\vspace{-1ex}\item $M_0:S \rightarrow \IN$, the {\em initial marking},\\
satisfying $M_0(s)\leq K(s)$ for $s \in S$.
\vspace{-1ex}\item and $l: T \rightarrow Act$, the {\em labelling function}.
\end{itemise}\vspace{-1ex}
\end{definition}
Petri nets are pictured by drawing the places as circles (subscripted
by `$\kappa = K(s)$' if they have finite capacity) and the
transitions as boxes, containing their label. Between $s$ in $S$ and
$t$ in $T$ there are $F(s,t)$ {\em arcs}.

When a Petri net represents a concurrent system, a global state of
such a system is given as a {\em marking}, a function $M:S \rightarrow
\IN$ satisfying $M(s)\leq K(s)$ for $s\in S$. Such a state is depicted
by placing $M(s)$ dots ({\em tokens}) in each place $s$. The initial state
is given by the marking $M_0$. 
In order to describe the behaviour of a net, we describe the the step
transition relation between markings.
\begin{definition}{firing}
Let $M:S \rightarrow \IN$ be a marking of a net.
A finite multiset $U:T \rightarrow \IN$ of transitions is {\em enabled}
under $M$ if $\Sigma_{t\in T} U(t) \cdot F(s,t) \leq M(s)$ and
$M'(s)=M(s)+\Sigma_{t\in T} U(t) \cdot (F(t,s)-F(s,t))\leq K(s)$
for all $s\in S$. In that case $U$ can {\em fire} under $M$, yielding
the marking $M'$, written \plat{M \goto{U} M'}.

A chain $M_0 \goto{U_1} M_1 \goto{U_2} \cdots \goto{U_n} M_n$ starting
from the initial marking $M_0$ is called a {\em firing sequence}.
A marking $M$ is {\em reachable} if there is such a sequence ending in $M=M_n$.
\end{definition}
If a set $U$ of transitions fires, for every transition $t$ in $U$ and
every arc from a place $s$ to $t$, a token moves along that arc
from $s$ to $t$. These tokens are consumed by the firing, but also new
tokens are created, namely one for every outgoing arc of $t$. These end up
in the places at the end of those arcs. If $t$ occurs several times in
$U$, all this happens several times (in parallel) as well.

The firing of $U$ is only possible if there are sufficiently many
tokens in the {\em preplaces} of $U$ (the ones where the incoming arcs
come from) and if by firing $U$, the capacities of the {\em
postplaces} (where the outgoing arcs go to) are not exceeded.
This is expressed by the two conditions in \df{firing}.

\begin{definition}{capacities}
A net is said to be without capacities if the range of $K$ is
$\{\infty\}$ and without arc\-weights if the range of $F$ is $\{0,1\}$.
\end{definition}

\paragraph{Equivalence relations on nets and the correspondence with
set systems}

There are two different schools of thought in interpreting the causal
behaviour of nets, which can be described as the {\em individual} and
{\em collective token} philosophy.\footnote{The individual token
interpretation of ordinary nets has nothing to do with the concept of
{\em Petri nets with individual tokens}; there the individuality is
hardwired into the syntax of nets.} The following example illustrates
their difference.

\begin{figure}[htp]
%\input{tokens}
\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.125in
    \rlap{\kern 0.000in\lower\graphtemp\hbox to 0pt{\hss A:\hss}}%
    \special{pn 8}%
    \special{ar 375 125 125 125 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 0.375in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 500 125}%
    \special{pa 750 125}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 650 100}%
    \special{pa 750 125}%
    \special{pa 650 150}%
    \special{pa 650 100}%
    \special{fp}%
    \special{pa 750 250}%
    \special{pa 1000 250}%
    \special{pa 1000 0}%
    \special{pa 750 0}%
    \special{pa 750 250}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 0.875in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 1000 125}%
    \special{pa 1250 125}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1150 100}%
    \special{pa 1250 125}%
    \special{pa 1150 150}%
    \special{pa 1150 100}%
    \special{fp}%
    \special{ar 1375 125 125 125 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 1.375in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1500 125}%
    \special{pa 1750 125}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1650 100}%
    \special{pa 1750 125}%
    \special{pa 1650 150}%
    \special{pa 1650 100}%
    \special{fp}%
    \special{pa 1750 250}%
    \special{pa 2000 250}%
    \special{pa 2000 0}%
    \special{pa 1750 0}%
    \special{pa 1750 250}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 1.875in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pa 2000 125}%
    \special{pa 2250 125}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2100 150}%
    \special{pa 2000 125}%
    \special{pa 2100 100}%
    \special{pa 2100 150}%
    \special{fp}%
    \special{ar 2375 125 125 125 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 2.375in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \hbox{\vrule depth0.250in width0pt height 0pt}%
    \kern 2.500in
  }%
}%
\centerline{\raise 1em\box\graph}
\end{figure}
\noindent
In this net, the transitions labelled $a$ and $b$ can fire once each.
After $a$ has fired, there are two tokens in the middle place.
According to the individual token philosophy, it makes a
difference which of these tokens is used in firing $b$. If the token
that was there already is used (which must certainly be the case if
$b$ happens before the token from $a$ arrives), the transitions $a$
and $b$ are causally independent. If the token that was produced by
$a$ is used, $b$ is causally dependent on $a$. Thus, the net A above
has two maximal computations, that can be characterised by the partial orders
\plat{\begin{array}{@{}c@{}}a\\[-3pt]b\end{array}} and 
\begin{picture}(11,0)
\put(0,0){$a$}
\put(3,1){\vector(1,0){5}}
\put(9,0){$b$}
\end{picture}. 
According to the collective token philosophy on the other hand, all
that is present in the middle place after the occurrence of $a$ is the
number 2. The preconditions for $b$ to fire do not change, and
consequently $b$ is always causally independent of $a$.

The individual token approach has been formalised by the notion of a
{\em process}, described in {\sc Goltz \& Reisig} \cite{GR83}.
A causality respecting bisimulation relation based on this approach
was proposed by {\sc Best, Devillers, Kiehn \& Pomello} \cite{BDKP91}
under the name {\em fully concurrent bisimulation}. It can be regarded
as a form of history preserving bisimulation with these
processes as histories. Below we contribute a form of history
preserving bisimulation, and several related equivalences, based on
the collective token philosophy. That both philosophies yield
incomparable notions of equivalence follows from the following example.

\begin{figure}[htb]
%\input{incomparable}
\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.125in
    \rlap{\kern 0.000in\lower\graphtemp\hbox to 0pt{\hss B:\hss}}%
    \special{pn 8}%
    \special{ar 375 125 125 125 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 0.375in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 500 125}%
    \special{pa 750 125}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 650 100}%
    \special{pa 750 125}%
    \special{pa 650 150}%
    \special{pa 650 100}%
    \special{fp}%
    \special{pa 750 250}%
    \special{pa 1000 250}%
    \special{pa 1000 0}%
    \special{pa 750 0}%
    \special{pa 750 250}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 0.875in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 1000 125}%
    \special{pa 1250 125}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1150 100}%
    \special{pa 1250 125}%
    \special{pa 1150 150}%
    \special{pa 1150 100}%
    \special{fp}%
    \special{ar 1375 125 125 125 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 1.375in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1750 250}%
    \special{pa 2000 250}%
    \special{pa 2000 0}%
    \special{pa 1750 0}%
    \special{pa 1750 250}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 1.875in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pa 2000 125}%
    \special{pa 2250 125}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2100 150}%
    \special{pa 2000 125}%
    \special{pa 2100 100}%
    \special{pa 2100 150}%
    \special{fp}%
    \special{ar 2375 125 125 125 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 2.375in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \hbox{\vrule depth0.250in width0pt height 0pt}%
    \kern 2.500in
  }%
}%
\centerline{\raise 1em\box\graph}
\end{figure}
\noindent
In the collective token philosophy the precondition of $b$ expressed
by the place in the middle is redundant, and hence A must be
equivalent to B\@. A and B are not fully concurrent bisimulation equivalent
however, as B lacks the computation
\begin{picture}(11,0)
\put(0,0){$a$}
\put(3,1){\vector(1,0){5}}
\put(9,0){$b$}
\end{picture}. 
On the other hand, A is fully concurrent bisimulation equivalent with
C below.%
\begin{figure}[htb]
\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.125in
    \rlap{\kern 0.000in\lower\graphtemp\hbox to 0pt{\hss C:\hss}}%
    \special{pn 8}%
    \special{ar 375 125 125 125 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 0.375in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 500 125}%
    \special{pa 750 125}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 650 100}%
    \special{pa 750 125}%
    \special{pa 650 150}%
    \special{pa 650 100}%
    \special{fp}%
    \special{pa 750 250}%
    \special{pa 1000 250}%
    \special{pa 1000 0}%
    \special{pa 750 0}%
    \special{pa 750 250}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 0.875in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 1000 125}%
    \special{pa 1250 125}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1150 100}%
    \special{pa 1250 125}%
    \special{pa 1150 150}%
    \special{pa 1150 100}%
    \special{fp}%
    \special{ar 1375 125 125 125 0 6.28319}%
    \special{pa 1500 125}%
    \special{pa 1750 125}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1650 100}%
    \special{pa 1750 125}%
    \special{pa 1650 150}%
    \special{pa 1650 100}%
    \special{fp}%
    \special{pa 1750 250}%
    \special{pa 2000 250}%
    \special{pa 2000 0}%
    \special{pa 1750 0}%
    \special{pa 1750 250}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 1.875in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pa 2000 125}%
    \special{pa 2250 125}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2100 150}%
    \special{pa 2000 125}%
    \special{pa 2100 100}%
    \special{pa 2100 150}%
    \special{fp}%
    \special{ar 2375 125 125 125 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.125in
    \rlap{\kern 2.375in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1750 600}%
    \special{pa 2000 600}%
    \special{pa 2000 350}%
    \special{pa 1750 350}%
    \special{pa 1750 600}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.475in
    \rlap{\kern 1.875in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pa 2268 189}%
    \special{pa 2000 350}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2099 320}%
    \special{pa 2000 350}%
    \special{pa 2073 277}%
    \special{pa 2099 320}%
    \special{fp}%
    \special{ar 1375 475 125 125 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.475in
    \rlap{\kern 1.375in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1500 475}%
    \special{pa 1750 475}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1650 450}%
    \special{pa 1750 475}%
    \special{pa 1650 500}%
    \special{pa 1650 450}%
    \special{fp}%
    \hbox{\vrule depth0.600in width0pt height 0pt}%
    \kern 2.500in
  }%
}%
\centerline{\raise 1em\box\graph}
\end{figure}

\noindent
In fact, C is the occurrence net obtained from A by the
unfolding of {\sc Meseguer, Montanari \& Sassone} \cite{MMS92},
mentioned in the introduction.
In the individual token philosophy, both nets have the computations
\plat{\begin{array}{c}a\\[-3pt]b\end{array}} and 
\begin{picture}(11,0)
\put(0,0){$a$}
\put(3,1){\vector(1,0){5}}
\put(9,0){$b$}
\end{picture}. 
However, A does not have a run
\begin{picture}(11,0)
\put(0,0){$a$}
\put(3,1){\vector(1,0){5}}
\put(9,0){$b$}
\end{picture}
in the collective token philosophy, and can therefore not be
equivalent to C in any causality preserving way.

One often is interested in the behaviour of nets as far as it can be
expressed in terms of transition firings. The places etc.\ are then
seen as just a tool in specifying such behaviour. In this view, one of the
most discriminating behavioural equivalences we can think of in the
collective token framework is the following notion of {\em marking
equivalence}:
\begin{definition}{marking equivalence}
Two nets $N$ and $N'$ are {\em marking equivalent} if $T_N = T_{N'}$
and there exists a bijection $i$ between their reachable markings,
such that the initial markings are related, $M \goto{U}_{N} M'
\Leftrightarrow i(M) \goto{U}_{N'} i(M')$, and $l_N = l_{N'}$.
\end{definition}
Note that marking equivalence preserves all causal information
present in the net representation of a concurrent system. Whether two
transitions are causally independent is a context-sensitive matter. It
varies with the markings enabling them both. In such a marking two
transitions are independent iff they can fire in one step. This
kind of information is present in the step transition relation \plat{\goto{U}}.
The nets A and B are marking equivalent. However,
for many purposes marking equivalence is too fine. 
It distinguishes for instance the nets P and Q below, as well as M and N.

 \begin{figure}[t]
 %\input{marking}
\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.804in
    \rlap{\kern 1.250in\lower\graphtemp\hbox to 0pt{\hss P:\hss}}%
    \special{pn 8}%
    \special{ar 1768 804 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.804in
    \rlap{\kern 1.768in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 2036 536}%
    \special{pa 2214 536}%
    \special{pa 2214 357}%
    \special{pa 2036 357}%
    \special{pa 2036 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 2.125in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 1.946in\lower\graphtemp\hbox to 0pt{\hss $t_1$\hss}}%
    \special{ar 1876 554 250 250 -0.074252 1.645049}%
    \special{sh 1.000}%
    \special{pa 2103 573}%
    \special{pa 2125 536}%
    \special{pa 2153 569}%
    \special{pa 2103 573}%
    \special{fp}%
    \special{pa 1321 536}%
    \special{pa 1500 536}%
    \special{pa 1500 357}%
    \special{pa 1321 357}%
    \special{pa 1321 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 1.411in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 1.232in\lower\graphtemp\hbox to 0pt{\hss $t_2$\hss}}%
    \special{ar 1660 554 250 250 1.496544 3.215845}%
    \special{sh 1.000}%
    \special{pa 1383 569}%
    \special{pa 1411 536}%
    \special{pa 1433 573}%
    \special{pa 1383 569}%
    \special{fp}%
    \special{ar 1768 89 89 89 0 6.28319}%
    \special{ar 1660 339 250 250 3.067340 4.786641}%
    \special{sh 1.000}%
    \special{pa 1645 62}%
    \special{pa 1679 89}%
    \special{pa 1641 112}%
    \special{pa 1645 62}%
    \special{fp}%
    \special{ar 1876 339 250 250 -1.645049 0.074252}%
    \special{sh 1.000}%
    \special{pa 1895 112}%
    \special{pa 1857 89}%
    \special{pa 1891 62}%
    \special{pa 1895 112}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.804in
    \rlap{\kern 2.589in\lower\graphtemp\hbox to 0pt{\hss Q:\hss}}%
    \special{ar 3036 804 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.804in
    \rlap{\kern 3.036in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 3304 536}%
    \special{pa 3482 536}%
    \special{pa 3482 357}%
    \special{pa 3304 357}%
    \special{pa 3304 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 3.393in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 3.214in\lower\graphtemp\hbox to 0pt{\hss $t_1$\hss}}%
    \special{pa 3099 740}%
    \special{pa 3304 536}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3261 543}%
    \special{pa 3304 536}%
    \special{pa 3296 579}%
    \special{pa 3261 543}%
    \special{fp}%
    \special{pa 2589 536}%
    \special{pa 2768 536}%
    \special{pa 2768 357}%
    \special{pa 2589 357}%
    \special{pa 2589 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 2.679in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 2.500in\lower\graphtemp\hbox to 0pt{\hss $t_2$\hss}}%
    \special{pa 2973 740}%
    \special{pa 2768 536}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2775 579}%
    \special{pa 2768 536}%
    \special{pa 2811 543}%
    \special{pa 2775 579}%
    \special{fp}%
    \special{ar 2679 89 89 89 0 6.28319}%
    \special{pa 2679 357}%
    \special{pa 2679 179}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2654 214}%
    \special{pa 2679 179}%
    \special{pa 2704 214}%
    \special{pa 2654 214}%
    \special{fp}%
    \special{ar 3393 89 89 89 0 6.28319}%
    \special{pa 3393 357}%
    \special{pa 3393 179}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 3368 214}%
    \special{pa 3393 179}%
    \special{pa 3418 214}%
    \special{pa 3368 214}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 3.857in\lower\graphtemp\hbox to 0pt{\hss M:\hss}}%
    \special{ar 4089 446 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 4.089in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 4000 179}%
    \special{pa 4179 179}%
    \special{pa 4179 0}%
    \special{pa 4000 0}%
    \special{pa 4000 179}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 4.089in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 3.911in\lower\graphtemp\hbox to 0pt{\hss $t_1$\hss}}%
    \special{ar 3940 252 250 250 -0.298444 0.552547}%
    \special{sh 1.000}%
    \special{pa 4192 366}%
    \special{pa 4152 383}%
    \special{pa 4150 340}%
    \special{pa 4192 366}%
    \special{fp}%
    \special{ar 4239 252 250 250 2.589046 3.440037}%
    \special{sh 1.000}%
    \special{pa 3966 205}%
    \special{pa 4000 179}%
    \special{pa 4013 220}%
    \special{pa 3966 205}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.804in
    \rlap{\kern 3.857in\lower\graphtemp\hbox to 0pt{\hss N:\hss}}%
    \special{ar 4089 804 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.804in
    \rlap{\kern 4.089in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 4179 804}%
    \special{pa 4357 804}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 4321 779}%
    \special{pa 4357 804}%
    \special{pa 4321 829}%
    \special{pa 4321 779}%
    \special{fp}%
    \special{pa 4357 893}%
    \special{pa 4536 893}%
    \special{pa 4536 714}%
    \special{pa 4357 714}%
    \special{pa 4357 893}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.804in
    \rlap{\kern 4.446in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 4536 804}%
    \special{pa 4714 804}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 4679 779}%
    \special{pa 4714 804}%
    \special{pa 4679 829}%
    \special{pa 4679 779}%
    \special{fp}%
    \special{ar 4804 804 89 89 0 6.28319}%
    \special{pa 4893 804}%
    \special{pa 5071 804}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 5036 779}%
    \special{pa 5071 804}%
    \special{pa 5036 829}%
    \special{pa 5036 779}%
    \special{fp}%
    \special{pa 5071 893}%
    \special{pa 5250 893}%
    \special{pa 5250 714}%
    \special{pa 5071 714}%
    \special{pa 5071 893}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.804in
    \rlap{\kern 5.161in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 5250 804}%
    \special{pa 5429 804}%
    \special{dt 0.050}%
    \special{sh 1.000}%
    \special{pa 5393 779}%
    \special{pa 5429 804}%
    \special{pa 5393 829}%
    \special{pa 5393 779}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.625in
    \rlap{\kern 4.446in\lower\graphtemp\hbox to 0pt{\hss $t_1$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.625in
    \rlap{\kern 5.161in\lower\graphtemp\hbox to 0pt{\hss $t_2$\hss}}%
    \hbox{\vrule depth0.893in width0pt height 0pt}%
    \kern 5.429in
  }%
}%
 \centerline{\raise 1em\box\graph}
 \end{figure}\vspace{-2ex}

\begin{definition}{configuration} 
A {\em configuration} of a net is any finite multiset $X$ of transitions
with the property that the function $M_X:S \rightarrow \IZ$ given by
$M_X(s) = {M_0}(s) + \Sigma_{t\in T} X(t) \cdot (F(t,s)-F(s,t))$ is a
marking (i.e.\ $0 \leq M_X(s) \leq K(s)$ for all $s\in S$).  The
firing relation between markings is inherited by the configurations of
a net by $X \goto{U} X' \Leftrightarrow M_X \goto{U} M_X'$.

The {\em (labelled) configuration structure associated to net $N$} is
the tuple ${\cal C}(N)= (T_N,C_N,\goto{}_N,l_N)$, in which $C_N$
denotes the set of configurations of $N$.
\end{definition}
Note that if $M_X \goto{U} M'$ then $X \oplus U$ is a configuration
and $M'=M_{X\oplus U}$. It follows that the {\em reachable}
configurations can equivalently be defined as those multisets of
transitions $X$ for which there is a firing sequence
\plat{M_0 \goto{U_1} M_1 \goto{U_2} \cdots \goto{U_n} M_n} with
$X=\bigoplus_{i=1}^n U_i$.

Note too that the configuration structure associated to a net is not
a configuration structure in the sense of \df{labelled}. It is a
structure in a class that enriches set systems in two ways: first
by the use of multisets instead of sets, and second, by the
addition of the transition relation. Still we define:

\begin{definition}{configuration equivalence}
Two nets $N$ and $N'$ are {\em configuration equivalent} if
${\cal C}(N)={\cal C}(N')$.
\end{definition}
{\em Reachable configuration equivalence} is defined similarly and is
strictly coarser than (reachable) marking equivalence:
The nets P and Q are (reachable) configuration equivalent.
However M and N below are not.  The reason is that although in N all
transitions have a different identity, even though they have the same label.

Next we will determine which class of nets can be described by means of
set systems.

\begin{definition}{1-occurrence}
A {\em 1-occurrence net} is a net in which every configuration is a set.
\end{definition}
This implies that any transition can fire at most once.
Were we interested only in the reachable configurations we could
equivalently require that in every firing sequence
\plat{M_0 \goto{U_1} \cdots \goto{U_n} M_n}
the multisets $U_1,...,U_n$ are sets and disjoint.

In general the firing relation $\goto{}_N$ of a net $N$
is not determined by the set of configurations of $N$.
The nets S and T have a very different behaviour:
in S the actions $a$ and $b$ can be done in parallel, whereas in T
there is mutual exclusion.
\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.911in\lower\graphtemp\hbox to 0pt{\hss S:\hss}}%
    \special{pn 8}%
    \special{ar 1161 89 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 1.161in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1161 179}%
    \special{pa 1161 357}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1186 321}%
    \special{pa 1161 357}%
    \special{pa 1136 321}%
    \special{pa 1186 321}%
    \special{fp}%
    \special{pa 1071 536}%
    \special{pa 1250 536}%
    \special{pa 1250 357}%
    \special{pa 1071 357}%
    \special{pa 1071 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 1.161in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 1161 536}%
    \special{pa 1161 714}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1186 679}%
    \special{pa 1161 714}%
    \special{pa 1136 679}%
    \special{pa 1186 679}%
    \special{fp}%
    \special{ar 1161 804 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 1.018in\lower\graphtemp\hbox to 0pt{\hss $d$\hss}}%
    \special{ar 1518 89 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 1.518in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1518 179}%
    \special{pa 1518 357}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1543 321}%
    \special{pa 1518 357}%
    \special{pa 1493 321}%
    \special{pa 1543 321}%
    \special{fp}%
    \special{pa 1429 536}%
    \special{pa 1607 536}%
    \special{pa 1607 357}%
    \special{pa 1429 357}%
    \special{pa 1429 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 1.518in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pa 1518 536}%
    \special{pa 1518 714}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1543 679}%
    \special{pa 1518 714}%
    \special{pa 1493 679}%
    \special{pa 1543 679}%
    \special{fp}%
    \special{ar 1518 804 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 1.661in\lower\graphtemp\hbox to 0pt{\hss $e$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 1.982in\lower\graphtemp\hbox to 0pt{\hss T:\hss}}%
    \special{ar 2232 89 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 2.232in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 2232 179}%
    \special{pa 2232 357}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2257 321}%
    \special{pa 2232 357}%
    \special{pa 2207 321}%
    \special{pa 2257 321}%
    \special{fp}%
    \special{pa 2143 536}%
    \special{pa 2321 536}%
    \special{pa 2321 357}%
    \special{pa 2143 357}%
    \special{pa 2143 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 2.232in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{pa 2232 536}%
    \special{pa 2232 714}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2257 679}%
    \special{pa 2232 714}%
    \special{pa 2207 679}%
    \special{pa 2257 679}%
    \special{fp}%
    \special{ar 2232 804 89 89 0 6.28319}%
    \special{ar 2589 446 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 2.589in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 2.089in\lower\graphtemp\hbox to 0pt{\hss $d$\hss}}%
    \special{ar 2395 596 250 250 -1.869240 -1.018249}%
    \special{sh 1.000}%
    \special{pa 2509 343}%
    \special{pa 2526 383}%
    \special{pa 2483 386}%
    \special{pa 2509 343}%
    \special{fp}%
    \special{ar 2395 297 250 250 1.018249 1.869240}%
    \special{sh 1.000}%
    \special{pa 2348 570}%
    \special{pa 2321 536}%
    \special{pa 2363 522}%
    \special{pa 2348 570}%
    \special{fp}%
    \special{ar 2946 89 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.089in
    \rlap{\kern 2.946in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 2946 179}%
    \special{pa 2946 357}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2971 321}%
    \special{pa 2946 357}%
    \special{pa 2921 321}%
    \special{pa 2971 321}%
    \special{fp}%
    \special{pa 2857 536}%
    \special{pa 3036 536}%
    \special{pa 3036 357}%
    \special{pa 2857 357}%
    \special{pa 2857 536}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 2.946in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{pa 2946 536}%
    \special{pa 2946 714}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 2971 679}%
    \special{pa 2946 714}%
    \special{pa 2921 679}%
    \special{pa 2971 679}%
    \special{fp}%
    \special{ar 2946 804 89 89 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.446in
    \rlap{\kern 3.089in\lower\graphtemp\hbox to 0pt{\hss $e$\hss}}%
    \special{ar 2784 596 250 250 -2.123343 -1.272352}%
    \special{sh 1.000}%
    \special{pa 2696 386}%
    \special{pa 2652 383}%
    \special{pa 2670 343}%
    \special{pa 2696 386}%
    \special{fp}%
    \special{ar 2784 297 250 250 1.272352 2.123343}%
    \special{sh 1.000}%
    \special{pa 2816 522}%
    \special{pa 2857 536}%
    \special{pa 2830 570}%
    \special{pa 2816 522}%
    \special{fp}%
    \hbox{\vrule depth0.893in width0pt height 0pt}%
    \kern 3.089in
  }%
}%
\centerline{\raise 1em\box\graph}
\end{figure}
Yet their configurations are the same: S corresponds to the
configuration structure D of \ex{transitions}; T corresponds to a
similar structure, but without the diagonal $ab$. Therefore it is not
a good idea to equate a 1-occurrence net $N$ with the configuration
structure $(T_N,C_N,l_N)$.

\begin{definition}{loops}
A net $N$ is {\em pure} if there is no $s$ in $S_N$ and $t$ in $T_N$
with $F_N(s,t)>0$ and $F_N(t,s)>0$, i.e.\ if it is without {\em self-loops}.
\end{definition}

\begin{proposition}{loops}
In a pure net $N$ we have $X \goto{}_N Y$ iff $\forall Z (X
\subset Z \subset Y \Rightarrow Z\in C_N)$ for all 
$X,Y$ in $C_N$.
\end{proposition}
It follows that for pure nets the transition relation is completely
determined by the associated set of configurations. Thus
for every pure 1-occurrence net $N$, $\fC(N)$ is a set system.

As a consequence, all equivalence notions that are available for
configuration structures are available for pure 1-occurrence nets as well.
Two such nets are $x$-equivalent iff the associated configuration
structures are. One also has these equivalences for comparing such nets with
configuration or event structures.

Moreover, the equivalence notions of Section~\ref{computational}
generalise verbatim to configuration structures enriched with an
explicit step transition relation, and hence apply to arbitrary
1-occurrence nets.

Now we can ask whether any 1-occurrence net, possibly with self-loops,
is equivalent to a pure 1-occurrence net, or configuration structure.
The net T is 
history preserving bisimulation equivalent to a pure 1-occurrence net.
This does not hold in general:

\begin{figure}[htb]
%\input{3mutex}
\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 750 750 83 83 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.750in
    \rlap{\kern 0.750in\lower\graphtemp\hbox to 0pt{\hss $\bullet\bullet$\hss}}%
    \special{pa 667 500}%
    \special{pa 833 500}%
    \special{pa 833 333}%
    \special{pa 667 333}%
    \special{pa 667 500}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 0.417in
    \rlap{\kern 0.750in\lower\graphtemp\hbox to 0pt{\hss $a$\hss}}%
    \special{ar 908 566 250 250 2.619058 3.410024}%
    \special{sh 1.000}%
    \special{pa 632 532}%
    \special{pa 667 500}%
    \special{pa 680 545}%
    \special{pa 632 532}%
    \special{fp}%
    \special{ar 592 566 250 250 -0.268432 0.522535}%
    \special{sh 1.000}%
    \special{pa 851 669}%
    \special{pa 809 691}%
    \special{pa 807 644}%
    \special{pa 851 669}%
    \special{fp}%
    \special{ar 750 83 83 83 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 0.083in
    \rlap{\kern 0.750in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 750 167}%
    \special{pa 750 333}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 775 293}%
    \special{pa 750 333}%
    \special{pa 725 293}%
    \special{pa 775 293}%
    \special{fp}%
    \special{pa 1000 1167}%
    \special{pa 1167 1167}%
    \special{pa 1167 1000}%
    \special{pa 1000 1000}%
    \special{pa 1000 1167}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.083in
    \rlap{\kern 1.083in\lower\graphtemp\hbox to 0pt{\hss $b$\hss}}%
    \special{ar 833 1000 250 250 -1.570796 -0.000000}%
    \special{sh 1.000}%
    \special{pa 1108 960}%
    \special{pa 1083 1000}%
    \special{pa 1058 960}%
    \special{pa 1108 960}%
    \special{fp}%
    \special{ar 1017 834 250 250 1.637391 3.157143}%
    \special{sh 1.000}%
    \special{pa 741 870}%
    \special{pa 767 830}%
    \special{pa 791 870}%
    \special{pa 741 870}%
    \special{fp}%
    \special{ar 1417 1417 83 83 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 1.417in
    \rlap{\kern 1.417in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 1358 1358}%
    \special{pa 1167 1167}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 1177 1213}%
    \special{pa 1167 1167}%
    \special{pa 1213 1177}%
    \special{pa 1177 1213}%
    \special{fp}%
    \special{pa 333 1167}%
    \special{pa 500 1167}%
    \special{pa 500 1000}%
    \special{pa 333 1000}%
    \special{pa 333 1167}%
    \special{fp}%
    \graphtemp=.5ex\advance\graphtemp by 1.083in
    \rlap{\kern 0.417in\lower\graphtemp\hbox to 0pt{\hss $c$\hss}}%
    \special{ar 667 1000 250 250 -3.141593 -1.570796}%
    \special{sh 1.000}%
    \special{pa 627 725}%
    \special{pa 667 750}%
    \special{pa 627 775}%
    \special{pa 627 725}%
    \special{fp}%
    \special{ar 483 834 250 250 -0.015551 1.504201}%
    \special{sh 1.000}%
    \special{pa 542 1106}%
    \special{pa 500 1083}%
    \special{pa 538 1056}%
    \special{pa 542 1106}%
    \special{fp}%
    \special{ar 83 1417 83 83 0 6.28319}%
    \graphtemp=.5ex\advance\graphtemp by 1.417in
    \rlap{\kern 0.083in\lower\graphtemp\hbox to 0pt{\hss $\bullet$\hss}}%
    \special{pa 142 1358}%
    \special{pa 333 1167}%
    \special{fp}%
    \special{sh 1.000}%
    \special{pa 287 1177}%
    \special{pa 333 1167}%
    \special{pa 323 1213}%
    \special{pa 287 1177}%
    \special{fp}%
    \hbox{\vrule depth1.500in width0pt height 0pt}%
    \kern 1.500in
  }%
}%
\centerline{\raise 1em\box\graph}
\end{figure}

\begin{proposition}{unpure}
The 1-occurrence net above is not history preserving bisimulation
equivalent to a configuration structure.
However, every 1-occurrence net is ST-bisimulation equivalent to such a
structure. 
\end{proposition}

Below we show that the restriction to 1-occurrence nets is not very
crucial; every net can be ``unfolded'' into a 1-occurrence net
without changing its behaviour in any essential way. However, the
unfolding cannot be configuration equivalent to the original, as
the identity of transitions cannot be preserved.

\begin{definition}{1-unfolding}
Let $N=(S,T,F,K,M_0,l)$ be a Petri net. Its {\em 1-unfolding}
$N'=(S',T',F',K',M_0',l')$ into a 1-occurrence net is given by
(for $s \in S$, $t\in T$, $u\in T'$)
\begin{itemise}
\item $T'=T \times \IN$ and $l'((t,n))=l(t)$,
\item $S'=S \cup (T' \times \{*\})$,
\item $F'(s,(t,n))=F(s,t)$ and $F'((t,n),s)=F(t,s)$,
\item $F'(u,(u,*)) = F'((u,*),u') = F(u',(u,*)) = 0$ and
      $F'((u,*),u)=1$ for $u,u'\in T'$ with $u\neq u'$,
\item $K'(s)=K(s)$ and $K((u,*))=\infty$,
\item $M_0'(s)=M_0(s)$ and $M_0'((u,*))=1$.
\end{itemise}
\end{definition}
Thus, every transition is replaced by countably many copies, each of
which is connected with its environment (though the flow relation) in
exactly the same way as the original. Furthermore, for every such copy
$u$ an extra place $(u,*)$ is created, containing one initial token, and
having no incoming arcs and only one outgoing arc, going to $u$.
This place guarantees that $u$ can fire only once.
In any reachable marking of the unfolded net, one can see exactly which
transitions have fired, namely those transitions $u$ for which the
place $(u,*)$ is empty. Hence every such marking has only one configuration.

\begin{proposition}{1-unfolding}
Two nets are configuration equivalent iff their unfoldings are.
Moreover, for each of our equivalences $x$, two 1-occurrence nets are
$x$-equivalent iff their unfoldings are.
\end{proposition}
\pr{1-unfolding} shows we can define all our equivalences on
general nets.

\begin{definition}{eq. in general}
Two nets are said to be $x$-equivalent iff their unfoldings are.
\end{definition}
\pr{1-unfolding} guarantees that this definition is consistent with
the one we had already for 1-occurrence nets. Under this definition a
net is configuration preserving bisimulation equivalent with its
unfolding, although there is no {\em bijective} relation between the
configurations.  This is because a (trivial) element of choice is
introduced by the construction.

\begin{proposition}{unfolding}
Every net is configuration preserving as well as fully concurrent
bisimulation equivalent with its unfolding.
\end{proposition}
This tells us that the notion of unfolding preserves the behaviour of
nets under both the collective and the individual token interpretation.

It is possible however to give a slightly different interpretation of nets,
namely by excluding transitions from firing concurrently with themselves.%
\footnote{This distinction is independent of the individual--collective token
dichotomy, thus yielding four computational interpretations of nets.}
This amounts to simplifying \df{firing} by requiring $U$ to be a set
rather than a multiset. Under this interpretation our unfolding
could introduce concurrency that was not present before. However, for
this purpose \df{1-unfolding} can be adapted by removing the initial
tokens from the places $((t,n),*)$ for $t\in T$ and $n>0$ (but leaving
the token in $((t,0),*)$), and adding an arc from transition $(t,n)$
to place $((t,n+1),*)$ for every $t\in T$ and $n \in \IN$.
If both \df{firing} and \ref{df-1-unfolding} are adapted as indicated
above, Propositions \ref{pr-1-unfolding} and \ref{pr-unfolding} hold again.

Note that the construction in \df{1-unfolding} does not introduce
self-loops. Thus unfoldings of pure nets remain pure.
\begin{corollary}{net2conf}
For every Petri net there exists an ST-bisimulation equivalent
configuration structure. For every pure net there exists a configuration
preserving bisimulation equivalent configuration structure.
And for every pure 1-occurrence net $N$, $\fC(N)$ {\em is} a
configuration structure.
\end{corollary}
The configuration structure associated to a Petri net is always finitary
and rooted. The following shows that \cor{net2conf} has an an inverse:
every such configuration structure can be obtained as the image of a
pure 1-occurrence net.

\begin{theorem}{conf2net}
For every finitary rooted configuration structure there exists a
pure 1-occurrence net without capacities or arcweights with the same
configurations.
\end{theorem}

\begin{proof}
As transitions of the net we take the events of the configuration
structure. For every transition we add one place without incoming
arcs, and with its only outgoing arc going to that transition.
These places make sure that every transition fires only once.
Let $\Phi$ be an axiomatisation of the configuration structure
consisting of propositional sequents only. For every sequent $X
\Rightarrow Y$ with $X$ finite, 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 the configuration structure is rooted, $n \neq 0$. We finish
the construction by putting $n-1$ initial tokens in the created place.

The place belonging to sequent $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 places the same restriction on the occurrence of
events as the corresponding sequent. It follows that the constructed
net has exactly the same reachable configurations as the original
configuration structure. It even has the same unreachable ones.
\end{proof}
As a corollary we obtain that every pure net is configuration preserving
bisimulation equivalent to a net without capacities or arcweights.
Every pure 1-occurrence net is even configuration equivalent to a net
without capacities or arcweights.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\small
%\bibliography{/uf/rvg/lib/abbreviations,/uf/rvg/lib/dbase,/uf/rvg/lib/new}
\begin{thebibliography}{10}

\bibitem{BDKP91}
{\sc E.~Best, R.~Devillers, A.~Kiehn \& L.~Pomello} (1991):
\newblock {\em Concurrent bisimulations in {P}etri nets.}
\newblock {\sl Acta Informatica} 28, pp. 231--264.

\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-Verlag, pp. 62--95.

\bibitem{Ga81}
{\sc D.M. Gabbay} (1981):
\newblock {\em Semantic Investigations in {H}eyting's Intuitionistic Logic}, {\sl Synthese Library} 148.
\newblock D. Reidel.

\bibitem{vG95c}
{\sc R.J.~van Glabbeek} (1995):
\newblock {\em History preserving process graphs.}
\newblock Report, Stanford University, Available at\\ {\footnotesize \tt ftp://boole.stanford.edu/pub/DVI/history.dvi.gz}.

\bibitem{GG89ea}
{\sc R.J.~van Glabbeek \& U.~Goltz} (1989):
\newblock {\em Equivalence notions for concurrent systems and refinement of actions.}
\newblock In A.~Kreczmar \& G.~Mirkowska, editors: {\sl {\rm Proceedings $14^{th}$ Symposium on} Mathematical Foundations of Computer Science, {\rm Por{\pa}bka-Kozubnik, Poland 1989}}, {\sl \rm LNCS} 379, Springer-Verlag, pp. 237--248.

\bibitem{GG90}
{\sc R.J.~van Glabbeek \& U.~Goltz} (1990):
\newblock {\em Refinement of actions in causality based models.}
\newblock In J.W. de~Bakker, W.P.~de Roever \& G.~Rozenberg, editors: {\sl Proceedings REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, {\rm Mook, The Netherlands, May/June 1989}}, {\sl \rm LNCS} 430, Springer-Verlag, pp. 267--300.

\bibitem{GV87}
{\sc R.J.~van Glabbeek \& F.W. Vaandrager} (1987):
\newblock {\em Petri net models for algebraic theories of concurrency.}
\newblock In J.W.~de Bakker, A.J. Nijman \& P.C. Treleaven, editors: {\sl Proceedings PARLE conference, {\rm Eindhoven}, Vol. II (Parallel Languages)}, {\sl \rm LNCS} 259, Springer-Verlag, pp. 224--242.

\bibitem{GR83}
{\sc U.~Goltz \& W.~Reisig} (1983):
\newblock {\em The non-sequential behaviour of {Petri} nets.}
\newblock {\sl Information and Computation} 57, pp. 125--147.

\bibitem{Gun92b}
{\sc J.~Gunawardena} (1992):
\newblock {\em Causal automata.}
\newblock {\sl Theoretical Computer Science} 101, pp. 265--288.

\bibitem{Gup94}
{\sc V.~Gupta} (1994):
\newblock {\em Chu Spaces: A Model of Concurrency}.
\newblock PhD thesis, Stanford University.
\newblock Available at {\tt ftp://boole.stanford.edu/pub/gupthes.ps.gz}.

\bibitem{GP93}
{\sc V.~Gupta \& V.R. Pratt} (1993):
\newblock {\em Gates accept concurrent behavior.}
\newblock In {\sl Proc. 34th Ann. IEEE Symp. on Foundations of Comp. Sci.}, pp. 62--71.

\bibitem{Lk92}
{\sc R.~Langerak} (1992):
\newblock {\em Transformations and Semantics for LOTOS}.
\newblock PhD thesis, Department of Computer Science, University of Twente.

\bibitem{LW91}
{\sc K.G. Larsen \& G.~Winskel} (1991):
\newblock {\em Using information systems to solve recursive domain equations.}
\newblock {\sl Information and Computation} 91(2), pp. 232--258.

\bibitem{MMS92}
{\sc J.~Meseguer, U.~Montanari \& V.~Sassone} (1992):
\newblock {\em On the semantics of {Petri} nets.}
\newblock In W.R. Cleaveland, editor: {\sl Proceedings CONCUR 92, {\rm Stony Brook, NY, USA}}, {\sl \rm LNCS} 630, Springer-Verlag, pp. 286--301.

\bibitem{Mi80}
{\sc R.~Milner} (1980):
\newblock {\em A Calculus of Communicating Systems}, {\sl \rm LNCS} 92.
\newblock Springer-Verlag.

\bibitem{NPW81}
{\sc M.~Nielsen, G.D. Plotkin \& G.~Winskel} (1981):
\newblock {\em Petri nets, event structures and domains, part {I}.}
\newblock {\sl Theoretical Computer Science} 13(1), pp. 85--108.

\bibitem{PP95}
{\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{PP}
{\sc G.D. Plotkin \& V.R. Pratt} (1988):
\newblock {\em Teams can see pomsets.}
\newblock Manuscript available at\\ {\tt ftp://boole.stanford.edu/pub/DVI/pp2.dvi.gz}.

\bibitem{Pr91a}
{\sc V.R. Pratt} (1991):
\newblock {\em Modeling concurrency with geometry.}
\newblock In {\sl Proc. 18th Ann. ACM Symposium on Principles of Programming Languages}, pp. 311--322.

\bibitem{Pr94a}
{\sc V.R. Pratt} (1994):
\newblock {\em Chu spaces: complementarity and uncertainty in rational mechanics.}
\newblock Tech. report, TEMPUS Summer School, Budapest.
\newblock Available at {\tt ftp://boole.stanford.edu/pub/DVI/bud.dvi.gz}.

\bibitem{Sc74}
{\sc D.S. Scott} (1974):
\newblock {\em Completeness and axiomatizability in many-valued logic.}
\newblock In L.~Henkin et~al., editors: {\sl Proc. Tarski Symposium}, AMS, pp. 411--435.

\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-Verlag, 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-Verlag, pp. 364--397.

\end{thebibliography}
\end{document}
