# Token Multiplicity in Reversing Petri Nets Under the Individual Token
Interpretation

Anna Philippou Kyriaki Psara Department of Computer Science, University of
Cyprus
Nicosia, Cyprus<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

Reversing Petri nets (RPNs) have recently been proposed as a net-based
approach to model causal and out-of-causal order reversibility. They are based
on the notion of individual tokens that can be connected together via bonds.
In this paper we extend RPNs by allowing multiple tokens of the same type to
exist within a net based on the individual token interpretation of Petri nets.
According to this interpretation, tokens of the same type are distinguished
via their causal path. We develop a causal semantics of the model and we prove
that the expressive power of RPNs with multiple tokens is equivalent to that
of RPNs with single tokens by establishing an isomporphism between the
Labelled Transition Systems (LTSs) capturing the reachable parts of the
respective RPN models.

##  1 Introduction

Reversible computation is a form of computing where transitions can be
executed in both the forward and the reverse direction, allowing systems to
return to past states. It has been attracting increasing attention due to its
application in a variety of fields such as low-power computing, biological
modelling, quantum computation, robotics, and distributed systems.

In the sequential setting reversibility is generally understood as the ability
to execute past actions in the exact inverse order in which they occurred, a
process referred to as _backtracking_. However, in the concurrent setting
matters are less clear. Indeed, various approaches have been investigated
within a variety of formalisms [9, 27, 17, 34, 25, 21]. One of the most well-
studied approaches considered suitable for a wide variety of concurrent
systems is that of _causal-consistent reversibility_ advocating that a
transition can be undone only if all its effects, if any, have been undone
beforehand [8]. The study of reversibility also extends to _out-of-causal-
order reversibility_ , a form of reversing where executed actions can be
reversed in an out-of-causal order [29, 28, 16] most notably featured in
biochemical systems.

In this work, we focus on Reversing Petri Nets [25] (RPNs), a reversible model
inspired by Petri nets that allows the modelling of reversibility as realised
by backtracking, causal-order, and out-of-causal-order reversing. A key
challenge when reversing computations in Petri nets is handling _backward
conflicts_. These conflicts arise when tokens occur in a certain place due to
different causes making unclear which transitions ought to be reversed. To
handle this ambiguity, RPNs introduce the notion of a _history_ of
transitions, which records causal information of executions. Furthermore,
inspired by biochemical systems as well as other resource-aware applications,
the model employs named tokens that can be connected together to form bonds,
and are preserved during execution.

A restriction in RPNs is that each token is unique and in order to model a
system with multiple items of the same type, it is necessary to employ a
distinct token for each item, at the expense of the net size. In the current
paper we consider an extension of RPNs, which allows multiple tokens of the
same type. The introduction of multiple identical tokens creates further
challenges involving backward conflicts and requires to extend the RPN
machinery for extracting the causal dependencies between transitions. We note
that formalizing causal dependencies is a well-studied problem in the context
of Petri nets, where various approaches have been proposed to reason about
causality [12, 14, 33]. In this work we draw inspiration from the so-called
individual token and collective interpretations of Petri nets [13, 11]. The
collective token philosophy considers all tokens of a certain type to be
identical, which results in ambiguities when it comes to causal dependencies.
In contrast, in an individual token interpretation, tokens are distinguished
based on their causal path. This approach leads to more complicated semantics
since to achieve token individuality requires precise correspondence between
the token instances and their past. However, it enables backward determinism,
which is a crucial property of reversible systems.

#### Contribution.

In this paper we extend RPNs to support multiple tokens of the same type
following the individual token interpretation. As such, tokens are associated
with their causal history and, while tokens of the same type are equally
eligible to fire a transition when going forward, when going backwards they
are able to reverse only the transitions they have previously fired. In this
context, we define a causal semantics for the model, based on the intuition
that a causal link exists between two transitions if a token produced by one
was used to fire the other. This leads to the observation that a transition
may reverse in causal order only if it was the last transition executed by all
the tokens it has involved. We note that this approach allows a causal-order
reversible semantics that, unlike the original RPN model, does not require any
global history information. In fact, all information necessary for reversal is
available locally within the history of tokens. Subsequently, we turn to study
the expressiveness of the presented model in comparison to RPNs with single
tokens. To do this we employ Labelled Transition Systems (LTSs) capturing the
state space of RPN models. We show that for any RPN with multiple tokens there
exists an RPN with single tokens with an isomorphic LTS, thereby confirming
our conjecture that RPNs with single tokens are as expressive as RPNs with
multiple tokens.

#### Related Work.

The first study of reversible computation within Petri nets was proposed in
[5, 6], where the authors investigated the effects of adding _reversed_
versions of selected transitions by reversing the directions of a transition’s
arcs. Unfortunately, this approach to reversibility violates causality.
Towards examining causal consistent reversibility the work in [22]
investigates whether it is possible to add a complete set of effect-reverses
for a given transition without changing the set of reachable markings, showing
that this problem is in general undecidable. In another line of work [21]
propose a causal semantics for P/T nets by identifying the causalities and
conflicts of a P/T net through unfolding it into an equivalent occurrence net
and subsequently introducing appropriate reverse transitions to create a
coloured Petri net (CPN) that captures a causal-consistent reversible
semantics. On a similar note, [20] introduces the notion of reversible
occurrence nets and associates a reversible occurrence net to a causal
reversible prime event structure, and vice versa. Finally, [7] introduces a
reversible approach to Petri nets following the individual token
interpretation. This work is similar to our approach though it refers to a
basic PN model, which does not contain named tokens nor bonds, and it does not
support backtracking and out-of-causal reversibility.

The modelling of bonding in the context of reversibility was first considered
within reversible processes and event structures in [30], where its usefulness
was illustrated with examples taken from software engineering and
biochemistry. Reversible frameworks that feature bonds as first-class
entities, like RPNs, also include the Calculus of Covalent Bonding [16], which
supports causal and out-of-causal-order reversibility in the context of
chemical reactions, as well as the Bonding Calculus [2], a calculus developed
for modeling covalent bonds between molecules in biochemical systems. In fact,
the latter two frameworks and RPNs were reviewed and compared for modeling
chemical reactions in [15] with case study the autoprotolysis of water.

This paper extends a line of research on reversing Petri nets, initially
introduced for acyclic nets [23] and subsequently for nets with cycles [25].
The usefulness of the framework was illustrated in a number of examples
including the modelling of long-running transactions with compensation and a
signal-passing mechanism used by the ERK pathway. The RPN framework has been
extended to control reversibility in [26] with an application to Massive MIMO.
Introducing multiple tokens in RPNs was also examined in [24] by allowing
multiple tokens of the same type to exist within a net following the
collective interpretation and yielding a locally-controlled, out-of-causal-
order reversibility semantics. RPNs have been translated to Answer Set
Programming (ASP), a declarative programming framework with competitive
solvers [10], and to bounded Coloured Petri Nets [3, 4].

##  2 Reversing Petri Nets with Multiple tokens

In our previous works we introduced Reversing Petri Nets, a net-based
formalism, which features individual tokens that can be connected together via
bonds [25]. An assumption of RPNs is that tokens are pairwise distinct. To
relax this restriction, subsequent work [24] introduced token multiplicity
whereby a model may contain multiple tokens of the same type. It was observed
that the possibility of firing a transition multiple times using different
sets of tokens, may introduce nondeterminism, also known as backward conflict,
when going backwards. Furthermore, two approaches were identified to define
reversible semantics in the presence of such backward conflicts, inspired by
the individual token and the collective token interpretations [11, 13],
defined to reason about causality in Petri nets. In the individual token
approach, multiple tokens of the same type residing in the same place are
distinguished based on their causal path, whereas in the collective token
interpretation they are not distinguished. In [24] the model of RPNs with
multiple tokens was investigated under the collective token approach, yielding
an out-of-causal-order form of reversibility. In this work, we instead apply
the individual token interpretation to define a causal semantics, and we
establish that in fact the addition of multiple tokens does not add to the
expressiveness of the model, in that for any RPN with multiple tokens there
exists an equivalent RPN with only a single token of each type.

Figure 1: RPN example of a pen assembly/dissassembly

To appreciate the challenges induced through the introduction of multiple
tokens and the difference between the individual and the collective token
interpretations, let us consider the example in Fig. 1(a). In this example we
may see an RPN model of an assembly/disassembly of a pen. The product consists
of the ink, the cup, and the button of the pen, modelled by tokens $i$, $c$,
and $b$, respectively. We may observe that transitions, in addition to
transferring tokens between places, have the capacity of creating bonds. Thus,
the process of manufacturing the pen requires the ink to be fitted inside the
cup, modelled by the creation of the bond $i-c$ by transition $t_{\\_}1$ and,
subsequently, the fitting of the button on the cup to complete the assembly,
modelled as the creation of the bond $c-b$ by transition $t_{\\_}2$ (RPN in
Fig. 1(b)). The effect of reversing a transition in RPNs is to break the bonds
created by the transition (if any) and returning the tokens/bonds from the
outgoing places to the incoming places of the transition. In [23, 25]
machinery has been developed in order to model backtracking, causal, and out-
of-causal-order reversibility for the model. In particular, in the example of
Fig. 1(b) reversing transition $t_{\\_}2$ will result in the destruction of
bond $c\\!-\\!b$ and the return of token $b$ to place $y$.

Suppose we wish to extend the model of Fig. 1(a) for the assembly of two pens.
Given that in RPNs tokens are unique, it would be necessary to introduce three
new and distinct tokens and clone the transitions while renaming their arcs to
accommodate for the names of the new tokens to be employed, resulting in a
considerable expansion of the model for each new pen to be produced. Thus, a
natural extension of the formalism involves relaxing this restriction and
allowing multiple tokens of the same type to exist within a model. To this
effect consider the scenario of Fig. 2(a) presenting a system with an already
assembled/sample pen in place $x$ and two items of each of the ink, cup, and
button components.

Figure 2: Executing transition $t_{\\_}1$ in the net (a) may yield the net in
(b). Different selections of tokens could have been made. In net (b)
transition $t_{\\_}1$ is executed with the (only) available tokens leading to
net (c), whereby execution of $t_{\\_}2$ with the component produced by the
first execution of $t_{\\_}1$ yields net (d).

An issue arising in this new setting is that due to the presence of multiple
tokens of the same type, the phenomenon of backwards nondeterminism occurs
when transitions are reversed. For instance, after execution of transition
$t_{\\_}1$ twice and $t_{\\_}2$, two assembled pens will exist in place $x$
and well as a component $i-c$, as seen in Fig. 2(d). Suppose that in this
state transition $t_{\\_}1$ is reversed. In the collective token
interpretation, all instances of the bond $i-c$ are considered identical. As a
result, any of these bonds could be destroyed during the reversal of
transition $t_{\\_}1$. However, in the individual token interpretation the
various ink and cup tokens are distinguished based on their causal path.
Therefore, the first execution of transition $t_{\\_}1$ yielding the net in
Fig. 2(b) and involving the shaded component of tokens in the figure, is
considered to have caused the execution of transition $t_{\\_}2$. Given this
causal relationships between the transitions, under a causal reversibility
semantics, the specific $i-c$ component should not be decomposed until
transition $t_{\\_}2$ is reversed. Similarly, the pre-existing pen should not
be broken down into its parts as it was not the created by any of the
transitions. Instead, reversing transition $t_{\\_}1$ in the RPN of Fig. 2(d)
should break the bond in the component consisting the single bond $i-c$. Note
that this is compatible with the understanding that disassembly of the product
would not allow the separation of the ink from the inside of the cup before
the button is removed, since this is enclosed within the pair of the cup and
the button.

As a result we observe that following the individual token interpretation,
reversing a computation requires keeping track of past behavior – in the
context of the example, distinguishing the tokens involving the pre-existing
pen and the tokens used to fire each transition. In the following sections we
implement this approach for introducing multiple tokens and we study its
properties in the context of causal-order reversibility. Furthermore, we
establish a correspondence between this model and RPNs with single tokens.

##  3 Multi Reversing Petri Nets

We present multi reversing Petri nets, an extension of RPNs with multiple
tokens of the same type that allow transitions to be reversed following the
individual token interpretation. Formally, they are defined as follows:

###### Definition 1

A _multi reversing Petri net_ (MRPN) is a tuple $(P,T,{\cal A},{\cal
A}_{\\_}V,{\cal B},F)$ where:

  1. 1.

$P$ is a finite set of _places_ and $T$ is a finite set of _transitions_.

  2. 2.

