\documentclass[runningheads]{llncs}
\bibliographystyle{plain}
\unitlength 1mm
\spnewtheorem{observation}{Observation}{\bfseries}{}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%                            References                                %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\thm}[1]{Theorem~\ref{thm-#1}}
\newcommand{\pr}[1]{Prop.~\ref{pr-#1}}
\newcommand{\cor}[1]{Cor.~\ref{cor-#1}}
\newcommand{\df}[1]{Def.~\ref{df-#1}}
\newcommand{\ex}[1]{Example~\ref{ex-#1}}
\newcommand{\fig}[1]{Fig.~\ref{fig-#1}}
\newcommand{\sect}[1]{Sect.~\ref{sec-#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}   % no vertical space
\newcommand{\goto}[1]{\stackrel{#1}{\longrightarrow}}	% transition
\newcommand{\pre}[1]{\mbox{$^\bullet #1$}}	        % preplaces
\newcommand{\rest}{					% restriction operator
        \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} }
\newfont{\fsc}{eusm10}                                  % frenchscript letters
\newcommand{\multi}{\mbox{\fsc M}}                      % french M (multisets)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%				Abbreviations			          %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\bbbn}		            	        % natural numbers
\newcommand{\eA}{{\rm A}} 			        % LSTS
\newcommand{\eB}{{\rm B}}			        % LSTS
\newcommand{\eN}{{\rm N}}			        % Petri net
\newcommand{\eP}{{\rm P}}			        % Petri net
\newcommand{\eQ}{{\rm Q}}			        % Petri net
\newcommand{\CT}{\mathcal{H}_{\rm CT}}    % collective token interpretation
\newcommand{\IT}{\mathcal{H}_{\rm IT}}    % individual token interpretation
\newcommand{\ssCT}{\mathcal{H}_{\rm CT}^{ss}}  % self-seq CT interpretation
\newcommand{\ssIT}{\mathcal{H}_{\rm IT}^{ss}}  % self-seq IT interpretation

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{The Individual and Collective Token Interpretations of Petri Nets}
\author{Rob van Glabbeek}
\institute{National ICT Australia\\
and School of Computer Science and Engineering\\
The University of New South Wales\\
\email{rvg@cs.stanford.edu}}
\begin{document}
\maketitle

\begin{abstract}
Starting from the opinion that the standard firing rule of Petri nets
embodies the collective token interpretation of nets rather than their
individual token interpretation, I propose a new firing rule that
embodies the latter. Also variants of both firing rules for the
self-sequential interpretation of nets are studied. Using these rules,
I express the four computational interpretations of Petri nets by
semantic mappings from nets to labelled step transition systems, the
latter being event-oriented representations of higher dimensional
automata.  This paper totally orders the expressive power of the four
interpretations, measured in terms of the classes of labelled step
transition systems up to isomorphism of reachable parts that can be
denoted by nets under each of the interpretations.  Furthermore, I
extend the unfolding construction of place/transition nets into
occurrence net to nets that may have transitions without incoming
arcs.
\end{abstract}

\section*{Introduction}

In the literature on Petri nets $2\times 2 = 4$ computational
interpretations of nets can be distinguished, that in {\sc Van
Glabbeek \& Plotkin} \cite{GP95} were called the \emph{individual
token} and the \emph{collective token} interpretation, and,
orthogonally, the \emph{self-sequential} and the
\emph{self-concurrent} interpretation. The differences show up only
when dealing with non-safe place/transition nets and, as far as the
individual/collective token dichotomy concerns, only when precisely
keeping track of causal dependencies between action occurrences.

The individual token interpretation has been formalised by the notion
of a \emph{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 fully concurrent bisimulation.  {\sc Engelfriet}
\cite{En91} and {\sc Meseguer {\it et al.}} \cite{MMS97} define an
unfolding of Petri nets into occurrence nets that preserves this
interpretation. {\sc Best \& Devillers} \cite{BD87} adapted the
process concept of \cite{GR83} to fit the collective token philosophy.
Equivalence relations on Petri nets based on the collective token
interpretation were proposed in \cite{GP95}.

In older papers on Petri nets a multiset of transitions was allowed to
fire only if it was a set, i.e., no transition could fire multiple
times concurrent with itself. The argument for this restriction was
that a transition can be thought of as a subsystem like a printer,
that can only print one file at a time. When there are enough tokens
in its preplaces (representing print-requests and other preconditions
for printing) to handle two files, these have to be printed one by
one.\linebreak {\sc Goltz \& Reisig} \cite{GR83} exemplified that not
all subsystems suffer from such limitations; when one does, this is a
matter of scarcity of recourses that can be modelled by an extra
place. Since \cite{GR83} multisets are generally allowed to fire.
Nevertheless, for the sake of completeness, I take both
interpretations into account.

The present work can be understood as a way of formally pinpointing
the differences between these computational interpretations.  This is
done by formulating four different firing rules, and by giving four
translations from Petri nets into labelled step transition systems,
one for each interpretation. \emph{Labelled step transition systems}
arose from discussions with Vaughan Pratt in 1991 as an event-oriented
representation of \emph{higher dimensional automata} \cite{Pr91a}, an
angle that will not be pursued here. Step transition systems were used
to describe the operational behaviour of Petri nets in {\sc Mukund}
\cite{Mu92}. In the form proposed here, but without the labelling,
they appear in {\sc Badouel} \cite{Ba96}.

I compare the expressive power of classes of Petri nets under each of
the four interpretations in terms of the labelled step transition
systems they can denote up to isomorphism of reachable parts, and find
that the class of all Petri nets under either one of the individual
token interpretations is equally expressive as a subclass of nets on
which all four interpretations coincide. Likewise, the class of all
Petri nets under the self-concurrent collective token interpretation
is equally expressive as a subclass of nets on which both collective
token interpretations coincide. This gives rise to the following
hierarchy:

\begin{figure}[ht]
\unitlength .64mm
\begin{center}
\begin{picture}(0,45)(0,-14)
\put(0,-12){\makebox[0pt]{\textit{self-sequential individual token interpretation}}}
\put(0,-3.5){\vector(0,-1){5}}
\put(0,-6.5){\vector(0,1){5}}
\put(0,0){\makebox[0pt]{\textit{self-concurrent individual token interpretation}}}
\put(0,3.5){\vector(0,1){10}}
\put(0,15){\makebox[0pt]{\textit{self-sequential collective token interpretation}}}
\put(0,18.5){\vector(0,1){10}}
\put(0,30){\makebox[0pt]{\textit{self-concurrent collective token interpretation}}}
\end{picture}
\caption{Relative expressiveness of four computational
  interpretations of Petri nets}
\label{fig-computational hierarchy}
\end{center}\vspace{-1.5em}\end{figure}

\noindent
The expressiveness results above were first claimed by me in
\cite{vG05}, using a different model of higher dimensional automata
for interpreting the dynamic behaviour of Petri nets, namely
\emph{cubical sets} instead of labelled step transition systems.
However, the individual token interpretations of \cite{vG05} apply to
\emph{standard nets} only, nets in which each transition has at least
one incoming arc, and a proof is given for the expressiveness result
relating the two self-concurrent interpretations only.

As a spin-off, this study provides a particularly simple definition of
the unfolding of an arbitrary place/transition net into an occurrence
net.  My construction extends the constructions of \cite{Wi87a},
\cite{En91} and \cite{MMS97} by including non-standard nets.

\section{Petri Nets and the Firing Rule}\label{sec-Petri}

\begin{definition}\rm\label{petri}
A (labelled, marked) {\em Petri net} is a tuple $(S,T,F,I,l)$ with
\begin{itemize}\vspace{-1ex}
\item $S$ and $T$ two disjoint sets of {\em places} ({\em Stellen} in German)
and {\em transitions},
\item $F: (S \times T \cup T\times S)\rightarrow \IN$,
the {\em flow relation},
\item $I:S \rightarrow \IN$, the {\em initial marking},
\item and $l: T \rightarrow A$, for $A$ a set of
\emph{actions}, the {\em labelling function}.
\end{itemize}\vspace{-2ex}
\end{definition}

\noindent
Petri nets are pictured by drawing the places as circles and the
transitions as boxes, containing their label. For
$x,\hspace{-.5pt}y\!\in\! S\hspace{-1.4pt}\cup\hspace{-1.4pt} T$ there
are $F(\hspace{-.5pt}s,t)$ {\em arcs} from $x$ to $y$.
When a Petri net represents a concurrent system, a global state of
this system is given as a \emph{marking}, a function $M:S\rightarrow\IN$.
Such a state is depicted by placing $M(s)$ dots (\emph{tokens}) in
each place $s$. The initial state is given by the marking $I$.\linebreak[2]
In order to describe the behaviour of a net, one defines the \emph{step
transition relation} between markings.

\begin{definition}\rm\label{df-multiset}
A {\em multiset} over a set $S$ is a function $M\!:S \rightarrow \IN$,
i.e.\ $M\in \IN^S$.
For multisets $M$ and $N$ over $S$ write $M \leq N$ if $M(s) \leq
N(s)$ for all $s \in S$. $M+N \in \IN^S$ is the multiset with
$(M+N)(s)=M(s)+N(s)$, and $M-N$ is the function given by
$(M-N)(s)=M(s)-N(s)$---it is not always a multiset.
The function $0\!:S\rightarrow\IN$ given by $0(s)=0$ for all $s \in S$
is the \emph{empty} multiset.
A multiset $M \in \IN^S$ with $M(s) \leq 1$ for all $s\!\in\!S$ is
identified with the set $\{s \in S \mid M(s)=1\}$.  A multiset $M$
over $S$ is \emph{finite} if $\{s \in S \mid M(s)>0\}$ is finite.
Let $\multi(S)$ denote the collection of finite multisets over $S$.
\end{definition}

\begin{definition}\rm\label{df-firing}
For a finite multiset $U:T \rightarrow \IN$ of transitions in a Petri net, let
$^\bullet U,~ U^\bullet: S \rightarrow \IN$ be the multisets of
\emph{input} and \emph{output places} of $U$, given by
$$^\bullet U(s)=\sum_{t\in T} F(s,t) \cdot U(t)~~\mbox{and}~~
U^\bullet (s)=\sum_{t\in T} U(t) \cdot F(t,s)~~\mbox{for all}~s \in S.$$
$U$ is \emph{enabled} under a marking $M$ if $^\bullet U \leq M$.
In that case $U$ can \emph{fire} under $M$, yielding the marking
$M'=M - \mbox{$^\bullet U$} + U^\bullet$, written \plat{M\goto{U}M'}.
\end{definition}
If a multiset $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 preplaces of $U$ (the places where the incoming arcs
come from). 

The components of a net $\eN$ are called $S^\eN$, $T^\eN$, $F^\eN$,
$I^\eN$ and $l^\eN$, a convention that also applies to other
structures given as tuples. When clear from context, the index $\eN$
is omitted.

Two nets P and Q are \emph{isomorphic}, written $P\cong Q$, if they
differ only in the names of their places and transitions, i.e.\ if
there are bijections $\beta\!:S^\eP \rightarrow S^\eQ$ and $\eta\!:T^\eP
\rightarrow T^\eQ$ such that, for $s\!\in\! S^\eP$ and $t\!\in\!T^\eP$:
~~$I^\eQ(\beta(s))=I^\eP(s)$, ~~$F^\eQ(\beta(s),\eta(t))=F^\eP(s,t)$,
~~$F^\eQ(\eta(t),\beta(s))=F^\eP(t,s)$~~ and ~~$l^\eQ(\eta(t))=l^\eP(t)$.

\section{The Individual and Collective Token Interpretations}
\label{sec-interpretations}

In the \emph{individual token interpretation} of Petri nets one
distinguishes different tokens residing in the same place, keeping
track of where they come from. If a transition fires by using a token
that has been produced by another transition, there is a causal link
between the two.  Consequently, the causal relations between the
transitions in a run of a net can always be described by means of a
partial order. In the \emph{collective token interpretation}, on the
other hand, tokens cannot be distinguished: if there are two tokens in
a place, all that is present there is the number 2. This gives rise to
more subtle causal relationships between transitions in a run of a
net, which cannot be expressed by partial orders.

The following example illustrates the difference between the two
interpretations.

\begin{figure}[htp]
\input{tokens}
\vspace{-2em}
\centerline{\raise 1em\box\graph}
\vspace{-1em}
\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 executions, that can be characterised by the partial orders
\plat{\begin{array}{@{}c@{}}~~a\\[-4pt]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 following illustrates that both philosophies yield
incomparable notions of equivalence.

\begin{figure}[htb]
\vspace{-2em}
\input{incomparable}
\centerline{\raise 1em\box\graph}
\vspace{-1em}
\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\@.
However, A and B are not \emph{fully concurrent bisimulation equivalent}
(a causality respecting equivalence based on the individual token
approach \cite{BDKP91}), as B lacks the execution
\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]
\vspace{-2em}
\input{netC}
\centerline{\raise 1em\box\graph}
\vspace{-1.5em}
\end{figure}

\noindent
In fact, C is the occurrence net obtained from A by the unfolding of
\cite{En91,MMS97}.  In the individual token philosophy, both A and C
have the executions
\begin{picture}(11,0)
\put(0,0){$a$}
\put(3,1){\vector(1,0){5}}
\put(9,0){$b$}
\end{picture}
and \plat{\begin{array}{@{}c@{}}a~~\\[-5pt]~~b\end{array}}.
However, in the collective token philosophy 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}
and can therefore not be equivalent to C in any causality preserving way.

\begin{figure}[htp]
\input{disjunctive}
\centerline{\raise 1em\box\graph}
\vspace{-1.3em}
\end{figure}
The Petri net D above (ignore $\CT({\rm D})$ and $\IT({\rm D})$ for
now) illustrates how the collective token interpretation gives rise to
causal relationships that cannot be expressed by partial orders. Under
the collective token interpretation this net features {\em disjunctive
causality}\/: $c$ is causally dependent on $a\vee b$.  In contrast,
under the individual token interpretation D admits two executions, one
in which $c$ depends only on $a$, and one in which $c$ depends only on
$b$.

Antoni Mazurkiewicz once argued for the collective reading of this net
by letting $a$ and $b$ be $\pounds 1$ contributions of two school
children to buy a present for their teacher. The act of buying the
present, which only costs $\pounds 1$, is represented by $c$.  Now the
individual token interpretation suggests that the present is bought
from the contribution from either one child or the other, whereas the
collective token interpretation admits only one complete execution, in
which the buying of the present is caused by the disjunction of the
two contributions. The latter would be a fairer description of the
intended state of affairs.

\section{A Firing Rule for the Individual Token Interpretation}
\label{sec-individual}

In my opinion, the standard definition of a marking and the
corresponding firing rule (\df{firing}) embody the collective token
interpretation rather than the individual one.  Here I will redefine
these concepts in a way that embodies the individual token
interpretation. To this end I define the notion of a token as it could
occur in a Petri net, in such a way that all possible token
occurrences have a different name.  A token will be a triple
$(t',k,s)$, with $s$ the place where the token occurs, and $t'$ the
transition firing that brought it there.  For tokens that are in $s$
initially, I take $t'=*$. When the number of tokens that $t'$ deposits
in $s$ in $n$, I distinguish these tokens by giving them ordinal
numbers $k=0,1,2,\ldots,n\!-\!1$.  In order to define tokens as
announced above I need to define transition firings simultaneously.
These will be pairs $(X,t)$ with $t$ the transition that fires, and
$X$ the set of tokens that is consumed in the firing. Transitions $t$
that can fire without consuming tokens can fire multiple times on the
same (empty) input; these firings will be called $(k,t)$ with $k\in
\IN$ instead of $(\emptyset,t)$.  I define the functions $\beta$ from
tokens to the places where they occur by $\beta(x,k,s)=s$, and $\eta$
from transition firings to the transition that fires by
$\eta(x,t)=t$. The function $\beta$ extends to a function from sets of
tokens $X$ to multisets of places $\beta(X):S\rightarrow \IN$, by
$\beta(X)(s)=|\{s'\in X\mid \beta(s')=s\}|$.

\begin{definition}\rm\label{df-tokens}
Given a Petri net $\eN=(S,T,F,I,l)$, the sets of \emph{tokens} $S_\bullet$
and \emph{transition firings} $T_\bullet$ of $\eN$ are recursively defined by
\begin{itemize}\vspace{-1ex}
\item $(*,k,s)\in S_\bullet$ for $s\in S$ and $k<I(s)$;
\item $(t',k,s)\in S_\bullet$ for $s\in S$, $t'\in T_\bullet$ and $k<F(\eta(t'),s)$;
\item $(X,t)\in T_\bullet$ for $t\in T$ and $X \subseteq S_\bullet$ such that
      $\beta(X)=\,^\bullet t \neq 0$;
\item $(k,t)\in T_\bullet$ for $k\in\IN$ and $t\in T$ such that
      $^\bullet t=0$.
\end{itemize}
The labelling function $l_\bullet\!:T_\bullet \rightarrow A$ on
transition firings is given by $l_\bullet(t)=l(\eta(t))$.  An
\emph{individual marking} of $\eN$ is a multiset
$M\!:S_\bullet\rightarrow\IN$ of tokens.  The \emph{initial} individual
marking $I_\bullet\!:S_\bullet\rightarrow\IN$ is given by
$I_\bullet(*,k,s)=1$ and $I_\bullet(t',k,s)=0$.
\end{definition}

\subsubsection{Standard Nets.}

A {\em standard net} is a net N in which each transition has at least
one incoming arc: $\forall t \in T.~\pre{t}>0$.  A net is standard iff
its set of \emph{spontaneous transition firings} $T_\circ=\{(k,t)\in
T_\bullet\mid k\!\in\!\IN\}$ is empty. I define the firing rule
embodying the individual token interpretation for standard nets first.

\begin{definition}\rm\label{df-firing individual}
For a finite set $U\subseteq T_\bullet$ of transition firings in a
standard net, let $$^\bullet U=\!\!\! \sum_{(X,t)\in U}\!\!\! X
~~\mbox{and}~~U^\bullet=\{(t',k,s)\mid t'\in U\wedge
k<F(\eta(t'),s)\}$$ be the multiset of \emph{input tokens} and the set
of \emph{output tokens} of $U$.  The set $U$ is \emph{enabled} under
an individual marking $M\!\in\IN^{S_\bullet}$ if $^\bullet U \leq M$.
In that case $U$ can \emph{fire} under $M$, yielding $M'=M -
\mbox{$^\bullet U$} + U^\bullet \in\IN^{S_\bullet}$, written
\plat{M\goto{U}_\bullet M'}.  \\ A chain $I_\bullet \goto{U_1}_\bullet
M_1 \goto{U_2}_\bullet \cdots \goto{U_n}_\bullet M_n$ is called a {\em
firing sequence}.  An individual marking $M\!\in\IN^{S_\bullet}$ is
{\em reachable} if there is such a sequence ending in $M=M_n$.
\end{definition}
The following proposition says that I succeeded in giving all possible
token occurrences a different name.

\begin{proposition}\label{pr-set}
In a standard net, any reachable multiset of tokens is a set.
\end{proposition}

\begin{proof}
I show that in a firing sequence $I_\bullet \goto{U_1}_\bullet M_1
\goto{U_2}_\bullet \cdots \goto{U_n}_\bullet M_n$ the multiset
$I_\bullet+\sum_{i=1}^n U_i^\bullet$, which includes $M_n$, is a
set. Applying induction on $n$, the base case holds by the definition
of $I_\bullet$. For the induction step, if a token occurs twice in
$I_\bullet+\sum_{i=1}^n U_i^\bullet$, the definitions of $I_\bullet$
and $U^\bullet$ imply that it has the form $(t',k,s)$, hence the
transition firing $t'$ occurs twice in $\sum_{i=1}^n U_i$.
As $t'$ is not spontaneous, it has the form $(X,t)$ with $X$ a
nonempty set of tokens. By the definition of $^\bullet U$, a token in
$X$ occurs twice in $I_\bullet+\sum_{i=1}^{n-1} U_i^\bullet$.\qed
\end{proof}
\pr{set} also shows that there is no point in upgrading
\df{firing individual} to \emph{multi}sets $U$.

\subsubsection{Non-standard Nets.}

For arbitrary nets, the definition of $U^\bullet$, for $U$ a finite
set of transitions, remains the same, but in the definition of
$^\bullet U$ one needs to decide on the input conditions of
spontaneous transition firings. The simplest solution would be to
treat $k$ as $\emptyset$ in the definition of $^\bullet U$ or,
equivalently, to let the sum range over the non-spontaneous transition
firings in $U$ only. However, this would lead to a failure of \pr{set}
for non-standard nets, as a spontaneous transition firing $(k,t)$
could occur multiple times in a firing sequence, leaving multiple
copies of its output tokens in the resulting reachable marking.  A
solution for this problem would be to upgrade the definition of a
firing sequence with the requirement that each spontaneous transition
firing may only occur once in it. This condition would be motivated by
the idea that every time a transition $t$ with $^\bullet t=0$ fires,
its firing gets a different identifier.

Here I aim at the same result by using a notion of state that consists
of an individual marking, together with the set names of spontaneous
transition firings that may still fire. I could just as well have
taken the set of spontaneous transition firings that have already
occurred, this set being equally rich in information content, but the
choice above allows me to combine both components of a state into one
set of resources that need to be available for transition firings to occur.

\begin{definition}\rm\label{df-resources}
Let N be a Petri net. Let $S_\bullet^+ = S_\bullet \cup \{t_k \mid
(k,t)\!\in\!T_\circ\}$ be the set of \emph{resources} of $\eN$.  An
\emph{individual state} $M\in \IN^{S_\bullet^+}$ of N is the union of
an individual marking and a multiset of names \plat{t_k} of
spontaneous transition firings $(k,t)$. The \emph{initial state}
$I_\bullet^+=\{(*,k,s)\mid k<I(s)\} \cup \{t_k \mid
(k,t)\!\in\!T_\circ\}$ is the union of $I_\bullet$ and the set of names
of all spontaneous transition firings.  The multiset of \emph{input
resources} of a finite set of transition firings $U\subseteq T_\bullet$
is given by $$^\bullet U=\!\!\!\!\!\!\!  \sum_{(X,t)\in U-T_\circ}
\!\!\!\!\!\!\! X + \{t_k \mid (k,t)\in U\cap T_\circ\}.$$
All other elements of \df{firing individual} apply unchanged, but
using individual states instead of individual markings, and
$I_\bullet^+$ instead of $I_\bullet$.
\end{definition}
\begin{corollary}\label{cor-set}
In any Petri net, all reachable individual states are sets.
\end{corollary}

\section{The Individual and Collective Firing Rules Agree}

Having defined a new firing rule that caters to the individual token
interpretation, I now show how it is consistent with the standard
firing rule of Definition~\ref{df-firing}. I use variables $M_\bullet$
to range over individual states, and $U_\bullet$ to range over sets of
transition firings.  The function $\eta$ from transition firings to
the transition that fires extends to a function from sets of
transition firings $U_\bullet$ to multisets of transitions
$\eta(U_\bullet):T\rightarrow \IN$, by $\eta(U_\bullet)(t)=|\{t'\in
U_\bullet \mid \eta(t')=t\}|$. Moreover, the function $\beta$ from
tokens to the places where they occur extends to a function from
individual states (multisets of resources) to markings (multisets of
places) by $\beta(M_\bullet)(s)=\sum_{s'\in\beta^{-1}(s)}M_\bullet(s')$
(where non-token resources are ignored).

Now the following theorem, whose proof is trivial, says that the
functions $\beta$ and $\eta$ constitute a \emph{bisimulation} between
the step transition relations of a given net under the individual and
collective token interpretations.
\begin{theorem}
$\beta(I_\bullet^+)=I$ and for any individual states $M_\bullet$ and
  markings $M'$:\vspace{-1ex}
$$\beta(M_\bullet)\goto{U}M' \Leftrightarrow \exists U_\bullet,
M'_\bullet: M_\bullet \goto{U_\bullet}_\bullet M'_\bullet \wedge
\eta(U_\bullet)=U \wedge \beta(M'_\bullet)=M'.$$
\end{theorem}

\section{Firing Rules for the Self-sequential Interpretations}
\label{sec-self-sequential}

The firing rules of Sections~\ref{sec-Petri} and~\ref{sec-individual}
embody the \emph{self-concurrent} interpretations of Petri nets,
allowing a transition to fire concurrently with itself. Here I
investigate how they need to be adapted to obtain firing rules for the
\emph{self-sequential} interpretations, excluding transitions from
firing concurrently with themselves.

The firing rule for the self-sequential collective token
interpretation is evident: a multiset $U$ of transitions is
\emph{enabled} under the self-sequential interpretation of nets if it
is enabled in the sense of \df{firing} and $U$ is a set.  The
\emph{self-sequential step transition relation} $\rightarrow^{ss}$
between markings is given by $M \plat{\goto{U}}^{ss} M'$ iff $M
\goto{U} M'$ and $U$ is a set.

On standard nets, a firing rule for the self-sequential individual
token interpretation can be obtained in the same way: a
multiset $U$ of transition firings is \emph{enabled} under the
self-sequential interpretation of nets if it is enabled in the sense
of \df{firing individual} and $U$ is a set with the property that if
$(X,t),(Y,t)\in U$ for $t\in T$ then $X=Y$. Thus, all transition
firings in $U$ should be firings of different transitions. One defines
$\rightarrow_\bullet^{ss}$ by imposing the same requirement.

On non-standard nets, before employing the same definitions, I take
the opportunity to rectify an unfortunate design decision that was
unavoidable under the self-concurrent interpretation.  Namely, if a
net contains a transition $t$ without input places, \df{resources}
yields an infinitely branching transition relation: there is a
transition
$I_\bullet\stackrel{\{(k,t)\}}{-\!\!-\!\!\!\longrightarrow}_\bullet
M_{(k,t)}$ for any $k\in \IN$. The reason this was unavoidable under
the self-concurrent interpretation is that any number of transition
firings $(k,t)$ can happen simultaneously, and I want to preserve the
fundamental property of Petri nets that whenever a number of
transition firings can happen in one step, they can happen in any
order; so any of the firings $(k,t)$ can happen first.  Under the
self-sequential interpretation, on the other hand, it is much more
natural so take the point of view that although the transition $t$
allows arbitrary many firings to occur sequentially, there is no point
in distinguishing different kinds of first firings. Thus, I will use
$k$ not merely as a label taken from an arbitrary countable set, but
as an actual number, $(k,t)$ denoting the $k\!+\!1^{th}$ firing of
transition $t$. The set $S_\bullet^+$ of resources of a net and the
individual states \plat{M\in\IN^{S_\bullet^+}} are as in \df{resources},
but this time the presence of $t_k$ in a state signifies that the
$k\!+\!1^{th}$ firing of $t$ is enabled. The multiset of input resources
remains the same as in \df{resources}, but the notions of initial
state and output resources need to be adapted.

\begin{definition}\rm\label{df-firing ss}
Let $\eN$ be a Petri net. The \emph{initial state} of $\eN$ under the
self-sequential interpretation is $I_\bullet^{ss}=\{(*,k,s)\mid k<I(s)\}
\cup \{t_0 \mid t\!\in\!T \wedge ^\bullet t =0\}$,
and the set of \emph{output resources} of a finite set of transition
firings $U\subseteq T_\bullet$ is
$$U^\bullet_{ss}=\{(t',k,s)\mid t'\in U\wedge k<F(\eta(t'),s)\} \cup
\{t_{k+1}\mid (k,t)\in U\cap T_\circ\}.$$ The set $U$ is
\emph{enabled} in an individual state $M\!:S_\bullet^+ \rightarrow\IN$
under the self-sequential interpretation if $^\bullet U \leq M$ and
$\forall t ((x,t),(y,t)\!\in\!U \Rightarrow x=y)$.  In that case $U$ can
\emph{fire} under $M$, yielding the state $M'=M - \mbox{$^\bullet U$} +
U^\bullet_{ss}$, written $\plat{M\goto{U}}_\bullet^{ss} M'$.
\end{definition}
Again, it is trivial to check that all
$\rightarrow_\bullet^{ss}$-reachable individual states are sets, and
$\beta$ and $\eta$ constitute a bisimulation between the step
transition relations of a net under the self-sequential individual and
collective token interpretations.
\begin{theorem}
$\beta(I_\bullet^{ss})=I$ and for any individual states $M_\bullet$ and
  markings $M'$:\vspace{-1pt}
$$\beta(M_\bullet)\plat{\goto{U}}^{ss}M' \Leftrightarrow \exists U_\bullet,
M'_\bullet: M_\bullet \plat{\goto{U_\bullet}}^{ss}_\bullet M'_\bullet \wedge
\eta(U_\bullet)=U \wedge \beta(M'_\bullet)=M'.$$
\end{theorem}

\section{Labelled Step Transition Systems}\label{sec-LSTS}

\begin{definition}\rm\label{df-LSTS}
A \emph{labelled step transition system} is a tuple
$(Q,E,\rightarrow,I,l)$ with
\begin{itemize}\vspace{-1ex}
\item $Q$ and $E$ are two disjoint sets of \emph{states} and
  \emph{events},
\item $\rightarrow\; \subseteq Q \times \multi(E) \times Q$, the
  \emph{step transition relation}, satisfying
\begin{center}
\begin{tabular}{l@{~~}l@{~~}l@{}}
  (1)&if $(p,u,q),(p,u,q')\in\;\rightarrow$ then $q=q'$&(determinism)\\
  (2)&$(p,0,p)\in\;\rightarrow$                        & (trivial step)\\
  (3)&if $(p,u+v,r) \in\;\rightarrow$ then
        $\exists q: (p,u,q), (q,v,r) \in\;\rightarrow$ & (asynchronousness)\\
\end{tabular}
\end{center}
\item $I\in Q$, the \emph{initial state},
\item and $l: E \rightarrow A$, for $A$ a set of
  \emph{actions}, the {\em labelling function}.
\end{itemize}\vspace{-1ex}
Henceforth, write $p\goto{u}q$ for $(p,u,q)\in \;\rightarrow$.
\end{definition}
{\bf Notes.\,} A \emph{labelled transition system} (LTS) is a
quadruple $(Q,\Sigma,\rightarrow,I)$ with $Q$ a set of states,
$\Sigma$ a set of \emph{labels}, $\rightarrow\;\subseteq
Q\times\Sigma\times Q$, and $I\in Q$.  An LTS is \emph{deterministic},
if it satisfies (1) above; in that case the \emph{transition relation}
$\rightarrow$ is really a \emph{partial function} from $Q\times
\Sigma$ to $Q$. A \emph{step transition system} is an LTS whose labels
are \emph{sets} or \emph{multisets} of actions, rather than single
actions.  Here $p\goto{u}q$ means that the represented system can
transition from state $p$ to state $q$ by performing the actions in
$u$ in \emph{one step}, meaning simultaneously or concurrently.
Property (2) says that in any state $p$ it is possible to do nothing
and stay in $p$.  Together with (1), property (2) implies that
\plat{p\goto{0}q} iff $q=p$, so without performing actions it is not
possible to move to another state. The information content would be
the same if in \df{LSTS} instead of (2) it would be required that
transitions are labelled by \emph{nonempty} multisets.

A step transition system is \emph{asynchronous} if it satisfies (3).
This requirement represents the postulate that different action
occurrences do not synchronise in any way; they can happen
simultaneously \emph{only} if they are causality independent, and in
that case they can also happen in any order.

Now a \emph{labelled step transition system} (LSTS) is a \emph{doubly}
labelled transition system. First of all the arrows are labelled by
sets of \emph{events}, and secondly the events are labelled by
actions. This double layer of labelling is reflected in the name, as
the word ``step'' already implies ``labelled''. The creation of events
as an intermediate concept between transitions and actions is a trick
that allows me to control the non-determinism of concurrent systems on
the level of actions.  I want to be able to model that a system in
state $p$ has a choice between two $a$-actions, leading to different
successor states, and at the level of abstraction at which the system
is represented there is no way to tell the two $a$s apart (or
\pagebreak[2]
influence the choice).  However, optionally based on the belief that
the world is not truly non-deterministic, the nondeterminism can be
attributed to a difference between the two $a$ actions that, although
not observable, does account for the fact that they lead to different
successor states. An \emph{event} is now an action together with all its
subtle qualities that influence which state it leads to when executed
in a given state. Thus, an action is an equivalence class of events
that are indistinguishable at the chosen level of abstraction.

When used for representing concurrent systems, LSTSs need to be
considered modulo a suitable semantic equivalence. One the finest
possible candidates is the following notion of
\emph{isomorphism of reachable parts}, $\cong_\mathcal{R}$:

\begin{definition}\rm\label{df-isom-reach}
Two LSTSs $\eA$ and $\eB$ are \emph{isomorphic}, written $\eA\cong\eB$,
if they differ only in the names of their states and events, i.e.\
if there are bijections $\beta: Q^\eA \rightarrow Q^\eB$ and
$\eta: E^\eA \rightarrow E^\eB$ such that $\beta(I^\eA)=I^\eB$, and,
for $p,q\!\in\! Q^\eA$, $u:E^\eA\rightarrow\IN$ and $e\!\in\! E^\eA$:
~~~\plat{\beta(p)\goto{\eta(u)}\beta(q)} iff $p\goto{u}q$~~~ and
~~~$l^\eB(\eta(e))=l^\eA(e)$.

The set $R(Q)$ of \emph{reachable states} in $\eA=(Q,E,\rightarrow,I,l)$
is the smallest set such that $I$ is reachable and whenever $p$ is
reachable and $p\goto{u}q$ then $q$ is reachable.
The \emph{reachable part} of $\eA$ is the LSTS
$\mathcal{R}(\eA)=(R(Q),E,\rightarrow\!\!\rest R(Q),I,l)$.

Write $\eA \cong_\mathcal{R} \eB$ if
${\cal R}(\eA)$ and ${\cal R}(\eB)$ are isomorphic.
\end{definition}
To check $\eA\cong_\mathcal{R}\eB$ it suffices to restrict to subsets
of $Q^\eA$ and $Q^\eB$ that contain all reachable states, and
construct an isomorphism between the resulting LSTSs.

\section{Interpreting Petri Nets in LSTSs}

I now give four translations from Petri nets into labelled
step transition systems, one for each of the computational
interpretations of this paper. This is a way of formally
pinpointing the differences between these interpretations; it amounts
to giving four different semantics of Petri nets.

\begin{definition}\rm
Let $\eN=(S,T,F,I,l)$ be a net. Then
$\CT(\eN)=(\IN^S,T,\rightarrow,I,l)$\linebreak is the LSTS associated to N
under the self-concurrent collective token interpretation, and
$\IT(\eN)=(\IN^{S_\bullet^+},T_\bullet,\rightarrow_\bullet,
I_\bullet^+,l_\bullet)$ is the LSTS associated to N under the
self-concurrent collective token interpretation.
$\ssCT(\eN)=(\IN^S,T,\rightarrow^{ss},I,l)$ and
$\ssIT(\eN)=(\IN^{S_\bullet^+},T_\bullet,
\rightarrow_\bullet^{ss},I_\bullet^{ss},l_\bullet)$ are the LSTSs
associated to N under the self-sequential interpretations.
\end{definition}

\begin{example}
\begin{figure}[b]
\vspace{-1.5em}
\input{ABC}
\centerline{\raise 1em\box\graph}
\vspace{-.3em}
\end{figure}
  The LSTSs below express the collective and individual
  token interpretation of the net A from \sect{interpretations},
  respectively. The equivalence of A and B under the collective token
  interpretation, and of A and C under the individual token
  interpretation, manifests itself as isomorphism of reachable parts
  of the associated LSTSs.

The pictures above display LSTSs up to isomorphism of reachable parts.
Letters like $b_a$ and $b_*$ stand for ``different events labelled
$b$''.  In fact, if the places of A are called $s_1$, $s_2$ and $s_3$,
respectively, and its transitions $a$ and $b$, then the event $b_*$ is
$(\{(*,0,s_2),(*,0,s_3)\},b)$, whereas
$b_a=(\{((\{(*,0,s_1)\},a),0,s_2),(*,0,s_3)\},b)$.
\end{example}

\begin{example}
The LSTSs associated to the net D of \sect{interpretations} under the
the collective and individual token interpretations can be found right
next to it.
\end{example}

\begin{example}\label{ex-self concurrency}
In the previous examples there was no difference between the
self-sequential and the self-concurrent interpretations.  The
following shows, however, that in general all four interpretations
yield a different result.
\begin{figure}[htp]
\vspace{-1.5em}
\input{self-conc}
\centerline{\raise 1em\box\graph}
\vspace{-1.5em}
\end{figure}
\end{example}

\section{The Relative Expressiveness of the Four Interpretations}
\label{sec-expressiveness}

Each of the four computational interpretations above makes a different
model of concurrency out of Petri nets. These models can now be
compared with respect to their expressive power in denoting labelled
step transition systems.

\subsection{The Individual versus Collective Token Interpretations}

The following theorem says that Petri nets under the self-concurrent
collective token interpretation are at least as expressive as Petri
nets under the self-concurrent individual token interpretation, in the
sense that any LSTS that can be denoted by a net under the latter
interpretation can also be a denoted by a net under the former
interpretation. On the other hand, the LSTS $\CT({\rm D})$ in
\sect{interpretations} cannot be denoted by a Petri net under the
individual token interpretation.

\begin{theorem}\label{thm-ind-col-hierarchy}
For every net $\eN$ there is a net $\eN_\bullet$ such that
$\CT(\eN_\bullet)=\IT(\eN)$.
\end{theorem}

\begin{proof}
$\eN_\bullet=(S_\bullet^+,T_\bullet,F_\bullet,I_\bullet^+,l_\bullet)$
with $S_\bullet^+$, $T_\bullet$, $I_\bullet^+$ and $l_\bullet$ as in
\df{tokens} and~\ref{df-resources}, and
\begin{itemize}\vspace{-1ex}
\item $F_\bullet(s',t')=1$ if $t'=(X,t)$ with $s'\in X$,
      or $t'=(k,t)\in T_\circ$ and $s'=t_k$;\\ $F_\bullet(s',t')=0$ otherwise;
\item $F_\bullet(t',s')=1$ if $s'$ has the form $(t',k,s)$;~
      $F_\bullet(t',s')=0$ otherwise.
\end{itemize}\vspace{-1ex}
That $\CT(\eN_\bullet)=\IT(\eN)$ is straightforward.\qed
\end{proof}
The net $\eN_\bullet$ constructed above is a close relative of the
\emph{unfolding} of a Petri net into an \emph{occurrence net}, as
defined in \cite{Wi87a,En91,MMS97} (see \sect{unfolding}). The
difference is that I have not bothered to eliminate unreachable places
and transitions.

\subsection{The Self-sequential versus Self-concurrent Interpretations}

In general, results as strong as the one above can not be obtained: in
order to compare expressiveness in a meaningful way, processes
represented by LSTSs, Petri nets, or other models of concurrency
should be regarded modulo some semantic equivalence relation. A
particularly fine equivalence relation that allows me to totally
order the computational interpretations of Petri nets is
isomorphism of reachable parts of LSTSs (see \df{isom-reach} in
\sect{LSTS}).

The following theorem shows that the behaviour of nets under the
self-sequential interpretations can easily be encoded into the
behaviour of nets under the corresponding self-concurrent
interpretation.

\begin{theorem}\label{thm-self-hierarchy}
For every net $\eN$ there is a net $\eN^{ss}$ such that
$\CT(\eN^{ss})\cong_\mathcal{R}\!\ssCT(\eN)$ and
$\IT(\eN^{ss})\cong_\mathcal{R}\ssIT(\eN)$.
\end{theorem}

\begin{proof}
Following \cite{GR83}, $\eN^{ss}$ is obtained from $\eN$ by adding for
every transition $t$ a {\em self-loop}, consisting of a place $s_t$
with $I(s_t)=F(s_t,t)=F(t,s_t)=1$ and $F(s_t,u)=F(u,s_t)=0$ for all
$u\neq t$.  Write $S_{new}$ for the set of new places $s_t$.

To check that $\CT(\eN^{ss})\cong_\mathcal{R}\ssCT(\eN)$,
restrict the states of $\CT(\eN^{ss})$, i.e.\ the markings $M$ of
$\eN^{ss}$, to the ones with $M(s_t)=1$ for all $s_t \!\in\!S_{new}$;
this set of states surely contains all reachable ones. Let
$\overline\beta(M)\!\in\IN^S$ be obtained by restricting the domain of
$M\!\in\IN^{S\cup S_{new}}$ to $S$, and $\overline\eta$ be the
identity. Now the bijections $\overline\beta$ and $\overline\eta$
constitute an isomorphism of reachable parts between $\CT(\eN^{ss})$
and $\ssCT(\eN)$.

To check that $\IT(\eN^{ss})\cong_\mathcal{R}\ssIT(\eN)$,
restrict the states of $\IT(\eN^{ss})$ to the individual states
$M_\bullet$ of $\eN^{ss}$ that contain exactly one token of the form
$(x,0,s_t)$ for each $s_t\in S_{new}$; this set of states surely
contains all reachable ones.  Also, in view of \cor{set}, the states
of $\IT(\eN^{ss})$ and $\ssIT(\eN)$ may be restricted to
\emph{sets} of resources rather than multisets.  Let $S_\circ =
\{s_t\!\in\! S_{new} \mid \pre{t}=0~\,(\mbox{in}~\eN)\}$.  For
$s_t\!\in\!S_\circ$, let $s_t^0=(*,0,s_t)$ and
$s_t^{k+1}=((\{s_t^k\},t),0,s_t)$.  Then all tokens $(x,k,s_t)$ of
$\eN^{ss}$ are of the form $s_t^k$ for $k\in\IN$.  Now the mappings
$\overline\eta$ from the transition firings in $\eN^{ss}$ to the
transition firings in $\eN$, for convenience extended with
$\overline\eta(*)=*$, and $\overline\beta$ from sets of individual
tokens in $\eN^{ss}$ to sets of individual resources in $\eN$, are
defined with recursion on the structure of transition firings and sets
of tokens by~
$\overline\eta(X,t)=\left\{\begin{array}{@{}l@{~\mbox{if}~}l@{}}
(\overline\beta(X),t)& \pre{t}\neq0\\ (k,t) & \pre{t}=0 \wedge
X=\{s_t^k\}\end{array}\right.$\\ and~ $\overline\beta(X)=
\{(\overline\eta(x),k,s) \mid (x,k,s)\!\in\! X \wedge
s\!\not\in\!S_{new}\}\cup\{t_k \mid s_t^k \!\in\! X \wedge
s_t\!\in\!S_{\circ}\}$.\\ Again, the bijections $\overline\beta$ and
$\overline\eta$ constitute an isomorphism between the
reachable parts of $\IT(\eN^{ss})$ and $\ssIT(\eN)$.\qed
\end{proof}
The construction of $\eN^{ss}$ above, reducing the self-sequential to
the self-concurrent interpretation of nets is well known \cite{GR83}.
The point of the proof above is to some extent just a sanity check on
the definitions of $\CT$, $\ssCT$, $\IT$ and $\ssIT$.

By \thm{self-hierarchy}, any LSTS that can be denoted by a Petri nets
under the self-sequential collective token interpretation, can
also be denoted by a net under the self-concurrent collective token
interpretation, and likewise for nets under the individual token
interpretations. On the other hand, the LSTS $\CT({\rm E})$ of
\ex{self concurrency} cannot be denoted by a Petri net under the
self-sequential collective token interpretation.

\subsection{Subsumption}

So far, I proved the expressiveness results $\ssIT \preceq \IT \prec
\CT \succ \ssCT$, where $\mathcal{J}\prec\mathcal{K}$ means that up to
$\cong_\mathcal{R}$ the class of LSTSs that can be denoted by Petri
nets under the computational interpretation $\mathcal{J}$ is a proper
subclass of the class that can be denoted by Petri nets under the
computational interpretation $\mathcal{K}$. Here I will strengthen and
augment these results by considering the following \emph{subsumption}
relation between computational interpretations and classes of nets.

\begin{definition}\rm\label{df-subsumption}
Write $\mathcal{J}\preceq_{\bf C}\mathcal{K}$ if ${\bf C}$ is a
class of Petri nets such that
\begin{itemize}\vspace{-1ex}
\item for any net $\eN\in{\bf C}$ one has
      $\mathcal{J}(\eN)\cong_\mathcal{R}\mathcal{K}(\eN)$ and
\item for any net $\eN$ there is a net $\eN'\in{\bf C}$ such that
      $\mathcal{J}(\eN')\cong_\mathcal{R} \mathcal{J}(\eN)$.
\end{itemize}\vspace{-1ex}
\end{definition}
If $\mathcal{J}\preceq_{\bf C}\mathcal{K}$, then up to
$\cong_\mathcal{R}$, the class of all Petri nets under interpretation
$\mathcal{J}$ is equally expressive as the subclass {\bf C} on which
the two interpretations coincide.

\begin{observation}
If $\mathcal{J}\preceq_{\bf C}\mathcal{K}\preceq_{\bf D}\mathcal{L}$
and ${\bf C}\subseteq{\bf D}$ then $\mathcal{J}\preceq_{\bf C}\mathcal{L}$.
\end{observation}
\begin{observation}
If $\mathcal{J}\preceq_{\bf C}\mathcal{K}\preceq_{\bf C}\mathcal{L}$
then $\mathcal{K}\preceq_{\bf C}\mathcal{J}$.
\end{observation}
Moreover, $\mathcal{J}\preceq_{\bf C}\mathcal{K}$ implies
$\mathcal{J}\preceq\mathcal{K}$. Also note that in the presence of
the first clause, the second clause of \df{subsumption} is
equivalent with
\begin{itemize}\vspace{-1ex}
\item for any net $\eN$ there is a net $\eN'\in{\bf C}$ such that
      $\mathcal{K}(\eN')\cong_\mathcal{R} \mathcal{J}(\eN)$.
\end{itemize}\vspace{-1ex}

\subsection{Self-sequential Petri Nets}

\begin{definition}\rm
A Petri net is \emph{self-sequential} if, using the standard
firing rule of \df{firing}, under no reachable marking a
proper multiset of transitions is enabled, i.e.\ a transition is
doubly enabled. Let {\bf SS} be the class of self-sequential nets.
\end{definition}

\begin{theorem}\label{thm-self-subsumption}
$\ssCT \preceq_{\bf SS} \CT$ and
$\ssIT \preceq_{\bf SS} \IT$.
\end{theorem}

\begin{proof}
If $\eN$ is self-sequential, trivially $\mathcal{R}(\ssCT(\eN))=
\mathcal{R}(\CT(\eN))$, and therefore $\ssCT(\eN)
\cong_\mathcal{R} \CT(\eN)$. Likewise, $\mathcal{R}(\ssIT(\eN))=
\mathcal{R}(\IT(\eN))$, considering that self-sequential nets can have
no transitions $t$ with $\pre{t}=0$. The second clause of
\df{subsumption} is satisfied because the net $N^{ss}$ constructed in
the proof of \thm{self-hierarchy} is self-sequential.
\end{proof}

\subsection{Unique-Occurrence Nets}

\begin{definition}\rm
A Petri net is a \emph{unique-occurrence net} if
 $\forall t \in T.~\pre{t}>0$ (i.e.\ it is a standard net),
 $\forall s\in S.~ I(s) + \Sigma_{t \in T} F(t,s) = 1$ and
 the flow relation $F$ is well-founded, i.e.\ there is no infinite
 alternating sequence $x_0, x_1,\ldots$ of places and transitions such
 that $F(x_{i+1},x_{i})>0$ for $i\in\IN$.
Let {\bf UO} be the class of unique-occurrence nets.
\end{definition}
This class of nets is a close relative of the class of
\emph{occurrence nets} of {\sc Winskel} \cite{Wi87a}; it just lacks
the requirements that cause the elimination of unreachable places and
transitions (see \sect{unfolding}).

\begin{proposition}\label{pr-UO-isomorphism}
For every Petri net $\eN$, the net $\eN_\bullet$ is an
unique-occurrence net.  Moreover, if $\eN$ is an unique-occurrence
net, then $\eN_\bullet \cong \eN$.
\end{proposition}

\begin{proof}
The first statement follows immediately from the construction of
$N_\bullet$, the well-foundedness of $F$ being a consequence of the
recursive nature of \df{tokens}.

The second statement follows with induction on the well-founded order
$F$, using the mappings $\beta$ and $\eta$ of \sect{individual}.\qed
\end{proof}
\pr{UO-isomorphism} tells that in a unique-occurrence net there is a
bijective correspondence between places and token occurrences, and
between transitions and transition firings. In particular, in a run of
a net each place will be visited at most once, and each transition will
fire at most once. Hence the name ``unique-occurrence nets''. It follows
that unique-occurrence nets are self-sequential.

\begin{theorem}\label{ITsubCT}
$\IT \preceq_{\bf UO} \CT$.
\end{theorem}

\begin{proof}
Let $\eN$ be a unique-occurrence net. Then
$\IT(\eN)=\CT(\eN_\bullet)\cong\CT(\eN)$, using
\thm{ind-col-hierarchy}, \pr{UO-isomorphism} and the observation
$\eN_\bullet\cong\eN \Rightarrow \CT(\eN_\bullet)\cong\CT(\eN)$.
Now let $\eN$ be any Petri net. Then $\eN_\bullet \in {\bf UO}$ by
\pr{UO-isomorphism} and $\CT(\eN_\bullet)\cong\IT(\eN)$
by \thm{ind-col-hierarchy}.
\end{proof}

\begin{theorem}
$\ssIT \preceq_{\bf UO} \IT \preceq_{\bf UO} \ssCT$ and
$\IT \preceq_{\bf UO} \ssIT \preceq_{\bf UO} \CT$.
\end{theorem}

\begin{proof}
Let $\eN$ be a unique-occurrence net.  As unique-occurrence nets are
self-sequential, Theorems~\ref{thm-self-subsumption} and~\ref{ITsubCT}
yield $\ssIT(\eN)\cong_\mathcal{R}\!\IT(\eN)
\cong_\mathcal{R}\!\CT(\eN)\cong_\mathcal{R}\!\ssCT(\eN)$.  Now
let $\eN$ be any Petri net. Then $(\eN^{ss})_\bullet$ is a
unique-occurrence net by \pr{UO-isomorphism} and
$\mathcal{H}_{\it any}^{\it any}((\eN^{ss})_\bullet)\cong_\mathcal{R}
\CT((\eN^{ss})_\bullet)\cong_\mathcal{R}\IT(\eN^{ss})
\cong_\mathcal{R}\ssIT(\eN)$ by
Theorems~\ref{thm-ind-col-hierarchy} and~\ref{thm-self-hierarchy}.
\end{proof}
This yields the expressiveness hierarchy of \fig{computational hierarchy}.

\section{Unfolding into Occurrence Nets}\label{sec-unfolding}

\begin{definition}[\cite{Wi87a}]\label{df-occurrence net}\rm
An \emph{occurrence net} is a unique-occurrence net such that
\begin{itemize}\vspace{-1ex}
\item the {\em conflict relation} $\#\!\subseteq T\times T$ is
irreflexive, where
      $$x\#y ~\Leftrightarrow~ \exists t,t'\!\in\! T.\,~
	t\neq t',~ \pre{t} \cap \pre{t'} \neq \emptyset,~ t F^* x,~ t F^* y$$
\item and $\forall t \in T.~ \{t'\mid t' F^* t\}$ is finite.
\pagebreak[2]\end{itemize}
\end{definition}
Here $F^*$ denotes the reflexive and transitive closure of the
\emph{flow relation}, given by $xFy$ iff $F(x,y)>0$.  It is easy to
see that transitions in a unique-occurrence net that violate the
conditions above can never fire, and in fact an occurrence net is a
unique-occurrence net with the property that every place occurs in a
reachable marking and every transition in a firing sequence.
Therefore, any unique-occurrence net can be converted into an
occurrence net by the operation $\mathcal{R}$ that omits all
transitions $t$ that violate the requirements above, together with all
places and transitions $x$ with $tF^*x$. The net $\mathcal{R}(\eN)$
consists of the \emph{reachable} places and transitions in $\eN$, and
$\mathcal{H}(\mathcal{R}(\eN))\cong_\mathcal{R}\mathcal{H}({\eN})$ for
$\mathcal{H}\in\{\CT,\IT,\ssCT,\ssIT\}$.  This allows me to define an
\emph{unfolding operator} $\mathcal{U}$, turning any given Petri net
$\eN$ into an occurrence net $\mathcal{U}(\eN)$ with
$\IT(\mathcal{U}(\eN))\cong_\mathcal{R}\IT(\eN)$, as follows.

\begin{definition}\rm\label{unfolding}
Let $\eN$ be a Petri net. The unfolding $\mathcal{U}(\eN)$ of $\eN$ is
$\mathcal{R}(\eN_\bullet)$.
\end{definition}
This construction extends the prior unfolding constructions of {\sc
Winskel} \cite{Wi87a}, {\sc Engelfriet} \cite{En91} and {\sc Meseguer,
Montanari \& Sassone} \cite{MMS97}. The latter, and most general, was
given for standard nets only. Instead of restricting to reachable
transitions at the end, these approaches do so on the fly.  The same
could be done here, by applying the two requirements of \df{occurrence
net} in the third clause of \df{tokens}.

%\bibliography{../Stanford/lib/biblio/glabbeek,../Stanford/lib/abbreviations,../Stanford/lib/dbase,../Stanford/lib/new}
\begin{thebibliography}{10}

\bibitem{Ba96}
{\sc E.~Badouel} (1996):
\newblock {\em Splitting of actions, higher-dimensional automata, and net synthesis.}
\newblock Technical Report RR-3490, Inria, France.

\bibitem{BD87}
{\sc E.~Best \& R.~Devillers} (1987):
\newblock {\em Sequential and concurrent behavior in {Petri} net theory.}
\newblock {\sl Theoretical Computer Science} 55(1), pp. 87--136.

\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{En91}
{\sc J.~Engelfriet} (1991):
\newblock {\em Branching processes of petri nets.}
\newblock {\sl Acta Informatica} 28(6), pp. 575--591.

\bibitem{vG05}
{\sc R.J.~van Glabbeek} (2005):
\newblock {\em On the expressiveness of higher dimensional automata (extended abstract).}
\newblock Available at {\tt http://boole.stanford.edu/\-pub/\-hda-ea.pdf}.
\newblock {\sl Electronic Notes in Theoretical Computer Science}
128(2): Proc. 11th International Workshop on {\sl Expressiveness in Concurrency}, EXPRESS 2004, pp. 5--34.

\bibitem{GP95}
{\sc R.J.~van Glabbeek \& G.D. Plotkin} (1995):
\newblock {\em Configuration structures (extended abstract).}
\newblock In D.~Kozen, editor: {\sl {\rm Proceedings $10^{th}$ Annual IEEE Symposium on} Logic in Computer Science, {\rm LICS'95, San Diego, USA}}, IEEE Computer Society Press, pp. 199--209.
\newblock Available at {\tt http://boole.stanford.edu/\-pub/\-conf.ps.gz}.

\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{MMS97}
{\sc J.~Meseguer, U.~Montanari \& V.~Sassone} (1997):
\newblock {\em On the semantics of place/ transition {Petri} nets.}
\newblock {\sl Mathematical Structures in Computer Science} 7$\!$, pp. 359--397.

\bibitem{Mu92}
{\sc M.~Mukund} (1992):
\newblock {\em Petri nets and step transition systems.}
\newblock {\sl International Journal of Foundations of Computer Science} 3(4), pp. 443--478.

\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{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, {\rm Proceedings of an Advanced Course, Bad Honnef, September 1986}}, {\sl \rm LNCS} 255, Springer, pp. 325--392.
\vspace{-1em}
\end{thebibliography}
\end{document}
