\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*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
k0$ (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}
*