${\cal A}$ is a finite set of _base_ or _token types_ ranged over by
$A,B,\ldots$

  3. 3.

${\cal A}_{\\_}V$ is a finite set of _token variables_ ranged over by
$a,b,\ldots$ We write $\mathsf{type}(a)$ for the type of variable $a$ and
assume that $\mathsf{type}(a)\in{\cal A}$ for all $a\in{\cal A}_{\\_}V$.

  4. 4.

${\cal B}\subseteq{\cal A}\times{\cal A}$ is a finite set of undirected _bond
types_ ranged over by $\beta,\gamma,\ldots$ We assume ${\cal B}$ to be a
symmetric relation and we consider the elements $(A,B)$ and $(B,A)$ to refer
to the same bond type, which we also denote by $A\\!-\\!B$. Furthermore, we
write ${\cal B}_{\\_}V\subseteq{\cal A}_{\\_}V\times{\cal A}_{\\_}V$, assuming
that $(a,b)$ and $(b,a)$ represent the same bond, also denoted as $a-b$.

  5. 5.

$F:(P\times T\cup T\times P)\rightarrow{\cal P}({\cal A}_{\\_}V\cup{\cal
B}_{\\_}V)$ defines a set of directed labelled _arcs_ each associated with a
subset of ${\cal A}_{\\_}V\cup{\cal B}_{\\_}V$, where $(a,b)\in F(x,y)$
implies that $a,b\in F(x,y)$. Moreover, for all $t\in T$, $x,y\in P$, $x\neq
y$, $F(x,t)\cap F(y,t)=\emptyset$.

A multi reversing Petri net is built on the basis of a set of _token types_.
Multiple occurrences of a token type, referred to as _token instances_ , may
exist in a net. Tokens of the same type have identical capabilities on firing
transitions and can participate only in transitions with variables of the same
type.

As standard in net-based frameworks, places and transitions are connected via
labelled directed arcs. These labels are derived from ${\cal
A}_{\\_}V\cup{\cal B}_{\\_}V$. They express the requirements and the effects
of transitions based on the type of tokens consumed. Thus, collections of
tokens corresponding to the same types and connections as the variables on the
labelled arc are able to participate in the transition. More precisely, if
$F(x,t)=X\cup Y$, where $X\subseteq{\cal A}_{\\_}V$, $Y\subseteq{\cal
B}_{\\_}V$, the firing of $t$ requires a distinct token instance of type
$\mathsf{type}(a)$ for each $a\in X$, such that the overall selection of
tokens are connected together satisfying the restrictions posed by $Y$.
Similarly, if $F(t,x)=X\cup Y$, where $X\subseteq{\cal A}_{\\_}V$,
$Y\subseteq{\cal B}_{\\_}V$, this implies that during the forward execution of
the transition for each $a\in X$ a token instance of type $\mathsf{type}(a)$
will be transmitted to place $x$ by the transition, in addition to the bonds
specified by $Y$, some of which will be created as an effect of the
transition. We make the assumption that if $(a,b)\in Y$ then $a,b\in X$ and
the same variable cannot be used on two incoming arcs of a transition.

We introduce the following notations. We write $\circ t=\\{x\in P\mid
F(x,t)\neq\emptyset\\}$ and $t\circ=\\{x\in P\mid F(t,x)\neq\emptyset\\}$ for
the incoming and outgoing places of transition $t$, respectively. Furthermore,
we write $\mathsf{pre}(t)=\bigcup_{\\_}{x\in P}F(x,t)$ for the union of all
labels on the incoming arcs of transition $t$, and
$\mathsf{post}(t)=\bigcup_{\\_}{x\in P}F(t,x)$ for the union of all labels on
the outgoing arcs of transition $t$.

We restrict our attention to well-formed MRPNs, which satisfy the conservation
property [19] in the sense that the number of tokens in a net remains constant
during execution. In fact, as we will prove in the sequel, in well-formed nets
individual tokens are conserved.

###### Definition 2

An MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$ is _well-formed_ if for
all $t\in T$:

  1. 1.

${\cal A}_{\\_}V\cap\mathsf{pre}(t)={\cal A}_{\\_}V\cap\mathsf{post}(t)$ and

  2. 2.

$F(t,x)\cap F(t,y)=\emptyset$ for all $x,y\in P$, $x\neq y$.

Thus, a well-formed MRPN satisfies (1) whenever a variable exists in the
incoming arcs of a transition then it also exists on its outgoing arcs, and
vice versa, which implies that transitions neither create nor erase tokens,
and (2) tokens/bonds cannot be cloned into more than one outgoing place.

In the context of token multiplicity, a mechanism is needed in order to
distinguish between token instances with respect to their causal path. For
instance, consider the MRPN in Fig. 2(d). In this state, three connected
components of tokens are positioned in place $x$, where tokens of the same
type, e.g. the three $c$ tokens have distinct connections and causal
histories. To capture this, we distinguish between token instances, as
follows:

###### Definition 3

Given an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$ a _token instance_
has the form $(A,i,xs)$ where $xs$ is a (possibly empty) list of triples
$[(k_{\\_}1,t_{\\_}1,v_{\\_}1),\ldots,(k_{\\_}n,t_{\\_}n,v_{\\_}n)]$ with
$n\geq 0$, where $i\geq 1$, $A\in{\cal A}$, and for all $i$,
$k_{\\_}i\in\mathbb{N}$, $t_{\\_}i\in T$, and $v_{\\_}i\in\\{*\\}\cup{\cal
A}_{\\_}V$. We write ${\cal A}_{\\_}I$ for the set of token instances ranged
over by $A_{\\_}1$, $A_{\\_}2,\ldots$, and we define the set of bond instances
${\cal B}_{\\_}I$ by ${\cal B}_{\\_}I={\cal A}_{\\_}I\times{\cal A}_{\\_}I$.
Furthermore, given
$A_{\\_}i=(A,i,[(k_{\\_}1,t_{\\_}1,v_{\\_}1),\ldots,(k_{\\_}n,t_{\\_}n,v_{\\_}n)])$,
we write

$\displaystyle\mathsf{type}(A_{\\_}i)$ $\displaystyle=A$ $\displaystyle
A_{\\_}i\\!\downarrow$ $\displaystyle=$ $\displaystyle(A,i)$
$\displaystyle\mathsf{cpath}{A_{\\_}i}$ $\displaystyle=$
$\displaystyle[(t_{\\_}1,v_{\\_}1),\ldots,(t_{\\_}n,v_{\\_}n)]$
$\displaystyle\mathsf{last}(A_{\\_}i)$ $\displaystyle=$
$\displaystyle(k_{\\_}n,t_{\\_}n,v_{\\_}n)$ $\displaystyle A_{\\_}i+(k,t,v)$
$\displaystyle=$
$\displaystyle(A,i,[(k_{\\_}1,t_{\\_}1,v_{\\_}1),\ldots,(k_{\\_}n,t_{\\_}n,v_{\\_}n),(k,t,v)])$
$\displaystyle\mathsf{init}(A_{\\_}i)$ $\displaystyle=$
$\displaystyle(A,i,[(k_{\\_}1,t_{\\_}1,v_{\\_}1),\ldots,(k_{\\_}{n-1},t_{\\_}{n-1},v_{\\_}{n-1})])$

The set of token instances ${\cal A}_{\\_}I$ corresponds to the basic entities
that occur in a system. In the initial state of a net, tokens have the form
$(A,i,[])$ where $i$ is a unique identifier for the specific token instance of
type $A$. As computation proceeds the tokens evolve to capture their causal
path. If a transition $t$ is executed in the forward direction, with some
token instance
$(A,i,[(k_{\\_}1,t_{\\_}1,v_{\\_}1),\ldots,(k_{\\_}n,t_{\\_}n,v_{\\_}n)])$
substituted for a variable $v$, then the token evolves to
$(A,i,[(k_{\\_}1,t_{\\_}1,v_{\\_}1),\ldots,(k_{\\_}n,t_{\\_}n,v_{\\_}n),(k,t,v)])$,
where $k$ is an integer that characterizes the executed transition, as we will
formally define in the sequel.

In a graphical representation, tokens instances are indicated by $\bullet$
associated with their description, places by circles, transitions by boxes,
and bonds by lines between tokens. Note that token variables $a\in
F(x,t)\cap{\cal A}_{\\_}V$ with $\mathsf{type}(a)=A$ are denoted by $a:A$ over
the corresponding arc $F(x,t)$. An example of an MRPN can be seen in Fig. 3.
In this example, we have ${\cal A}=\\{I,C,B\\}$, ${\cal
A}_{\\_}V=\\{i,c,b\\}$, and the set of token instances in the specific state
are $\\{(I,i,[]),(B,i,[]),(C,i,[])\mid i\in\\{1,2,3\\}\\}$.

Figure 3: The net of Fig. 2(a) presented as an MRPN.

As with RPNs the association of token/bond instances to places is called a
_marking_ such that $M:P\rightarrow 2^{{\cal A}_{\\_}I\cup{\cal B}_{\\_}I}$,
where we assume that if $(A_{\\_}i,B_{\\_}i)\in M(x)$ then
$A_{\\_}i,B_{\\_}i\in M(x)$. In addition, we employ the notion of a _history_
, which assigns a memory to each transition $H:T\rightarrow 2^{\mathbb{N}}$.
Intuitively, a history of $H(t)=\emptyset$ for some $t\in T$ captures that the
transition has not taken place, or every execution of it has been reversed,
and a history such that $k\in H(t)$, captures that the transition had a firing
with identifier $k$ that was not reversed. Note that $|H(t)|>1$ may arise due
to cycles but also due to the consecutive execution of the transition by
different token instances. A pair of a marking and a history,
$\langle{M},{H}\rangle$, describes a _state_ of an MRPN with
$\langle{M_{\\_}0},{H_{\\_}0}\rangle$ the initial state, where
$H_{\\_}0(t)=\emptyset$ for all $t\in T$ and if $A_{\\_}i\in M_{\\_}0(x)$,
$x\in P$, then $A_{\\_}i=(A,i,[])$, and $A_{\\_}i\in M_{\\_}0(y)$ implies that
$x=y$.

Finally, we define $\mathsf{con}(A_{\\_}i,W)$, where $A_{\\_}i\in{\cal
A}_{\\_}I$ and $W\subseteq{{\cal A}_{\\_}I\cup{\cal B}_{\\_}I}$, to be the
tokens connected to $A_{\\_}i$ as well as the bonds creating these connections
according to set $W$:

$\displaystyle\mathsf{con}(A_{\\_}i,W)$ $\displaystyle=$
$\displaystyle(\\{A_{\\_}i\\}\cap W)$ $\displaystyle\cup$
$\displaystyle\\{x\mid\exists w\mbox{ s.t.
}\mathsf{path}(A_{\\_}i,w,W),(B_{\\_}i,C_{\\_}i)\in
w,x\in\\{(B_{\\_}i,C_{\\_}i),B_{\\_}i,C_{\\_}i\\}\\}$

