\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 $e0$ 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}