where $\mathsf{path}(A_{\\_}i,w,W)$ if
$w=\langle\beta_{\\_}1,\ldots,\beta_{\\_}n\rangle$, and for all $1\leq i\leq
n$, $\beta_{\\_}i=(x_{\\_}{i-1},x_{\\_}i)\in W\cap{\cal B}_{\\_}I$,
$x_{\\_}i\in W\cap{\cal A}_{\\_}I$, and $x_{\\_}0=A_{\\_}i$. For example,
consider the net in Fig. 3 and let $W$ represent the set of token and bond
instances in place $x$. Then,
$\mathsf{con}((I,3,[]),W)=\\{(I_{\\_}3,C_{\\_}3,B_{\\_}3,(I_{\\_}3,C_{\\_}3),(C_{\\_}3,B_{\\_}3)\\}$,
where $I_{\\_}3=(I,3,[])$, $B_{\\_}3=(B,3,[])$, and $C_{\\_}3=(C,3,[])$.

###  3.1 Forward Execution

During the forward execution of a transition in an MRPN, a set of token and
bond instances, as specified by the incoming arcs of the transition, are
selected and moved to the outgoing places of the transition, possibly forming
and/or destroying bonds. Precisely, for a transition $t$ we define
$\mathsf{eff}^{+}(t)$ to be the bonds that occur on its outgoing arcs but not
the incoming ones and by $\mathsf{eff}^{-}(t)$ the bonds that occur in the
incoming arcs but not the outgoing ones:

$\mathsf{eff}^{+}(t)=\mathsf{post}(t)-\mathsf{pre}(t)\hskip
28.45274pt\mathsf{eff}^{-}(t)=\mathsf{pre}(t)-\mathsf{post}(t)$

Due to the presence of multiple instances of the same token type, it is
possible that different token instances are selected during the transition’s
execution. To enable such a selection of tokens we define the following:

###### Definition 4

An injective function ${\cal W}:V\rightarrow{\cal A}_{\\_}I$, where
$V\subseteq{\cal A}_{\\_}V$, is called a type-respecting assignment if for all
$a\in V$, if ${\cal W}(a)=A_{\\_}i$ then
$\mathsf{type}(a)=\mathsf{type}(A_{\\_}i)$.

We extend the above notation and write ${\cal W}(a,b)$ for $({\cal W}(a),{\cal
W}(b))$ and, given a set $L\subseteq{\cal A}_{\\_}V\cup{\cal B}_{\\_}V$, we
write ${\cal W}(L)=\\{{\cal W}(x)\mid x\in L\\}$.

Based on the above we define the following:

###### Definition 5

Given an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$, a state
$\langle{M},{H}\rangle$, and a transition $t$, we say that $t$ is _forward-
enabled_ in $\langle{M},{H}\rangle$ if there exists a type-respecting
assignment ${\cal S}:\mathsf{pre}(t)\cap{\cal A}_{\\_}V\rightarrow{\cal
A}_{\\_}I$ such that:

  1. 1.

${\cal S}(F(x,t))\subseteq M(x)$ for all $x\in\circ t$.

  2. 2.

If $a,b\in F(x,t)$ for some $x\in\circ t$ and $(a,b)\in\mathsf{eff}^{+}(t)$,
then ${\cal S}(a,b)\not\in M(x)$.

  3. 3.

If $a\in F(t,y_{\\_}1)$ and $b\in F(t,y_{\\_}2)$, for some
$y_{\\_}1,y_{\\_}2\in t\circ$, $y_{\\_}1\neq y_{\\_}2$, then
$\mathsf{con}({\cal S}(a),\mathsf{comp}_{\mathsf{f}}(t,{\cal
S},M))\neq\mathsf{con}({\cal S}(b),\mathsf{comp}_{\mathsf{f}}(t,{\cal S},M))$.

where $\mathsf{comp}_{\mathsf{f}}(t,{\cal S},M)=(\bigcup_{\\_}{x\in\circ
t}M(x)\cup{\cal S}(\mathsf{eff}^{+}(t)))-{\cal S}(\mathsf{eff}^{-}(t))$.

Thus, $t$ is forward-enabled in state $\langle{M},{H}\rangle$ if there exists
a type-respecting assignment ${\cal S}$ of token instances to the variables on
the incoming edges of $t$, which we will refer to as a forward-enabling
assignment of $t$, such that (1) the token instances and bonds required by the
transition’s incoming edges, according to ${\cal S}$, are available from the
appropriate input places, (2) if the selected token instances to be
transferred by the transition are to be bonded together by the transition then
they should not be already bonded in an incoming place of the transition (thus
the bonds that occur only on the outgoing arcs of a transition are the bonds
being created by the transition), and (3) if two token instances are
transferred by a transition to different outgoing places then these tokens
should not be connected. This is to ensure that connected components are not
cloned. Note that $\mathsf{comp}_{\mathsf{f}}(t,{\cal
S},M)=(\bigcup_{\\_}{x\in\circ t}M(x)\cup{\cal
S}(\mathsf{eff}^{+}(t)))-S(\mathsf{eff}^{-}(t))$ denotes the set of token and
bond instances that occur in the incoming places of $t$
($\bigcup_{\\_}{x\in\circ t}M(x)$), including the new bond instances created
by $t$ (${\cal S}(\mathsf{eff}^{+}(t))$), and removing the bonds destroyed by
it (${\cal S}(\mathsf{eff}^{-}(t))$). Intuitively,
$\mathsf{comp}_{\mathsf{f}}(t,{\cal S},M)$ contains the components that are
moved forward by the transition.

To execute a transition $t$ according to an enabling assignment ${\cal S}$,
the selected token instances along with their connected components are
relocated to the outgoing places of the transition as specified by the
outgoing arcs, with bonds created and destroyed accordingly. An additional
effect is the update of the affected token and bond instances to capture the
executed transition in their causal path. To capture this update we define
where $k$ is an integer associated with the specific transition instance:

$\hskip 42.67912ptA_{\\_}i\oplus({\cal
S},t,k)=\left\\{\begin{array}[]{ll}A_{\\_}i+(k,t,a)\hskip 42.67912pt\textrm{
if }{\cal S}(a)=A_{\\_}i\\\ A_{\\_}i+(k,t,*)\hskip 42.67912pt\textrm{ if
}{\cal S}^{-1}(A_{\\_}i)=\bot\end{array}\right.$

Note that $A_{\\_}i$ may not belong to the range of ${\cal S}$, i.e. ${\cal
S}^{-1}(A_{\\_}i)=\bot$, if $A_{\\_}i$ was not specifically selected to
instantiate a variable in $\mathsf{pre}(t)$ but, nonetheless, belonged to a
connected component transferred by the transition. This is recorded in the
causal path of the token instance via the triple $(k,t,*)$. Moreover, we write
$(A_{\\_}i,B_{\\_}j)\oplus({\cal S},t,k)$ for $(A_{\\_}i\oplus({\cal
S},t,k),B_{\\_}j\oplus({\cal S},t,k))$ and, given $L\subseteq{\cal
A}_{\\_}I\cup{\cal B}_{\\_}I$, we write $L\oplus({\cal
S},t,k)=\\{x\oplus({\cal S},t,k)\mid x\in L\\}$. Finally, the history of the
executed transition is updated to include the next unused integer. Given the
above we define:

###### Definition 6

Given an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$, a state $\langle
M,H\rangle$, a transition $t$ that is enabled in state $\langle M,H\rangle$,
and an enabling assignment ${\cal S}$, we write
$\langle{M},{H}\rangle\stackrel{{\scriptstyle(t,S)}}{{\longrightarrow}}\langle{M^{\prime}},{H^{\prime}}\rangle$
where for all $x\in P$:

$\displaystyle M^{\prime}(x)$ $\displaystyle=$
$\displaystyle(M(x)-\bigcup_{\\_}{a\in F(x,t)}\mathsf{con}({\cal S}(a),M(x)))$
$\displaystyle\cup$ $\displaystyle\;\bigcup_{\\_}{a\in
F(t,x)}\mathsf{con}({\cal S}(a),\mathsf{comp}_{\mathsf{f}}(t,{\cal
S},M))\oplus({\cal S},t,k)$

where $k=max(\\{0\\}\cup H(t))+1$ and

$\hskip
42.67912ptH^{\prime}(t^{\prime})=\left\\{\begin{array}[]{ll}H(t^{\prime})\cup\\{k\\},\hskip
39.83368pt\textrm{ if }t^{\prime}=t\\\ H(t^{\prime}),\hskip 66.29497pt\textrm{
otherwise }\end{array}\right.$

Figure 4: The effect of executing $t_{\\_}1$ and $t_{\\_}2$ in the net of Fig.
3, where $B_{\\_}3=(B,3,[])$, $C_{\\_}3=(C,3,[])$, $I_{\\_}3=(I,3,[])$,
$I_{\\_}1=(I,1,[(1,t_{\\_}1,i)])$, $C_{\\_}2=(C,2,[(1,t_{\\_}1,c)]$,
$I_{\\_}1^{\prime}=(I,1,[(1,t_{\\_}1,i),(1,t_{\\_}2,*)])$,
$C_{\\_}2^{\prime}=(C,2,[(1,t_{\\_}1,c),(1,t_{\\_}2,c)])$, and
$B_{\\_}2=(B,2,[(1,t_{\\_}2,b)])$.

Fig. 4 shows the result of consecutively firing transitions $t_{\\_}1$ and
$t_{\\_}2$ from the MRPN in Fig. 3 with enabling assignments ${\cal
S}_{\\_}1$, where ${\cal S}_{\\_}1(i)=(I,1,[])$, ${\cal
S}_{\\_}1(c)=(C,2,[])$, and ${\cal S}_{\\_}2$, where ${\cal
S}_{\\_}2(b)=(B,2,[])$, ${\cal S}_{\\_}2(c)=(C,2,[(1,t_{\\_}1,c)])$. We note
the non-empty histories of the transitions depicted in the graphical
representation, as well as the updates in the causal paths of the tokens.

###  3.2 Causal-order Reversing

We now move on to consider causal-order reversibility for MRPNs. In this form
of reversibility, a transition can be reversed only if all its effects (if
any), i.e. transitions that it has caused, have already been reversed. As
argued in [25], two transition occurrences are causally dependent, if a token
produced by the one was subsequently used to fire the other. Since token
instances in MPRNs are associated with their causal path, we are able to
identify the transitions that each token has participated in by observing its
memory. Furthermore, if $\mathsf{last}(A_{\\_}i)=(k,t,a)$ then the last
transition that the token instance $A_{\\_}i$ has participated in was
transition $t$ and specifically its occurrence with history $k$.

Based on this observation, a transition occurrence $t$ can be reversed in a
certain state if the token/bonds instances it has employed have not engaged in
any further transitions. Thus, we define causal reverse enabledness as
follows.

###### Definition 7

Consider an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$, a state
$\langle{M},{H}\rangle$, and a transition $t$. We say that $t$ is _co-enabled_
in $\langle{M},{H}\rangle$ if there exists a type-respecting assignment ${\cal
R}:\mathsf{post}(t)\cap{\cal A}_{\\_}V\rightarrow{\cal A}_{\\_}I$ such that:

  1. 1.

${\cal R}(F(t,x))\subseteq M(x)$ for all $x\in t\circ$, and

  2. 2.

there exists $k\in H(t)$ such that for all $(A,i,xs)\in\bigcup_{\\_}{x\in
P}M(x)$ with $(k,t,b)\in xs$ for some $b$, $(k,t,b)=\mathsf{last}(A_{\\_}i)$.

We refer to ${\cal R}$ as the $co$-reversal enabling assignment for the
$k^{th}$ occurrence of $t$.

Thus, a transition $t$ is $co$-enabled in $\langle{M},{H}\rangle$ for a
specific occurrence $k$ if there exists a type-respecting assignment of token
instances on the variables of the outgoing arcs of the transition, which gives
rise to a set of token and bond instances that are available in the relevant
out-places and, additionally, these token/bond instances were last employed
for the firing of the specific occurrence of the transition.

To implement the reversal of a transition $t$ according to a $co$-reversal
enabling assignment ${\cal R}$, the selected token instances are relocated
from the outgoing places of $t$ to its incoming places, with bonds created and
destroyed accordingly. The occurrence of the reversed transition is removed
from its history.

###### Definition 8

Given an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$, a state $\langle
M,H\rangle$, a transition $t$ that is $co$-enabled with $co$-reversal enabling
assignment ${\cal R}$ for the $k^{th}$ occurrence of $t$, we write
$\langle{M},{H}\rangle\stackrel{{\scriptstyle(t,{\cal
R})}}{{\rightsquigarrow}}\langle{M^{\prime}},{H^{\prime}}\rangle$ where for
all $x\in P$:

$\displaystyle M^{\prime}(x)$ $\displaystyle=$
$\displaystyle(M(x)-\bigcup_{\\_}{a\in F(t,x)}\mathsf{con}({\cal R}(a),M(x)))$
$\displaystyle\cup$ $\displaystyle\;\bigcup_{\\_}{a\in
F(x,t)}\mathsf{init}(\mathsf{con}({\cal
R}(a),\mathsf{comp}_{\mathsf{r}}(t,{\cal R},M)))$

and

$H^{\prime}(t^{\prime})=\left\\{\begin{array}[]{ll}H(t^{\prime})-\\{k\\},\hskip
14.22636pt\textrm{ if }t^{\prime}=t\\\ H(t^{\prime}),\hskip
39.26494pt\;\textrm{ otherwise }\end{array}\right.$

where $\mathsf{comp}_{\mathsf{r}}(t,{\cal R},M)=(\bigcup_{\\_}{x\in
t\circ}M(x)\cup{\cal R}(\mathsf{eff}^{-}(t)))-{\cal R}(\mathsf{eff}^{+}(t))$.

Figure 5: The effect of reversing transition $t_{\\_}1$ with enabling
assignment ${\cal R}(i)=I_{\\_}1$, ${\cal R}(c)=C_{\\_}2$, in a state
following the execution of $t_{\\_}1$ twice from the net in Fig. 3, first with
enabling assignment ${\cal S}_{\\_}1(i)=(I,1,[])$, ${\cal
S}_{\\_}1(c)=(C,2,[])$, and next with enabling assignment ${\cal
S}_{\\_}2(i)=(I,2,[])$, ${\cal S}_{\\_}2(c)=(C,1,[])$ where we write
$I_{\\_}1=(I,1,[(1,t_{\\_}1,i])$, $I_{\\_}2=(I,2,[(2,t_{\\_}1,i])$,
$C_{\\_}1=(C,1,[(2,t_{\\_}1,c])$, and $C_{\\_}2=(C,2,[(1,t_{\\_}1,c])$.

In Fig. 5 we may observe the causal-order reversal of transition $t_{\\_}1$.
We note that the history information of the affected components is updated by
removing the occurrence of the reversed transition and the history information
of transition $t_{\\_}1$ reflects that occurrence with identifier $1$ has been
reversed.

Let us now consider executions of both forward and backward moves and write
$\stackrel{{\scriptstyle}}{{\longmapsto}}$ for
$\stackrel{{\scriptstyle}}{{\longrightarrow}}\cup\stackrel{{\scriptstyle}}{{\rightsquigarrow}}$.
We define the reachable states of an MRPN as follows.

###### Definition 9

Given an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$ and an initial state
$\langle M_{\\_}0,H_{\\_}0\rangle$ we say that state $\langle M,H\rangle$ is
_reachable_ , if there exist $\langle M_{\\_}i,H_{\\_}i\rangle$, $i\leq n$ for
some $n\geq 0$, such that
$\langle{M_{\\_}0},{H_{\\_}0}\rangle\stackrel{{\scriptstyle(t_{\\_}1,{\cal
W}_{\\_}1)}}{{\longmapsto}}\langle{M_{\\_}1},{H_{\\_}1}\rangle\stackrel{{\scriptstyle(t_{\\_}2,{\cal
W}_{\\_}2)}}{{\longmapsto}}\ldots\stackrel{{\scriptstyle(t_{\\_}n,{\cal
W}_{\\_}n)}}{{\longmapsto}}\langle{M_{\\_}n},{H_{\\_}n}\rangle=\langle{M},{H}\rangle$.

Furthermore, given a type $A$, an integer $i$, and a marking $M$, we write
$\mathsf{num}(A,i,M)$ for the number of token instances of the form $(A,i,xs)$
in $M$, defined by $\mathsf{num}(A,i,M)=|\\{(x,A_{\\_}i)\mid\exists x\in
P,A_{\\_}i\in M(x),A_{\\_}i\\!\downarrow=(A,i)\\}|$. Similarly, for a bond
instance $\beta_{\\_}i\in{\cal B}_{\\_}I$, we define
$\mathsf{num}(\beta_{\\_}i,M)=|\\{x\in P\mid\beta_{\\_}i\in M(x)\\}|$. The
following result confirms that in an execution beginning in the initial state
of an MRPN, token instances are preserved, at most one bond instance may occur
at any time, and a bond instance may be created/destroyed during a
forward/reverse execution of a transition that features the bond as its
effect.

###### Proposition 1

Given an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$, a reachable state
$\langle{M},{H}\rangle$, and a transition firing
$\langle{M},{H}\rangle\stackrel{{\scriptstyle(t,{\cal
W})}}{{\longmapsto}}\langle{M^{\prime}},{H^{\prime}}\rangle$, the following
hold:

  1. 1.

For all $A$, $i$, $\mathsf{num}(A,i,M^{\prime})=\mathsf{num}(A,i,M)$=1.

  2. 2.

For all $\beta_{\\_}i\in{\cal B}_{\\_}I$,

    1. (a)

$0\leq\mathsf{num}(\beta_{\\_}i,M^{\prime})\leq 1$,

    2. (b)

if $t$ is executed in the forward direction with forward enabling assignment
${\cal S}$ and $\beta_{\\_}i\in{\cal S}(\mathsf{eff}^{+}(t))$ then
$\mathsf{num}(\beta_{\\_}i,M^{\prime})=1$; if instead $\beta_{\\_}i\in{\cal
S}(\mathsf{eff}^{-}(t))$ then $\mathsf{num}(\beta_{\\_}i,M^{\prime})=0$,
otherwise
$\mathsf{num}(\beta_{\\_}i,M)=\mathsf{num}(\beta_{\\_}i,M^{\prime})$.

    3. (c)

if $\,t\,$ is executed in the reverse direction with reverse enabling
assignment $\;{\cal R}\;$ and $\beta_{\\_}i\,\in$ ${\cal
R}(\mathsf{eff}^{+}(t))$ then $\mathsf{num}(\beta_{\\_}i,M^{\prime})=0$; if
instead $\beta_{\\_}i\in{\cal R}(\mathsf{eff}^{-}(t))$ then
$\mathsf{num}(\beta_{\\_}i,M^{\prime})=1$, otherwise
$\mathsf{num}(\beta_{\\_}i,M)=\mathsf{num}(\beta_{\\_}i,M^{\prime})$.

_Proof:_ The proof follows by induction on the length of the execution
reaching state $\langle{M},{H}\rangle$. If this is the initial state the
result (i.e. clauses 1 and 2(a)) follows by our assumption on the initial
state. For the induction step, let us assume that $\langle{M},{H}\rangle$
satisfies the conditions of the proposition.

Let us begin with clause (1) and suppose $\stackrel{{\scriptstyle(t,{\cal
W})}}{{\longmapsto}}=\stackrel{{\scriptstyle(t,{\cal
S})}}{{\longrightarrow}}$, where ${\cal S}$ is the forward-enabling assignment
for the transition, and let $A_{\\_}i=(A,i,xs)\in{\cal A}_{\\_}I$. Two cases
exist:

  1. 1.

$A_{\\_}i\in\mathsf{con}(B_{\\_}j,M(x))$ for some $B_{\\_}j$, ${\cal
S}(a)=B_{\\_}j$, $a\in F(x,t)$. Note that $x$ is unique by the assumption that
$\mathsf{num}(A,i,M)=1$. To discern the location of $A_{\\_}i$ in $M^{\prime}$
two cases exist.

     * •

Suppose $A_{\\_}i\in\mathsf{con}(B_{\\_}j,\mathsf{comp}_{\mathsf{f}}(t,{\cal
S},M))$. We observe that, by Definition 2(1), $a\in\mathsf{post}(t)$. Thus,
there exists $y\in t\circ$, such that $a\in F(t,y)$. Note that this $y$ is
unique by Definition 2(2). As a result, by Definition 6,
$\mathsf{con}(B_{\\_}j,\mathsf{comp}_{\mathsf{f}}(t,{\cal S},M))\subseteq
M^{\prime}(y)$, which implies that $A_{\\_}i\in M^{\prime}(y)$.

     * •

Suppose
$A_{\\_}i\not\in\mathsf{con}(B_{\\_}j,\mathsf{comp}_{\mathsf{f}}(t,{\cal
S},M^{\prime}))$ and consider
$w=\langle(A_{\\_}{i_{\\_}1},A_{\\_}{i_{\\_}2}),\ldots,$
$(A_{\\_}{i_{\\_}n},B_{\\_}j)\rangle$, $A_{\\_}i=A_{\\_}{i_{\\_}1}$, $n\geq
1$, such that $\mathsf{path}(A_{\\_}i,w,M(x))$. Since
$A_{\\_}i\not\in\mathsf{con}(B_{\\_}j,\mathsf{comp}_{\mathsf{f}}(t,{\cal
S},M^{\prime}))$ it must be that for some $k$,
$(A_{\\_}{i_{\\_}{k-1}},A_{\\_}{i_{\\_}{k}})\in{\cal S}(\mathsf{eff}^{-}(t))$
and $A_{\\_}i\in\mathsf{con}(A_{\\_}{i_{\\_}k},M(x)-{\cal
S}(\mathsf{eff}^{-}(t)))$. Using the same argument as in the previous case for
$A_{\\_}{i_{\\_}k}$ instead of $B_{\\_}j$, we may conclude that $A_{\\_}i\in
M(y)$ such that ${\cal S}(b)=A_{\\_}{i_{\\_}k}$ and $b\in F(t,y)$.

Now suppose that
$A_{\\_}i\in\mathsf{con}(C_{\\_}k,\mathsf{comp}_{\mathsf{f}}(t,{\cal S},M))$,
$C_{\\_}k={\cal S}(b)$ for some $b\neq a$, $b\in F(t,y^{\prime})$. Then it
must be that $y=y^{\prime}$. As a result, we have that
$\mathsf{num}(A,i,M^{\prime})=\mathsf{num}(A,i,M)=1$ and the result follows.

  2. 2.

$A_{\\_}i\not\in\mathsf{con}({\cal S}(b),M(x))$ for all $b\in F(x,t)$, $x\in
P$. This implies that $\\{x\in P\mid A_{\\_}i\in M^{\prime}(x)\\}=\\{x\in
P\mid A_{\\_}i\in M(x)\\}$ and the result follows.

Now suppose $\stackrel{{\scriptstyle(t,{\cal
W})}}{{\longmapsto}}=\stackrel{{\scriptstyle(t,{\cal
R})}}{{\rightsquigarrow}}$ where ${\cal R}$ is the reverse-enabling assignment
of the transition. Consider $A_{\\_}i=(A,i,xs)\in{\cal A}_{\\_}I$. Two cases
exist:

  1. 1.

$A_{\\_}i\in\mathsf{con}(B_{\\_}j,M(x))$ for some $B_{\\_}j$, ${\cal
R}(a)=B_{\\_}j$, $a\in F(t,x)$. Note that $x$ is unique by the assumption that
$\mathsf{num}(A,i,M)=1$. To discern the location of $A_{\\_}i$ in $M^{\prime}$
two cases exist.

     * •

Suppose $A_{\\_}i\in\mathsf{con}(B_{\\_}j,\mathsf{comp}_{\mathsf{r}}(t,{\cal
R},M^{\prime}))$. We observe that, by Definition 2(1), $a\in\mathsf{pre}(t)$.
Thus, there exists $y\in\circ t$, such that $a\in F(y,t)$. Note that this $y$
is unique by Definition 2(3). As a result, by Definition 8,

$M^{\prime}(y)=M(x)-\bigcup_{\\_}{a\in F(t,x)}\mathsf{con}({\cal
R}(a),M(x)))\cup\;\bigcup_{\\_}{a\in F(x,t)}\mathsf{init}(\mathsf{con}({\cal
R}(a),\mathsf{comp}_{\mathsf{r}}(t,{\cal R},M)))$

Since $a\in F(y,t)\cap F(t,x)$, $A_{\\_}i\in\mathsf{con}({\cal R}(a),M(x)\cup
F(y,t))$, which implies that $a\in M^{\prime}(y)$.

     * •

Suppose
$A_{\\_}i\not\in\mathsf{con}(B_{\\_}j,\mathsf{comp}_{\mathsf{r}}(t,{\cal
R},M^{\prime}))$ and consider
$w=\langle(A_{\\_}{i_{\\_}1},A_{\\_}{i_{\\_}2}),\ldots,$
$(A_{\\_}{i_{\\_}n},B_{\\_}j)\rangle$, $A_{\\_}i=A_{\\_}{i_{\\_}1}$, $n\geq
1$, such that $\mathsf{path}(A_{\\_}i,w,M(x))$. Since
$A_{\\_}i\not\in\mathsf{con}(B_{\\_}j,$ $\mathsf{comp}_{\mathsf{r}}(t,{\cal
R},M^{\prime}))$ it must be that for some $k$,
$(A_{\\_}{i_{\\_}{k-1}},A_{\\_}{i_{\\_}k})\in$ ${\cal R}(\mathsf{eff}^{+}(t))$
and $A_{\\_}i\in\mathsf{con}(A_{\\_}{i_{\\_}k},M(x)-{\cal
R}(\mathsf{eff}^{+}(t)))$. Using the same argument as in the previous case for
$A_{\\_}{i_{\\_}k}$ instead of $B_{\\_}j$, we may conclude that $A_{\\_}i\in
M(y)$ such that ${\cal S}(b)=A_{\\_}{i_{\\_}k}$ and $b\in F(y,t)$.

Now suppose that
$A_{\\_}i\in\mathsf{con}(C_{\\_}k,\mathsf{comp}_{\mathsf{r}}(t,{\cal R},M))$,
$C_{\\_}k={\cal R}(b)$ for some $a\neq b$, $b\in F(y^{\prime},t)$. Then it
must be that $y=y^{\prime}$. As a result, we have that $\\{z\in P\mid
A_{\\_}i\in M^{\prime}(z)\\}=\\{y\\}$ and the result follows.

  2. 2.

$A_{\\_}i\not\in\mathsf{con}({\cal R}(a),M(x))$ for all $a\in F(t,x)$, $x\in
P$. This implies that $\\{x\in P\mid A_{\\_}i\in M^{\prime}(x)\\}=\\{x\in
P\mid A_{\\_}i\in M(x)\\}$ and the result follows.

The proof of clause 2 follows similar arguments. $\Box$

We may now proceed to establish the causal consistency of our semantics. We
begin with defining when two states of an MRPN are considered to be causally
equivalent. Intuitively, states $\langle{M},{H}\rangle$ and
$\langle{M^{\prime}},{H^{\prime}}\rangle$ are causally equivalent whenever the
executions that have led to them contain the same causal paths. Note that
these causal paths refer to different independent threads of computation,
possibly executed through different interleavings in the executions leading to
$\langle{M},{H}\rangle$ and $\langle{M^{\prime}},{H^{\prime}}\rangle$. In our
setting, we can enunciate this requirement by observing the causal histories
of token instances and requiring that for each token instance of some type $A$
in one of the two states there is a token instance of the same type that has
participated in the exact same sequence of transitions in the other state:

###### Definition 10

Consider MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$ and reachable states
$\langle{M},{H}\rangle$, $\langle{M^{\prime}},{H^{\prime}}\rangle$. Then the
states are _causally equivalent_ , denoted by
$\langle{M},{H}\rangle\asymp\langle{M^{\prime}},{H^{\prime}}\rangle$, if for
each $x\in P$, $A_{\\_}i\in M(x)$ there exists $A_{\\_}j\in M^{\prime}(x)$
with $\mathsf{cpath}(A_{\\_}i)=\mathsf{cpath}(A_{\\_}j)$, and vice versa.

We may now establish the Loop Lemma for our model.

######  Lemma 1 (Loop)

For any forward transition
$\langle{M},{H}\rangle\stackrel{{\scriptstyle(t,{\cal
S})}}{{\longrightarrow}}\langle{M^{\prime}},{H^{\prime}}\rangle$ there exists
a backward transition
$\langle{M^{\prime}},{H^{\prime}}\rangle\stackrel{{\scriptstyle(t,{\cal
R})}}{{\rightsquigarrow}}\langle{M},{H}\rangle$ and for any backward
transition $\langle{M},{H}\rangle\stackrel{{\scriptstyle(t,{\cal
R})}}{{\rightsquigarrow}}\langle{M^{\prime}},{H^{\prime}}\rangle$ there exists
a forward transition
$\langle{M^{\prime}},{H^{\prime}}\rangle\stackrel{{\scriptstyle(t,{\cal
S})}}{{\longrightarrow}}\langle{M^{\prime\prime}},{H^{\prime\prime}}\rangle$
where
$\langle{M},{H}\rangle\asymp\langle{M^{\prime\prime}},{H^{\prime\prime}}\rangle$.

_Proof:_ Suppose $\langle{M},{H}\rangle\stackrel{{\scriptstyle(t,{\cal
S})}}{{\longrightarrow}}\langle{M^{\prime}},{H^{\prime}}\rangle$. Then $t$ is
clearly reverse-enabled in $\langle{M^{\prime}},{H^{\prime}}\rangle$ with
reverse-enabling assignment ${\cal R}$ such that if ${\cal S}(a)=(A,i,xs)$,
then ${\cal R}(a)=(A,i,xs+(t,k,a))$, where $k$ is the maximum element of
$H(t)$. Furthermore,
$\langle{M^{\prime}},{H^{\prime}}\rangle\stackrel{{\scriptstyle t,{\cal
R}}}{{\rightsquigarrow}}\langle{M^{\prime\prime}},{H^{\prime\prime}}\rangle$
where $H^{\prime\prime}=H$. In addition, all token and bond instances involved
in transition $t$ (except those in $\mathsf{eff}^{+}(t)$) will be returned
from the outgoing places of transition $t$ back to its incoming places. At the
same time, all destroyed bonds (those in $\mathsf{eff}^{-}(p)$) will be re-
formed, according to Proposition 1. Specifically, for all $A_{\\_}i\in{\cal
A}_{\\_}I$, it is easy to see by the definition of
$\stackrel{{\scriptstyle}}{{\rightsquigarrow}}$ that $A_{\\_}i\in
M^{\prime\prime}(x)$ if and only if $A_{\\_}i\in M(x)$. Similarly, for all
$\beta_{\\_}i\in{\cal B}_{\\_}I$, $\beta_{\\_}i\in M^{\prime\prime}(x)$ if and
only if $\beta_{\\_}i\in M(x)$. The opposite direction can be argued
similarly, with the distinction that when a transition is executed immediately
following its reversal, it is possible that the transition instance is
assigned a different key, thus giving rise to a state
$\langle{M^{\prime\prime}},{H^{\prime\prime}}\rangle$ distinct but causally
equivalent to $\langle{M},{H}\rangle$. $\Box$

We now proceed to define some auxiliary notions. Given a transition
$\langle{M},{H}\rangle\stackrel{{\scriptstyle(t,{\cal
W})}}{{\longmapsto}}\langle{M^{\prime}},{H^{\prime}}\rangle$, we say that the
_action_ of the transition is $(t,{\cal W})$ if
$\langle{M},{H}\rangle\stackrel{{\scriptstyle(t,{\cal
W})}}{{\longrightarrow}}\langle{M^{\prime}},{H^{\prime}}\rangle$ and
$(\underline{t},{\cal W})$ if
$\langle{M},{H}\rangle\stackrel{{\scriptstyle(t,{\cal
W})}}{{\rightsquigarrow}}\langle{M^{\prime}},{H^{\prime}}\rangle$ and we may
write $\langle{M},{H}\rangle\stackrel{{\scriptstyle(\underline{t},{\cal
W})}}{{\longmapsto}}\langle{M^{\prime}},{H^{\prime}}\rangle$. We write
$Act_{\\_}N$ for the set of all actions in an MRPN $N$. We use $\alpha$ to
range over $\\{t,\underline{t}\mid t\in T\\}$ and write
$\underline{\underline{t}}=t$. Given an execution
$\langle{M_{\\_}0},{H_{\\_}0}\rangle\stackrel{{\scriptstyle(\alpha_{\\_}1,{\cal
W}_{\\_}1)}}{{\longmapsto}}\ldots\stackrel{{\scriptstyle(\alpha_{\\_}n,{\cal
W}_{\\_}n)}}{{\longmapsto}}\langle{M_{\\_}n},{H_{\\_}n}\rangle$, we say that
the _trace_ of the execution is $\sigma=\langle(\alpha_{\\_}1,{\cal
W}_{\\_}1),(\alpha_{\\_}2,{\cal W}_{\\_}2),\ldots,(\alpha_{\\_}n,{\cal
W}_{\\_}n)\rangle$, and write
$\langle{M},{H}\rangle\stackrel{{\scriptstyle\sigma}}{{\longmapsto}}\langle{M_{\\_}n},{H_{\\_}n}\rangle$.
Given $\sigma_{\\_}1=\langle(\alpha_{\\_}1,{\cal
W}_{\\_}1),\ldots,(\alpha_{\\_}k,{\cal W}_{\\_}k)\rangle$,
$\sigma_{\\_}2=\langle(\alpha_{\\_}{k+1},{\cal
W}_{\\_}{k+1}),\ldots,(\alpha_{\\_}n,{\cal W}_{\\_}n)\rangle$, we write
$\sigma_{\\_}1;\sigma_{\\_}2$ for $\langle(\alpha_{\\_}1,{\cal
W}_{\\_}1),\ldots,(\alpha_{\\_}n,{\cal W}_{\\_}n)\rangle$. We may also use the
notation $\sigma_{\\_}1;\sigma_{\\_}2$ when $\sigma_{\\_}1$ or $\sigma_{\\_}2$
is a single transition. A central concept in what follows is causal
equivalence on traces, a notion that employs the concept of concurrent
transitions:

###### Definition 11

Consider an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$, a reachable
state $\langle{M},{H}\rangle$ and actions $(\alpha_{\\_}1,{\cal W}_{\\_}1)$
and $(\alpha_{\\_}2,{\cal W}_{\\_}2)$. Then $(\alpha_{\\_}1,{\cal W}_{\\_}1)$
and $(\alpha_{\\_}2,{\cal W}_{\\_}2)$ are said to be _concurrent_ in state
$\langle{M},{H}\rangle$, if for all $u,v\in{\cal A}_{\\_}V$, if ${\cal
W}_{\\_}1(u)=A_{\\_}i$ and ${\cal W}_{\\_}2(v)=B_{\\_}j$,
$A_{\\_}i,B_{\\_}j\in M(x)$ then
$\mathsf{con}(A_{\\_}i,M(x))\neq\mathsf{con}(B_{\\_}j,M(x))$.

Thus, two actions are concurrent when they employ different token instances.
This notion captures when two actions are independent, i.e. the execution of
the one does not preclude the other. Indeed, we may prove the following
results.

######  Proposition 2 (Square Property)

Consider an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$, a reachable
state $\langle{M},{H}\rangle$ and concurrent actions $(\alpha_{\\_}1,{\cal
W}_{\\_}1)$ and $(\alpha_{\\_}2,{\cal W}_{\\_}2)$ in $\langle{M},{H}\rangle$,
such that $\langle{M},{H}\rangle\stackrel{{\scriptstyle(\alpha_{\\_}1,{\cal
W}_{\\_}1)}}{{\longmapsto}}\langle{M_{\\_}1},{H_{\\_}1}\rangle$ and
$\langle{M},{H}\rangle\stackrel{{\scriptstyle(\alpha_{\\_}2,{\cal
W}_{\\_}2)}}{{\longmapsto}}\langle{M_{\\_}2},{H_{\\_}2}\rangle$. Then
$\langle{M_{\\_}1},{H_{\\_}1}\rangle\stackrel{{\scriptstyle(\alpha_{\\_}2,{\cal
W}_{\\_}2)}}{{\longmapsto}}\langle{M^{\prime}},{H^{\prime}}\rangle$ and
$\langle{M_{\\_}2},{H_{\\_}2}\rangle\stackrel{{\scriptstyle(\alpha_{\\_}1,{\cal
W}_{\\_}1)}}{{\longmapsto}}\langle{M^{\prime\prime}},{H^{\prime\prime}}\rangle$,
where
$\langle{M^{\prime}},{H^{\prime}}\rangle\asymp\langle{M^{\prime\prime}},{H^{\prime\prime}}\rangle$.

_Proof:_ It is easy to see that since the two transitions involve distinct
tokens then they can be executed in any order. If, additionally,
$\alpha_{\\_}1\neq\alpha_{\\_}2$ or $\alpha_{\\_}1=\alpha_{\\_}2$ and they are
both reverse transitions, then the effects imposed on the histories and the
tokens of the transitions will be independent and the same in both cases, i.e.
$\langle{M^{\prime}},{H^{\prime}}\rangle=\langle{M^{\prime}},{H^{\prime}}\rangle$.
If instead $\alpha_{\\_}1=\alpha_{\\_}2$ and $\alpha_{\\_}1$, $\alpha_{\\_}2$
are not both reverse transitions, then it is possible that distinct tokens
will be assigned to the forward transition(s). Nonetheless, the sequence of
actions executed by each token instance will be the same in both interleavings
and, thus, the resulting states are causally equivalent. $\Box$

######  Proposition 3 (Reverse Transitions are Independent)

Consider an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$, a state
$\langle{M},{H}\rangle$ and enabled reverse actions
$(\underline{t_{\\_}1},{\cal R}_{\\_}1)$ and $(\underline{t_{\\_}2},{\cal
R}_{\\_}2)$ where $(\underline{t_{\\_}1},{\cal
R}_{\\_}1)\neq(\underline{t_{\\_}2},{\cal R}_{\\_}2)$.
Then,$(\underline{t_{\\_}1},{\cal R}_{\\_}1)$ and $(\underline{t_{\\_}2},{\cal
R}_{\\_}2)$ are concurrent.

_Proof:_ It is straightforward to see that two distinct reverse transitions
employ different tokens. This is because a token instance may only reverse the
last transition occurrence in its history. Therefore
$(\underline{t_{\\_}1},{\cal R}_{\\_}1)$ and $(\underline{t_{\\_}2},{\cal
R}_{\\_}2)$ satisfy the requirement for being concurrent. $\Box$

We also define two transitions to be opposite in a certain state as follows:

###### Definition 12

Consider an MRPN $(P,T{\cal A},{\cal A}_{\\_}V,{\cal B},F)$ and actions
$(\alpha_{\\_}1,{\cal W}_{\\_}1)$ and $(\alpha_{\\_}2,{\cal W}_{\\_}2)$. Then
$(\alpha_{\\_}1,{\cal W}_{\\_}1)$ and $(\alpha_{\\_}2,{\cal W}_{\\_}2)$ are
said to be _opposite_ if $\underline{\alpha_{\\_}1}=\alpha_{\\_}2$ and, if
$\alpha_{\\_}i=t$ for some $t$, for all $a\in\mathsf{pre}(t)$,
$\mathsf{init}({\cal W}_{\\_}i(a))={\cal W}_{\\_}{3-i}(a)$.

Note that this may arise exactly when the two actions are forward and reverse
executions of the same transition and using the same token instances. We are
now ready to define when two traces are causally equivalent.

###### Definition 13

Consider a reachable state $\langle{M},{H}\rangle$. Then _causal equivalence
on traces with respect to_ $\langle{M},{H}\rangle$, denoted by
$\sigma_{\\_}1\asymp_{\\_}{\langle{M},{H}\rangle}\sigma_{\\_}2$, is the least
equivalence relation on traces such that (i)
$\sigma_{\\_}1=\sigma;(\alpha_{\\_}1,{\cal W}_{\\_}1);$ $(\alpha_{\\_}2,{\cal
W}_{\\_}2);\sigma^{\prime}$ where
$\langle{M},{H}\rangle\stackrel{{\scriptstyle\sigma}}{{\longmapsto}}\langle{M^{\prime}},{H^{\prime}}\rangle$
and if $(\alpha_{\\_}1,{\cal W}_{\\_}1)$ and $(\alpha_{\\_}2,{\cal W}_{\\_}2)$
are concurrent in $\langle{M^{\prime}},{H^{\prime}}\rangle$ then
$\sigma_{\\_}2=\sigma;(\alpha_{\\_}2,{\cal W}_{\\_}2);(\alpha_{\\_}1,{\cal
W}_{\\_}1);\sigma^{\prime}$, and (ii) if $(\alpha_{\\_}1,{\cal W}_{\\_}1)$ and
$(\alpha_{\\_}2,{\cal W}_{\\_}2)$ are opposite transitions then
$\sigma_{\\_}2=\sigma;\epsilon;\sigma^{\prime}$.

We may now establish the Parabolic Lemma, which states that causal equivalence
allows the permutation of reverse and forward transitions that have no causal
relations between them. Therefore, computations are allowed to reach for the
maximum freedom of choice going backward and then continue forward.

######  Lemma 2 (Parabolic Lemma)

Consider an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$, a reachable
state $\langle{M},{H}\rangle$, and an execution
$\langle{M},{H}\rangle\stackrel{{\scriptstyle\sigma}}{{\longmapsto}}\langle{M^{\prime}},{H^{\prime}}\rangle$.
Then there exist traces $r,r^{\prime}$ both forward such that
$\sigma\asymp_{\\_}{\langle{M},{H}\rangle}\underline{r};r^{\prime}$ and
$\langle{M},{H}\rangle\stackrel{{\scriptstyle\underline{r};r^{\prime}}}{{\longmapsto}}\langle{M^{\prime\prime}},{H^{\prime\prime}}\rangle$
where
$\langle{M^{\prime}},{H^{\prime}}\rangle\asymp\langle{M^{\prime\prime}},{H^{\prime\prime}}\rangle$.

_Proof_ Following [18], given the satisfaction of the Square Property
(Proposition 2) and the independence of reverse transitions (Proposition 3),
we conclude that the lemma holds. A proof from first principles may also be
found in [31]. $\Box$

We conclude with Theorem 1 stating that two computations beginning in the same
state lead to equivalent states if and only if the two computations are
causally equivalent. This guarantees the consistency of the approach since
reversing transitions in causal order is in a sense equivalent to not
executing the transitions in the first place. Reversal does not give rise to
previously unreachable states, on the contrary, it gives rise to causally-
equivalent states due to different keys being possibly assigned to concurrent
transitions.

###### Theorem 1

Consider an MRPN $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$, a reachable
state $\langle{M},{H}\rangle$, and traces $\sigma_{\\_}1$, $\sigma_{\\_}2$
such that
$\langle{M},{H}\rangle\stackrel{{\scriptstyle\sigma_{\\_}1}}{{\longmapsto}}\langle{M_{\\_}1},{H_{\\_}1}\rangle$
and
$\langle{M},{H}\rangle\stackrel{{\scriptstyle\sigma_{\\_}2}}{{\longmapsto}}\langle{M_{\\_}2},{H_{\\_}2}\rangle$.
Then, $\sigma_{\\_}1\asymp_{\\_}{\langle{M},{H}\rangle}\sigma_{\\_}2$ if and
only if
$\langle{M_{\\_}1},{H_{\\_}1}\rangle\asymp\langle{M_{\\_}2},{H_{\\_}2}\rangle$.

_Proof:_ Following [18], given the satisfaction of the Parabolic Lemma and the
fact that the model does not allow infinite reverse computations, we conclude
that the theorem holds. A proof from first principles may also be found in
[31]. $\Box$

##  4 Multi Tokens versus Single Tokens

We now proceed to define Single Reversing Petri Nets as MRPNs where each token
type corresponds to exactly one token instance.

###### Definition 14

A _Single Reversing Petri Net_ (SRPN) $(P,T,{\cal A},{\cal A}_{\\_}V,{\cal
B},F)$ is an MRPN where for all $A\in{\cal A}$, $|A|=1$.

Forward and causal-order reversal for SRPNs is defined as for MRPNs.
Consequently, SPRNs are special instances of MRPNs. In the sequel, we will
show that for each MRPN there is an “equivalent” SRPN. To achieve this,
similarly to [32], we will employ Labelled Transition Systems defined as
follows:

###### Definition 15

A labelled transition system (LTS) is a tuple $(Q,E,\rightarrow,I)$ where:

  * •

$Q$ is a countable set of states,

  * •

$E$ is a countable set of actions,

  * •

$\rightarrow\subseteq Q\times E\times Q$ is the step transition relation,
where we write $p\stackrel{{\scriptstyle u}}{{\longrightarrow}}q$ for
$(p,u,q)\in\rightarrow$, and

  * •

$I\in Q$ is the initial state.

For the purposes of our comparison, we will employ LTSs in the context of
isomorphism of reachable parts:

###### Definition 16

Two LTSs $L_{\\_}1=(Q_{\\_}1,E_{\\_}1,\rightarrow_{\\_}1,I_{\\_}1)$ and
$L_{\\_}2=(Q_{\\_}2,E_{\\_}2,\rightarrow_{\\_}2,I_{\\_}2)$ are isomorphic,
written $L_{\\_}1\cong L_{\\_}2$, if they differ only in the names of their
states and events, i.e. if there are bijections $\gamma:Q_{\\_}1\rightarrow
Q_{\\_}2$ and $\eta:E_{\\_}1\rightarrow E_{\\_}2$ such that
$\gamma(I_{\\_}1)=I_{\\_}2$, and, for $p,q\in Q_{\\_}1$, $u\in
E_{\\_}1:\gamma(p)\stackrel{{\scriptstyle\eta(u)}}{{\longrightarrow}}_{\\_}2\gamma(q)$
iff $p\stackrel{{\scriptstyle u}}{{\longrightarrow}}_{\\_}1q$.

The set ${\cal R}(Q)$ of reachable states in $L=(Q,E,\rightarrow,I)$ is the
smallest set such that $I$ is reachable and whenever $p$ is reachable and
$p\stackrel{{\scriptstyle u}}{{\longrightarrow}}q$ then $q$ is reachable. The
reachable part of $L$ is the LTS ${\cal{R}}(L)=(R(Q),E,\rightarrow_{\\_}{\cal
R},I)$, where $\rightarrow_{\\_}{\cal R}$ is the part of the transition
relation restricted to reachable states. We write
$L_{\\_}1\cong_{\\_}{\cal{R}}L_{\\_}2$ if ${\cal{R}}(L_{\\_}1)$ and
${\cal{R}}(L_{\\_}2)$ are isomorphic. To check
$L_{\\_}1\cong_{\\_}{\cal{R}}L_{\\_}2$ it suffices to restrict to subsets of
$Q_{\\_}1$ and $Q_{\\_}2$ that contain all reachable states, and construct an
isomorphism between the resulting LTSs.

We proceed to give a translation from MRPNs to SPRNs. First, we present how an
LTS can be associated with an MRPN/SRPN structure.

###### Definition 17

Let $N=(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$ be an MRPN (or SRPN) with
initial marking $M_{\\_}0$. Then ${\cal{H}}(N,M_{\\_}0)=((P\rightarrow
2^{{\cal A}_{\\_}I\cup{\cal B}_{\\_}I})\times(T\rightarrow
2^{\mathbb{N}}),Act,\stackrel{{\scriptstyle}}{{\longmapsto}},\langle{M_{\\_}0},{H_{\\_}0}\rangle)$
is the LTS associated with $N$.

We may now establish that for any MRPN there exists an SPRN with an isomorphic
LTS.

###### Theorem 2

For every MRPN $N=(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$ with initial
marking $M_{\\_}0$ there exists an SRPN $N^{\prime}=(P,T^{\prime},{\cal
A}^{\prime},{\cal A}_{\\_}V^{\prime},{\cal B}^{\prime},F^{\prime})$ with
initial marking $M_{\\_}0^{\prime}$ such that
${\cal{H}}(N,M_{\\_}0)\cong_{\\_}{\cal{R}}{\cal{H}}(N^{\prime},M_{\\_}0^{\prime})$.

_Proof:_ Let $N=(P,T,{\cal A},{\cal A}_{\\_}V,{\cal B},F)$ be an MRPN with
initial state $\langle{M_{\\_}0},{H_{\\_}0}\rangle$. We introduce the notation
${\cal W}\\!\downarrow$ where for any type-respecting assignment ${\cal W}$,
${\cal W}\\!\\!\downarrow\\!\\!(a)={\cal W}(a)\\!\\!\downarrow$, that is
${\cal W}$ assigns to a variable in the range of ${\cal W}$ the token instance
associated to it by ${\cal W}$ but with its history removed. Furthermore, if
$f={\cal W}\\!\\!\downarrow$ we write $f_{\\_}s(a)=a_{\\_}i$ if $f(a)=(A,i)$.
We construct $N^{\prime}=(P,T^{\prime},{\cal A}^{\prime},{\cal
A}_{\\_}V^{\prime},{\cal B}^{\prime},F^{\prime})$ with initial state
$\langle{M_{\\_}0^{\prime}},{H_{\\_}0^{\prime}}\rangle$ as follows:

$\displaystyle{\cal A}^{\prime}$ $\displaystyle=$
$\displaystyle\\{A_{\\_}i\mid\exists(A,i,[])\in M_{\\_}0(x)\mbox{ for some
}x\in P\\}$ $\displaystyle{\cal A}_{\\_}V^{\prime}$ $\displaystyle=$
$\displaystyle\\{a_{\\_}i\mid A_{\\_}i\in{\cal A}^{\prime}\\}$
$\displaystyle{\cal B}^{\prime}$ $\displaystyle=$
$\displaystyle\\{(A_{\\_}i,B_{\\_}j)\mid A_{\\_}i,B_{\\_}j\in{\cal
A}^{\prime},(A,B)\in{\cal B}\\}$ $\displaystyle T^{\prime}$ $\displaystyle=$
$\displaystyle\\{t_{\\_}{{\cal W}\\!\downarrow}\mid t\in T,{\cal
W}:\mathsf{pre}(t)\rightarrow{\cal A}_{\\_}I\mbox{ is a type-respecting
assignment }\\}$ $\displaystyle F^{\prime}(x_{\\_}1,x_{\\_}2)$
$\displaystyle=$ $\displaystyle\\{f_{\\_}s(a)\mid\exists
i\in\\{1,2\\},x_{\\_}i=t_{\\_}f\in T^{\prime},\mbox{ and
}a\in\mathsf{pre}(t)\\}$ $\displaystyle\cup$
$\displaystyle\\{(f_{\\_}s(a),f_{\\_}s(b))\mid\exists
i\in\\{1,2\\},x_{\\_}i=t_{\\_}f\in T^{\prime},(a,b)\in\mathsf{pre}(t)\\}$
$\displaystyle M_{\\_}0^{\prime}(x)$ $\displaystyle=$
$\displaystyle\\{(A_{\\_}i,1,[])\mid(A,i,[])\in M_{\\_}0(x)\\},\;\forall x\in
P$ $\displaystyle H_{\\_}0^{\prime}(t)$ $\displaystyle=$
$\displaystyle\emptyset,\;\forall t\in T^{\prime}$

The above construction, projects each type $A$ in $N$ to a set of types
$A_{\\_}i$ in $N^{\prime}$ such that, $A_{\\_}i\in{\cal A}^{\prime}$ for each
instance $(A,i,[])$ of type $A$ in $M_{\\_}0$. Type $A_{\\_}i$ contains
exactly one element, initially named $(A_{\\_}i,1,[])$. Furthermore, for each
transition $t\in T$, we create a set of transitions of the form $t_{\\_}f\in
T^{\prime}$, to associate all possible ways in which token/bond instances may
be taken as input by $t$ with a distinct transition that takes as input the
combination of types projected to by the instances.

We now proceed to define bijections $\gamma$ and $\eta$ for establishing the
homomorphism between the two LTSs. To simplify the proof, we assume that
during the execution of transitions the enabling assignment is recorded both
in the transition histories, i.e. given a transition $t$ we have $(k,{\cal
W})\in H(t)$ signifying that the $k^{th}$ occurrence of $t$ was executed with
enabling assignment ${\cal W}$ and also in a token instance $(A,i,xs)$
elements of $xs$ have the form $(k,t,v,{\cal W}\\!\\!\downarrow)$ again
recording the assignment that enabled the specific execution of the transition
occurrence. In this setting, it is easy to associate each token instance of
$N$ to a token instance of $N^{\prime}$ as follows, where we write
$st(A_{\\_}i)$ for the equivalent token instance of $A_{\\_}i$ in the SPRN
$N^{\prime}$:

$\;\;\;st((A,i,xs))=(A_{\\_}i,1,ys)$

where, if $xs=[(k^{i},t^{i},v^{i},f^{i})]_{\\_}{1\leq i\leq n}$ then
$ys=[(|\\{(k,t^{i},v,f)\mid\exists k,v,f\mbox{ s.t.}(k,t^{i},v,f)\in
ys\\}|,t_{\\_}f^{i},f_{\\_}s(a))]_{\\_}{1\leq i\leq n}$.

For any reachable state $\langle{M},{H}\rangle$ in LTS
${\cal{H}}(N,M_{\\_}0)$, we define
$\gamma(\langle{M},{H}\rangle)=\langle{M^{\prime}},{H^{\prime}}\rangle$ such
that for all $x\in P$ and $t_{\\_}f\in T^{\prime}$

$\displaystyle M^{\prime}(x)$ $\displaystyle=$
$\displaystyle\\{st(A_{\\_}i)\mid A_{\\_}i\in
M(x)\\}\cup\\{(st(A_{\\_}i),st(B_{\\_}j))\mid(A_{\\_}i,B_{\\_}j)\in M(x)\\}$
$\displaystyle H^{\prime}(t_{\\_}f)$ $\displaystyle=$
$\displaystyle\\{1,\ldots,k\mid k=|\\{(i,{\cal R})\in H(t)\mid{\cal
R}\\!\\!\downarrow=f\\}|\\}$

Furthermore, given an action $(t,{\cal W})$, we write

$\eta((t,{\cal W}))=(t_{\\_}{{\cal W}\\!\downarrow},{\cal W}^{\prime})$

where if ${\cal W}(a)=A_{\\_}i$ then ${\cal
W}^{\prime}(a_{\\_}i)=st(A_{\\_}i)$.

Based on these, we may confirm that there exists an isomorphism between the
LTSs ${\cal{H}}(N,M_{\\_}0)$ and ${\cal{H}}(N^{\prime},M_{\\_}0^{\prime})$ as
follows. Suppose $\langle{M_{\\_}m},{H_{\\_}m}\rangle$ is a reachable state of
${\cal{H}}(N,M_{\\_}0)$ with
$\gamma(\langle{M_{\\_}m},{H_{\\_}m}\rangle)=\langle{M_{\\_}s},{H_{\\_}s}\rangle$.
Two cases exist:

  * •

Suppose $\langle{M_{\\_}m},{H_{\\_}m}\rangle\stackrel{{\scriptstyle(t,{\cal
S})}}{{\longrightarrow}}\langle{M_{\\_}m^{\prime}},{H_{\\_}m^{\prime}}\rangle$.
This implies that $t$ is a forward-enabled transition with forward-enabling
assignment ${\cal S}$. Consider $\eta(t,{\cal S})=(t_{\\_}{{\cal
S}\\!\downarrow},{\cal S}^{\prime})$, as defined above. It is easy to see that
$t_{\\_}{{\cal S}\\!\downarrow}$ is also a forward-enabled transition in
$\langle{M_{\\_}s},{H_{\\_}s}\rangle$ with forward-enabling assignment ${\cal
S}^{\prime}$. Furthermore, if
$\langle{M_{\\_}s},{H_{\\_}s}\rangle\stackrel{{\scriptstyle(t_{\\_}{{\cal
S}\\!\downarrow},{\cal
S}^{\prime})}}{{\longrightarrow}}\langle{M_{\\_}s^{\prime}},{H_{\\_}s^{\prime}}\rangle$,
then

$\displaystyle M_{\\_}s^{\prime}(x)$ $\displaystyle=$
$\displaystyle(M_{\\_}s(x)-\bigcup_{\\_}{a\in F^{\prime}(x,t_{\\_}{{\cal
S}\\!\downarrow})}\mathsf{con}({\cal S}^{\prime}(a),M^{\prime}(x)))$
$\displaystyle\cup$ $\displaystyle\;\bigcup_{\\_}{a\in
F^{\prime}(t_{\\_}{{\cal S}\\!\downarrow},x)}\mathsf{con}({\cal
S}^{\prime}(a),\mathsf{comp}_{\mathsf{f}}(t_{\\_}{{\cal S}\\!\downarrow},{\cal
S}^{\prime},M_{\\_}s))\oplus({\cal S}^{\prime},t_{\\_}{\cal S},k)$
$\displaystyle=$ $\displaystyle(M_{\\_}s(x)-\bigcup_{\\_}{a\in
F(x,t)}\\{st(A_{\\_}i),(st(A_{\\_}i),st(B_{\\_}j))\mid
A_{\\_}i,(A_{\\_}i,B_{\\_}j)\in\mathsf{con}({\cal S}(a),M_{\\_}m(x)))$
$\displaystyle\cup$ $\displaystyle\;\bigcup_{\\_}{a\in
F(t,x)}\\{st(A_{\\_}i),(st(A_{\\_}i),st(B_{\\_}j))\mid
A_{\\_}i,(A_{\\_}i,B_{\\_}j)\in$ $\displaystyle\hskip
108.405pt\mathsf{con}({\cal S}(a),\mathsf{comp}_{\mathsf{f}}(t,{\cal
S},M_{\\_}m))\oplus({\cal S},t,k)\\}$

where $k=max(\\{0\\}\cup\\{k^{\prime}|k^{\prime}\in H(t)\\})+1$ and

$\hskip
42.67912ptH^{\prime}(t)=\left\\{\begin{array}[]{ll}H(t)\cup\\{k\\},\hskip
34.14322pt\textrm{ if }t=t_{\\_}{{\cal S}\\!\downarrow}\\\
H(t^{\prime}),\hskip 56.9055pt\textrm{ otherwise }\end{array}\right.$

We may see that
$\gamma(\langle{M_{\\_}m},{H_{\\_}m}\rangle)=\langle{M_{\\_}s},{H_{\\_}s}\rangle$,
and the result follows. Reversing the arguments, we may also prove the
opposite direction.

  * •

Suppose $\langle{M_{\\_}m},{H_{\\_}m}\rangle\stackrel{{\scriptstyle(t,{\cal
R})}}{{\rightsquigarrow}}\langle{M_{\\_}m^{\prime}},{H_{\\_}m^{\prime}}\rangle$.
This implies that $t$ is a reverse enabled transition with enabling assignment
${\cal R}$. Consider $\eta(t,{\cal R})=(t_{\\_}{{\cal R}\\!\downarrow},{\cal
R}^{\prime})$, as defined above. It is easy to see that $t_{\\_}{{\cal
R}\\!\downarrow}$ is also a reverse-enabled transition in
$\langle{M_{\\_}s},{H_{\\_}s}\rangle$ with reverse-enabling assignment ${\cal
R}^{\prime}$. Furthermore, if
$\langle{M_{\\_}s},{H_{\\_}s}\rangle\stackrel{{\scriptstyle(t_{\\_}{{\cal
R}\\!\downarrow},{\cal
R}^{\prime})}}{{\rightsquigarrow}}\langle{M_{\\_}s^{\prime}},{H_{\\_}s^{\prime}}\rangle$,
then using similar arguments as in the previous case we may confirm that
$\gamma(\langle{M_{\\_}m},{H_{\\_}m}\rangle)=\langle{M_{\\_}s},{H_{\\_}s}\rangle$.
The same holds for the opposite direction. This completes the proof. $\Box$

(a) MRPN $N$ (b) Equivalent SRPN $N^{\prime}$

Figure 6: Translating MRPNs to SRPNs

In Fig. 6 we present an MRPN $N$ and its respective SRPN $N^{\prime}$. From
$N$ we obtain $N^{\prime}$ by constructing the new token types
$I_{\\_}1,I_{\\_}2,C_{\\_}1,C_{\\_}2$ and exactly one token instance of each
of these types. The places are the same in both RPN models. The transitions
required for the SRPN are dependent on the types of the variables required for
each MRPN transition and the token instances representing that type.
Specifically for each token-instance combination that may fire a transition in
the MRPN, a respective transition is required in the SRPN. In the example, two
token instances of type $I$ can be instantiated to variable $i$ and two token
instances of type $C$ can be instantiated to variable $v$. This yields four
combinations of token instances resulting in four different transitions.

In Fig. 7 we may see the isomorphic LTSs of the two RPNs, where

$\displaystyle t_{\\_}{1,1}=t_{\\_}{{\cal S}_{\\_}1\\!\downarrow}$
$\displaystyle\underline{t_{\\_}{1,1}}=\underline{t_{\\_}{{\cal
R}_{\\_}1\\!\downarrow}}$ $\displaystyle t_{\\_}{1,2}=t_{\\_}{{\cal
S}_{\\_}2\\!\downarrow}$
$\displaystyle\underline{t_{\\_}{1,2}}=\underline{t_{\\_}{{\cal
R}_{\\_}2\\!\downarrow}}$ $\displaystyle t_{\\_}{2,1}=t_{\\_}{{\cal
S}_{\\_}3\\!\downarrow}$
$\displaystyle\underline{t_{\\_}{2,1}}=\underline{t_{\\_}{{\cal
R}_{\\_}3\\!\downarrow}}$ $\displaystyle t_{\\_}{2,2}=t_{\\_}{{\cal
S}_{\\_}4\\!\downarrow}$
$\displaystyle\underline{t_{\\_}{2,3}}=\underline{t_{\\_}{{\cal
R}_{\\_}4\\!\downarrow}}$

and the enabling assignments of the actions in the two LTSs are

$\displaystyle{\cal S}_{\\_}1(i)=(I,1,[]),$ $\displaystyle{\cal
S}_{\\_}1(c)=(C,1,[])$ $\displaystyle{\cal R}_{\\_}1(i)=(I,1,[(t,1,i)]),$
$\displaystyle{\cal R}_{\\_}1(c)=(C,1,[(t,1,c)])$ $\displaystyle{\cal
S}_{\\_}2(i)=(I,1,[]),$ $\displaystyle{\cal S}_{\\_}2(c)=(C,2,[])$
$\displaystyle{\cal R}_{\\_}2(i)=(I,1,[(t,1,i)]),$ $\displaystyle{\cal
R}_{\\_}2(c)=(C,2,[(t,1,c)])$ $\displaystyle{\cal S}_{\\_}3(i)=(I,2,[]),$
$\displaystyle{\cal S}_{\\_}3(c)=(C,1,[])$ $\displaystyle{\cal
R}_{\\_}3(i)=(I,2,[(t,1,i)]),$ $\displaystyle{\cal
R}_{\\_}3(c)=(C,1,[(t,1,c)])$ $\displaystyle{\cal S}_{\\_}4(i)=(I,2,[]),$
$\displaystyle{\cal S}_{\\_}4(c)=(C,2,[])$ $\displaystyle{\cal
R}_{\\_}4(i)=(I,2,[(t,1,i)]),$ $\displaystyle{\cal
R}_{\\_}4(c)=(C,2,[(t,1,c)])$

and

$\displaystyle{\cal S}_{\\_}1^{\prime}(i)=(I_{\\_}1,1,[]),$
$\displaystyle{\cal S}_{\\_}1(c)=(C_{\\_}1,1,[])$ $\displaystyle{\cal
R}_{\\_}1(i)=(I_{\\_}1,1,[(t,1,i)]),$ $\displaystyle{\cal
R}_{\\_}1(c)=(C_{\\_}1,1,[(t,1,c)])$ $\displaystyle{\cal
S}_{\\_}2(i)=(I_{\\_}1,1,[]),$ $\displaystyle{\cal
S}_{\\_}2(c)=(C_{\\_}2,1,[])$ $\displaystyle{\cal
R}_{\\_}2(i)=(I_{\\_}1,1,[(t,1,i)]),$ $\displaystyle{\cal
R}_{\\_}2(c)=(C_{\\_}2,1,[(t,1,c)])$ $\displaystyle{\cal
S}_{\\_}3(i)=(I_{\\_}2,1,[]),$ $\displaystyle{\cal
S}_{\\_}3(c)=(C_{\\_}1,1,[])$ $\displaystyle{\cal
R}_{\\_}3(i)=(I_{\\_}2,1,[(t,1,i)]),$ $\displaystyle{\cal
R}_{\\_}3(c)=(C_{\\_}1,1,[(t,1,c)])$ $\displaystyle{\cal
S}_{\\_}4(i)=(I_{\\_}2,1,[]),$ $\displaystyle{\cal
S}_{\\_}4(c)=(C_{\\_}2,1,[])$ $\displaystyle{\cal
R}_{\\_}4(i)=(I_{\\_}2,1,[(t,1,i)]),$ $\displaystyle{\cal
R}_{\\_}4(c)=(C_{\\_}2,1,[(t,1,c)])$

(a) LTS of net of Fig. 6(a)  (b) LTS of net of Fig. 6(b)

Figure 7: Isomorphic LTSs of an MRPN and its SPRN translation

##  5 Conclusions

This paper presents an extension of RPNs with multiple tokens of the same type
based on the individual token interpretation. The individuality of tokens is
enabled by recording their causal path, while the semantics allows identical
tokens to fire any eligible transition when going forward, but only the
transitions they have been previously involved in when going backward. We have
presented a semantics for causal-order reversibility, which unlike the
semantics presented in [25] is purely local and requires no global control.
Another contribution of the paper is a result illustrating that introducing
multiple tokens in the model does not increase its expressive power. Indeed,
for every MRPN we may construct an equivalent SRPN, which preserves its
computation. In related work [31], MRPNs have also been associated with
backtracking and out-of-causal-order semantics and it was shown that in all
settings MRPNs are equivalent to the original RPN model.

In our current work we are developing a tool for simulating and verifying RPN
models [10], which we aim to apply towards the analysis of resource-aware
systems. Our experience in applying RPNs in the context of wireless
communications [26] has illustrated that resource management can be studied
and understood in terms of RPNs since, along with their visual nature, they
offer a number of features, such as token persistence, that is especially
relevant in these contexts. In future work, we would like to further apply our
framework in the specific fields as well as in the field of long-running
transactions.

## References

  * [1]
  * [2] Bogdan Aman & Gabriel Ciobanu (2018): _Bonding calculus_.  Natural Computing 17(4), pp. 823–832, 10.1007/s11047-018-9709-7.
  * [3] Kamila Barylska, Anna Gogolinska, Lukasz Mikulski, Anna Philippou, Marcin Piatkowski & Kyriaki Psara (2018): _Reversing Computations Modelled by Coloured Petri Nets_.  In: Proceedings of ATAED 2018, CEUR Workshop Proceedings 2115, pp. 91–111.  Available at http://ceur-ws.org/Vol-2115/ATAED2018-91-111.pdf.
  * [4] Kamila Barylska, Anna Gogolinska, Lukasz Mikulski, Anna Philippou, Marcin Piatkowski & Kyriaki Psara (2022): _Formal Translation from Reversing Petri Nets to Coloured Petri Nets_.  In: Proceedings of RC 2022, LNCS 13354, Springer, pp. 172–186, 10.1007/978-3-031-09005-9_12.
  * [5] Kamila Barylska, Maciej Koutny, Lukasz Mikulski & Marcin Piatkowski (2018): _Reversible computation vs. reversibility in Petri nets_.  Science of Computer Programming 151, pp. 48–60, 10.1016/j.scico.2017.10.008.
  * [6] Kamila Barylska, Lukasz Mikulski, Marcin Piatkowski, Maciej Koutny & Evgeny Erofeev (2016): _Reversing Transitions in Bounded Petri Nets_.  In: Proceedings of CS&P 2016, CEUR Workshop Proceedings 1698, CEUR-WS.org, pp. 74–85.
  * [7] Adel Benamira (2020): _Causal Reversibility in Individual Token Interpretation of Petri Nets_.  The Computer Science Journal 21(4), 10.7494/csci.2020.21.4.3728.
  * [8] Vincent Danos & Jean Krivine (2004): _Reversible Communicating Systems_.  In: Proceedings of CONCUR 2004, LNCS 3170, Springer, pp. 292–307, 10.1007/978-3-540-28644-8_19.
  * [9] Vincent Danos & Jean Krivine (2005): _Transactions in RCCS_.  In: Proceedings of CONCUR 2005, LNCS 3653, Springer, pp. 398–412, 10.1007/11539452_31.
  * [10] Yannis Dimopoulos, Eleftheria Kouppari, Anna Philippou & Kyriaki Psara (2020): _Encoding Reversing Petri Nets in Answer Set Programming_.  In: Proceedings of RC 2020, LNCS 12227, Spinger, pp. 264–271, 10.1007/978-3-030-52482-1_17.
  * [11] Rob J. van Glabbeek (2005): _The Individual and Collective Token Interpretations of Petri Nets_.  In: Proceedings of CONCUR 2005, LNCS 3653, Springer, pp. 323–337, 10.1007/11539452_26.
  * [12] Rob J. van Glabbeek, Ursula Goltz & Jens-Wolfhard Schicke (2021): _On Causal Semantics of Petri Nets_.  CoRR abs/2103.00729.  Available at https://arxiv.org/abs/2103.00729.
  * [13] Rob J. van Glabbeek & Gordon D. Plotkin (1995): _Configuration Structures_.  In: Proceedings of LICS 1995, IEEE Computer Society, pp. 199–209, 10.1109/LICS.1995.523257.
  * [14] Jetty Kleijn & Maciej Koutny (2002): _Causality semantics of Petri nets with weighted inhibitor arcs_.  In: Proceedings of CONCUR 2002, LNCS 2421, Springer, pp. 531–546, 10.1007/3-540-45694-5_35.
  * [15] Stefan Kuhn, Bogdan Aman, Gabriel Ciobanu, Anna Philippou, Kyriaki Psara & Irek Ulidowski (2020): _Reversibility in Chemical Reactions_.  In: Reversible Computation: Extending Horizons of Computing - Selected Results of the COST Action IC1405, LNCS 1270, Spinger, pp. 151–176, 10.1007/978-3-030-47361-7_7.
  * [16] Stefan Kuhn & Irek Ulidowski (2018): _Local reversibility in a Calculus of Covalent Bonding_.  Science of Computer Programming 151(Supplement C), pp. 18–47, 10.1016/j.scico.2017.09.008.
  * [17] Ivan Lanese, Claudio Antares Mezzina & Jean-Bernard Stefani (2016): _Reversibility in the higher-order $\pi$-calculus_.  Theoretical Computer Science 625, pp. 25–84, 10.1016/j.tcs.2016.02.019.
  * [18] Ivan Lanese, Iain C. C. Phillips & Irek Ulidowski (2020): _An Axiomatic Approach to Reversible Computation_.  In: Proceedings of FOSSACS 2020, LNCS 12077 12077, Springer, pp. 442–461, 10.1007/978-3-030-45231-5_23.
  * [19] Y. Edmund Lien (1976): _A note on transition systems_.  Information Sciences 10(4), pp. 347–362, 10.1016/0020-0255(76)90054-2.
  * [20] Hernán C. Melgratti, Claudio Antares Mezzina, Iain Phillips, G. Michele Pinna & Irek Ulidowski (2020): _Reversible Occurrence Nets and Causal Reversible Prime Event Structures_.  In: Proceedings of RC 2020, LNCS 12227, Spinger, pp. 19–36, 10.1007/978-3-030-52482-1_2.
  * [21] Hernán C. Melgratti, Claudio Antares Mezzina & Irek Ulidowski (2020): _Reversing Place Transition Nets_.  Logical Methods in Computer Science 16(4).  Available at https://lmcs.episciences.org/6843.
  * [22] Lukasz Mikulski & Ivan Lanese (2019): _Reversing Unbounded Petri Nets_.  In: Proceedings of PETRI NETS 2019, LNCS 11522, Springer, pp. 213–233, 10.1007/978-3-030-21571-2_13.
  * [23] Anna Philippou & Kyriaki Psara (2018): _Reversible Computation in Petri Nets_.  In: Proceedings of RC 2018, LNCS 11106, Springer, pp. 84–101, 10.1007/978-3-319-99498-7_6.
  * [24] Anna Philippou & Kyriaki Psara (2022): _A collective interpretation semantics for reversing Petri nets_.  Theoretical Computer Science 924, pp. 148–170, 10.1016/j.tcs.2022.05.016.
  * [25] Anna Philippou & Kyriaki Psara (2022): _Reversible computation in nets with bonds_.  Journal of Logical and Algebraic Methods in Programming 124, p. 100718, 10.1016/j.jlamp.2021.100718.
  * [26] Anna Philippou, Kyriaki Psara & Harun Siljak (2019): _Controlling Reversibility in Reversing Petri Nets with Application to Wireless Communications_.  In: Proceedings of RC 2019, LNCS 11497, Springer, pp. 238–245, 10.1007/978-3-030-21500-2_15.
  * [27] Iain Phillips & Irek Ulidowski (2007): _Reversing algebraic process calculi_.  Journal of Logic and Algebraic Programming 73(1-2), pp. 70–96, 10.1016/j.jlap.2006.11.002.
  * [28] Iain Phillips & Irek Ulidowski (2015): _Reversibility and asymmetric conflict in event structures_.  Journal of Logical and Algebraic Methods in Programming 84(6), pp. 781–805, 10.1016/j.jlamp.2015.07.004.
  * [29] Iain Phillips, Irek Ulidowski & Shoji Yuen (2012): _A Reversible Process Calculus and the Modelling of the ERK Signalling Pathway_.  In: Proceedings of RC 2012, LNCS 7581, Springer, pp. 218–232, 10.1007/978-3-642-36315-3_18.
  * [30] Iain Phillips, Irek Ulidowski & Shoji Yuen (2013): _Modelling of Bonding with Processes and Events_.  In: Proceedings of RC 2013, LNCS 7947, Springer, pp. 141–154, 10.1007/978-3-642-38986-3_12.
  * [31] Kyriaki Psara (2020): _Reversible Computation in Petri Nets_.  Ph.D. thesis, Department of Computer Science, University of Cyprus.  Available at https://arxiv.org/abs/2101.07066.
  * [32] Wolfgang Reisig (1985): _Petri Nets with Individual Tokens_.  Theoretical Computer Science 41, pp. 185–213, 10.1016/0304-3975(85)90070-2.
  * [33] Grzegorz Rozenberg & Joost Engelfriet (1996): _Elementary net systems_.  In: Advanced Course on Petri Nets, LNCS 1491, Springer, pp. 12–121, 10.1007/3-540-65306-6_14.
  * [34] Irek Ulidowski, Iain Phillips & Shoji Yuen (2014): _Concurrency and Reversibility_.  In: Proceedings of RC 2014, LNCS 8507, Springer, pp. 1–14, 10.1007/978-3-319-08494-7_1.