=Paper=
{{Paper
|id=Vol-2115/ATAED2018-91-111
|storemode=property
|title=Reversing Computations Modelled by Coloured Petri Nets
|pdfUrl=https://ceur-ws.org/Vol-2115/ATAED2018-91-111.pdf
|volume=Vol-2115
|authors=Kamila Barylska,Anna Gogolińska,Łukasz Mikulski,Anna Philippou,Marcin Piątkowski,Kyriaki Psara
|dblpUrl=https://dblp.org/rec/conf/apn/BarylskaGMPPP18
}}
==Reversing Computations Modelled by Coloured Petri Nets==
https://ceur-ws.org/Vol-2115/ATAED2018-91-111.pdf
Reversing Computations Modelled
by Coloured Petri Nets
1 1
Kamila Barylska , Anna Gogoli«ska , ukasz Mikulski ,
1
2 1
Anna Philippou , Marcin Pi¡tkowski , Kyriaki Psara
2
1
Faculty of Mathematics and Computer Science
Nicolaus Copernicus University, 87-100 Toru«, Poland
{kamila.barylska,anna.gogolinska,lukasz.mikulski,marcin.piatkowski}@mat.umk.pl
2
Department of Computer Science, University of Cyprus
{annap,kpsara01}@cs.ucy.ac.cy
Abstract. Reversible computation is an unconventional form of com-
puting where any sequence of performed operations can be executed in
reverse order at any point during computation. It has recently been at-
tracting increasing attention as on the one hand it promises low-power
computation and on the other hand it is inherent or of interest in a variety
of applications. In this paper we propose a structural way of translating
reversing Petri nets (RPNs), a formalism that embeds the three main
forms of reversibility (backtracking, causal reversing and out-of-causal-
order reversing), to Coloured Petri Nets (CPNs), an extension of tradi-
tional Petri Nets, where tokens carry data values. The translation into
the CPN model uses additional places and transitions in order to capture
the machinery employed in the RPN framework and demonstrates that
the abstract model of RPNs, and thus the principles of reversible compu-
tation, can be emulated in CPNs. The transformation can be automated
and utilized for the analysis of reversible systems using CPN Tools.
1 Introduction
Reversible computation is an emerging computational paradigm that al-
lows computation to be executed in the backward direction as eortlessly
as it can be executed in the standard forward direction. Physicist Rolf
Landauer [10] was the rst to argue that only irreversible computation
generates heat spawning a strong line of research towards the creation of
reversible logic gates and circuits. Besides, reversible computing attracts
much interest for its potential in a growing number of applications ranging
from biological processes, where computation may be carried out in for-
ward or backward direction [16, 9], to the eld of system reliability, where
reversibility can be used as a means of recovering from failures [6, 11].
Various strategies for reversing computation have been identi ed to
date, the most prominent being backtracking, causal reversing and out-
of-causal-order reversing. These approaches have been studied within a
variety of frameworks including process calculi and Petri nets. The main
91
challenge in these studies was to maintain the information needed to re-
verse computation, addressed by including memories of past behaviour.
The rst reversible process calculus RCCS [5] is a causal-consistent re-
versible extension of CCS that uses memory stacks in order to keep track
of past communications, further developed in [6, 7]. A general method for
reversing process calculi was subsequently proposed in [15] with CCSK be-
ing a special instance of the methodology. This proposal introduces keys to
bind synchronised actions together. Constructs for controlling reversibil-
ity were also proposed in reversible extensions of the π -calculus in [11, 12],
where the authors rely on simple thread tags, which act as unique identi-
ers. Furthermore, reversible computation was studied within event struc-
tures in [20, 17], whereas a reversible computational calculus for modelling
chemical systems, composed of signals and gates, was proposed in [3].
Petri nets (PNs) are a graphical mathematical language associated
with a rich mathematical theory and a variety of tools. They have been
used extensively for modelling and reasoning about a wide range of appli-
cations [19]. The rst study of reversible computation within Petri nets
was proposed in [1, 2]. In these works, the authors investigate the eects
of adding reversed versions of selected transitions in a PN, where these
transitions are obtained by reversing the directions of arcs connected to
them. They then explore decidability problems regarding reachability and
coverability in the resulting PNs.
In another line of work, [14] proposes a reversible approach to Petri
nets which implements an explicit approach for modelling reversible com-
putation that does not require the addition of transitions for modelling
reverse execution but, instead, allows to execute transitions in both for-
ward and backward direction. The proposed formalism, reversing Petri
nets (RPNs), introduces machinery and associated operational semantics
to tackle the challenges of the three main forms of reversibility. In par-
ticular, RPNs are acyclic Petri nets where tokens are persistent and are
distinguished from each other by an identity which allows transitions to
be reversed spontaneously in or out of causal order and a history function
is employed to track which transitions have been executed and in which
order. The model appears to be closely related to that of coloured Petri
nets (CPNs) [8], a backward compatible extension of traditional Petri
nets that allows tokens to have a data value/colour attached and hence
be distinguishable.
Contribution. The objective of this paper is to study the precise relation
between RPNs and CPNs, the main challenge being the presence of the
history notion in RPNs. Speci cally, histories in RPNs impose a form of
92
global control during transition execution that comes in contrast to the
nature of Petri nets where transition enabledness and execution can be
determined merely based on local conditions.
Our study of this relation has demonstrated that RPNs can be en-
coded into standard CPNs. We utilize bounded CPNs only, hence even if
some inhibitors are indirectly present (used to encode some functions of
CPN ML), the boundedness of a net assures that the state space is nite
and all inhibitors can be dropped by a standard complementary net con-
struction [2, 13]. As a result we conclude that the principles of reversible
computation can be encoded directly in the traditional model. Note that
inhibitor nets are in general Turing powerful and decision problems (in-
cluding reachability) are for them undecidable. However, in the case of
bounded inhibitor nets, which we are using, this is not an issue. The more
typical challenges are related with the complexity and the cost of increas-
ing (exponentially) the size of the net. Speci cally, we propose a structural
translation from RPNs to CPNs, where for each transition we consider
both forward and backward instances. Furthermore, the translation re-
lies on storing histories and causal dependencies of executed transition
sequences in additional places. The translation has been tested on a num-
ber of examples from all three forms of reversible computation, where the
CPN-tools [18] was employed to illustrate that the translations conform
to the semantics of reversible computation. Note that in addition to the
acyclicity assumption, we have also excluded forks from the present dis-
cussion in order to keep the presentation simpler, though we believe that
both of these assumptions can be lifted at the cost of a more complex
translation.
Paper organisation. In the next section we give an overview of reversing
Petri nets followed by Section 3, which describes the operational semantics
for backtracking, causal and out-of-causal-order reversibility. In Section 4
we recall the notion of coloured Petri nets, whereas the sections follow-
ing describe machinery for encoding local history (Section 5), encoding
of backtracking and causal reversing (Section 6) and encoding of out-of-
causal-order reversing (Section 7). Section 8 concludes the paper.
A working example of CPN that utilizes all constructions for out-of-
causal reversing is available: http://folco.mat.umk.pl/papers/reversing/.
93
2 Reversing Petri Nets
In this section we recall the notion of reversing Petri nets (RPNs) de ned
in [14] together with the basic de nitions and the semantic relations for
reversing computation in RPNs (see [14] for details).
RPNs support the main three categories of reversing computations.
The rst approach, the most restrictive one, called backtracking, allows
reversing only the transition which was last executed in the ongoing com-
putation. The second approach, less restrictive, called causal reversing,
allows a transition to rollback only if all its eects, if any, have been un-
done beforehand. The last form of undoing computation is the concept
of out-of-causal-order reversing, where any previously executed transition
can be undone. To capture this latter form of reversibility requires close
monitoring of token manipulation within a net. Indeed, undoing an ar-
bitrary transition during the execution of a Petri net calls for a clear
enunciation of each transition's eect and undoing such an eect involves
distinguishing each token on a net along with its causal path, i.e. the
places and transitions it has traversed before reaching its current state.
This requirement comes in con ict with transitions which might consume
multiple tokens but release only a subset or even a set of new tokens. To
resolve this, a reversing Petri net is built on the basis of a set of bases or
simply tokens that correspond to the basic entities that occur in a system.
These tokens are persistent, cannot be consumed, and can be combined to-
gether as the eect of transitions via so-called bonds into coalitions (also
called molecules ) that record the computational history of each token.
This approach is similar to reaction systems from biochemistry but can
be applied to a wide range of systems that feature reversible behaviour.
Based on this intuition, reversing Petri nets are de ned as follows:
De nition 1. A reversing Petri net is a tuple (P, T, F, A, B) where:
1. P and T are nite sets of places and transitions, respectively.
2. A is a nite set of bases or tokens. The set A = {a | a ∈ A} contains
negative instances and we write A = A ∪ A.
3. B ⊆ {{a, b} | a 6= b ∈ A} is a set of bonds. We use the notation a−b
for a bond {a, b} ∈ B . The set B = {β | β ∈ B} contains a negative
instance for each bond in B , B = B ∪ B .
4. F : (P × T ∪ T × P ) → 2
A∪B is a set of directed arcs labelled by
a subset of A ∪ B .
In the de nition of a reversing Petri net, the sets of places and transi-
tions are understood in a standard way (see [19]). For a label l = F (p, t)
94
or l = F (t, p) we assume that each token appears in l at most once (either
a or a), if a bond {a, b} ∈ l then a, b ∈ l and for l = F (t, p) we have
l ∩ A = ∅ and l ∩ B = ∅.
•
For transition t ∈ T we introduce t = {p ∈ P | F (p, t) 6= ∅},
t• = {p ∈SP | F (t, p) 6= ∅} (sets of
S input and output places of t), and
pre(t) = p∈P F (p, t), post(t) = p∈P F (t, p) (unions of labels of the
incoming/outgoing arcs of t), as well as effect(t) = post(t) \ pre(t).
The following restrictions give rise to the notion of well-formed RPNs.
De nition 2. A reversing Petri net is well-formed, if it satis es the fol-
lowing conditions for all t ∈ T :
1. A ∩ pre(t) = A ∩ post(t),
2. if a−b ∈ pre(t) then a−b ∈ post(t),
3. for every t ∈ T we have:
• t 6= ∅ and |t• |= 1,
4. if a, b ∈ F (p, t) and β = a−b ∈ F (t, q) then (β ∈ F (p, t) ∨ β ∈ F (p, t)).
Clause (1) indicates that transitions do not erase tokens and clause (2)
indicates that transitions do not destroy bonds. In (3) forks are prohibited
in order to avoid duplicating tokens that fork into dierent outgoing places
but are already bonded in the incoming places. Finally, clause (4) indicates
that tokens/bonds cannot be cloned into more than one outgoing places.
Remark 1. Note that the above de nition diers from De nition 2 of [14],
in that it additionally imposes condition 3. that every transition has at
least one incoming place and exactly one outgoing place. However, con ict
situations and concurrency might still occur.
A marking is a distribution of tokens and bonds across places, M :
P → 2A∪B , where for p ∈ P if a−b ∈ M (p) then a, b ∈ M (p). A history
assigns a memory to each transition, H : T → I
N. The value 0 associated
with a transition t ∈ T means that t has not been executed yet or it has
been reversed and not executed again, while a value k > 0 indicates that
t was the k th transition executed in the computation (and not reversed
until this moment) H0 denotes the initial history where H0 (t) = 0 for
every t ∈ T . A state is a pair hM, Hi of a marking and history.
For a ∈ A and C ⊆ A∪B we capture the set of tokens connected with a
via bonds as con(a, C) = ({a}∩C) ∪ {b, c, {b, c} | ∃w path{a, w, C}, {b, c} ∈
w}, where path{a, w, C} if w = hβ1 , . . . , βn i, and for all 1 ≤ i ≤ n we have
βi = {ai−1 , ai } ∈ C ∩ B , ai ∈ C ∩ A, and a0 = a.
As seen in Figure 1, reversing Petri nets admit a natural graphical
representation with places indicated by circles and transitions by boxes
95
connected to each other via labelled arcs. Tokens are indicated by • and
bonds by lines between relevant tokens. A history is represented over the
respective transition t as [m], where m = H(t), and is omitted when
m = 0.
From now on we assume RPNs to be well-formed and acyclic (in the
meaning of graph theory). Furthermore, as in [14], we assume that in
the initial marking of a RPN, M0 , there exists exactly one base of each
type, i.e. |{x | a ∈ M0 (x)}|= 1, for all a ∈ A. Now we can indicate the
conditions that must be met for a transition of a RPN to be enabled.
De nition 3. Consider a reversing Petri net (P, T, F, A, B), a transition
t ∈ T , and a state hM, Hi. We say that t is (forward) enabled in hM, Hi
if the following hold:
1. if a ∈ F (p, t), resp. β ∈ F (p, t), for p ∈
• t, then a ∈ M (p), resp. β ∈ M (p),
•
2. if a ∈ F (p, t), resp. β ∈ F (p, t) for p ∈ t, then a 6∈ M (p), resp. β 6∈ M (p),
3. if β ∈ F (t, p) for p ∈ t
• and β ∈ M (q) for q ∈ • t then β ∈ F (q, t).
A transition t is enabled in a state hM, Hi if all tokens from F (p, t)
for every p ∈ • t (i.e. tokens required by the action for execution) are
available, and none of the tokens whose absence is required exists in an
incoming place of the transition (clauses 1. and 2.). Clause 3 indicates
that if a pre-existing bond appears in an outgoing arc of a transition then
it is also a precondition for the transition to re. This enables us to de ne
the eect of a transition as effect(t) = post(t) − pre(t).
Remark 2. Note that the above de nition contains one less clause than
the associated de nition from [14] (de nition 3 ibidem). This clause has
become obsolete by the adoption of Clause 4. in the de nition of well-
formedness of the present paper, forbidding forks in RPNs.
De nition 4. Given a reversing Petri net (P, T, F, A, B), a state hM, Hi,
t 0 0
and a transition t enabled in hM, Hi, we write hM, Hi −→ hM , H i where:
S •
M (p) − a∈F (p,t)S
con(a, M (p)), if p ∈ t
M 0 (p) = M (p) ∪ F (t, p) ∪ a∈F (t,p),q∈• t con(a, M (q)), if p ∈ t•
M (p), otherwise
0 0
and H (t ) = max{k|k = H(t
00 ), t00 ∈ T } + 1 if t0 = t, and H(t0 ) otherwise.
After the execution of transition t, all suitable (according to De ni-
tion 4) tokens and bonds occurring in its incoming arcs are transferred
96
u u u
a
• a x a [1] x a [1] x
t 1 , t2 t2
t1 a-b y t1 a-b [2] y t1 a-b •a
•b y
•a
•b b t2 b-c b t2 b-c • b b t2 b-c
•c
w c c w c w c c
• •
z z z
Fig. 1. Forward and backtracking execution
from the input places to the output places of t. Moreover, the history
function H is changed by assigning the next available integer number to
the transition. An example of forward transitions can be seen in the rst
two steps of Figure 1 where transitions t1 and t2 take place with the his-
tories of the two transitions becoming [1] and [2], respectively. We also
note that the tokens have been transferred from the incoming places of t1
to the outgoing places of t2 whilst creating a bond between a−b−c
3 Forms of reversibility semantics
We now present the semantics for the three forms of reversibility as pro-
posed in [14].
3.1 Backtracking
A transition is backward enabled if the following holds:
De nition 5. Consider a reversing Petri net N = (P, T, F, A, B), a state
hM, Hi and a transition t ∈ T . We say that t is bt-enabled in hM, Hi if
H(t) = k > 0 with k ≥ k 0 for all k 0 ∈ N, k 0 = H(t0 ) and t0 ∈ T .
Thus, only the last executed transition can be backward executed in
this semantics. The eect of backtracking a transition in a reversing Petri
net is as follows:
De nition 6. Given a RPN N = (P, T, F, A, B), a state hM, Hi, and a
t 0 0
transition t bt-enabled in hM, Hi, we write hM, Hi b hM , H i where:
S •t
M (p) ∪ Sa∈F (p,t)∩F (t,q) con(a, M (q) − effect(t)), if p ∈
M 0 (p) = M (p) − a∈F (t,p) con(a, M (p)), if p ∈ t
•
M (p), otherwise
0 0
and H (t ) = 0 if t
0 = t, and H(t) otherwise.
97
After the reversal of t ∈ T all tokens and bonds from F (t, p) for p ∈ t ,
•
as well as their connected components, are removed, and transferred to
places from F (p, t). Note that in the nal step of Figure 1, the bonds
created by the transition are broken. Moreover the history function H of
t is changed to 0 to capture that the transition has been reversed.
3.2 Causal Reversing
Reversal enabledness in causal reversing semantics is de ned as follows.
De nition 7. Consider RPN N = (P, T, F, A, B), a state hM, Hi and
a transition t ∈ T . Then t is co-enabled in hM, Hi if H(t) > 0, and, for
0
all a ∈ F (t, p), if a ∈ M (q) for some q and con(a, M (q)) ∩ pre(t ) 6= ∅ for
0 0 0
some t ∈ T then either H(t ) = 0 or H(t ) ≤ H(t).
Note that the causal reversing of a transition t ∈ T is allowed if all
transitions executed causally after t have been reversed. The eect of
causally reversing a transition in a reversing Petri net is as follows:
De nition 8. Given a RPN N = (P, T, F, A, B), a state hM, Hi, and
t 0 0 0
a transition t co-enabled in hM, Hi, we write hM, Hi c hM , H i for M
0
and H as in De nition 6.
We reverse transitions in causal reversing semantics in the same man-
ner as in the backtracking semantics (De nition 6).
3.3 Out-of-causal-order Reversing
We are now ready to de ne out-of-causal-order reversing enabledness.
De nition 9. Consider a RPN N = (A, P, B, T, F ), a state hM, Hi and
a transition t ∈ T . We say that t is o-enabled in hM, Hi, if H(t) > 0.
According to the above de nition, in this setting, every transition
which has been executed can be reversed. The following notion helps to
de ne the last executed transition manipulating a given set of tokens,
where we write ⊥ to express that the value is unde ned.
De nition 10. Given a RPN N , an initial marking M0 , a current mark-
ing M , a history H , and a set of bases and bonds C we write:
t, if ∃t post(t) ∩ C 6= ∅, H(t) > 0,
last(C, H) = ∀t0 post(t0 ) ∩ C 6= ∅, H(t0 ) > 0, H(t0 ) ≤ H(t)
⊥, otherwise
The eect of reversing a transition in out-of-causal order is as follows:
98
u u
a
• a x a [1] x
t1 a-b y t1 t1 a-b •a
•b y
•b b t2 b-c b t2 b-c
w c c w c c
• •
z z
t2
u u
•a a x a [1] x
t1 a-b [2] y t1 t1 a-b [2] y
•a
b t2 b-c •b
•c b t2 b-c • b
•c
w c w c
z z
Fig. 2. Forward and out-of-causal-order execution
De nition 11. Given a RPN N = (A, P, B, T, F ), an initial marking
M0 , a state hM, Hi and a transition t that is o-enabled in hM, Hi, we
t 0 0 0
write hM, Hi o hM , H i where H is de ned as in De nition 6 and:
M 0 (p) = M (p) − effect(t) − {Ca,p | ∃a∈M (p) p ∈ t0• , t0 6= last(Ca,p , H 0 )}
∪ {Ca,q | ∃a,q a ∈ M (q), last(Ca,q ), H) = t0 , F (t0 , p) ∩ last(Ca,q ) 6= 0}
∪ {Ca,q | ∃a,y a ∈ M (q)last(Ca,q ), H 0 ) = ⊥, Ca,q ⊆ M0 (p)},
where Ca,p = con(a, M (p) − effect(t)).
As a result of out-of-causal-order reversing, a transition t ∈ T results
in breaking all bonds produced by t. For this reason in Figure 2 we can see
that it is possible for tokens to move backwards in the net. If the destruc-
tion of a bond divides a component into smaller connected components,
then those components should be relocated. They should be transferred
to the places in which they would have been located if transition t had
never been executed, which could imply the places in which they occurred
in the initial marking.
Note that out-of-causal-order reversing semantics may create new states
that were formerly unreachable by forward-only execution. For example
consider the process of catalysis from biochemistry where a catalyst a
helps the otherwise inactive molecules b and c to bond. Initially, a bonds
with b which then enables the bonding between b and c. Next (see nal
step of Figure 2), the catalyst is no longer needed and its bond to the
99
other two molecules is released in an out-of-causal manner which creates
the formerly unreachable state containing a bond between (only) b and c.
4 Coloured Petri Nets
Recall that RPNs constitute a model in which transitions can be reversed
according to three semantics: backtracking, causal, and out-of-causal-
order reversing. A main characteristic of RPNs is the concept of a history,
which assigns natural numbers to transitions. In general, this mechanism
may lead to the use of arbitrarily large numbers, thus requiring an in -
nite memory, hence resulting in an unbounded model. At the same time,
it imposes the need of a global control in order to reverse computation.
Our goal is to recast the model of [14] into one without the need for a
potentially in nite history while establishing the expressiveness relation
between RPNs and the model of bounded coloured Petri nets. In this sec-
tion we recall the notion of coloured Petri nets and we propose a model
that performs transition reversal according to the same semantics, but
needing only local memory to perform.
De nition 12 ([8]). A (non-hierarchical) coloured Petri net is a nine-
tuple CP N = (P, T, D, Σ, V, C, G, E, I), where:
P and T are nite, disjoint sets of places and transitions ;
D ⊆ P × T ∪ T × P is a set of directed arcs ;
Σ is a nite set of non-empty colour sets ;
V is a nite set of typed variables such that T ype(V ) ∈ Σ for all v ∈ V ;
C : P → Σ is a colour set function that assigns colour sets to places;
G : T → EXPR V is a guard function that assigns a guard to each
transition t such that Type[G(t)] = Bool;
E : D → EXPR V is an arc expression function that assigns an arc
C(p)
expression to each arc d ∈ D such that Type[E(d)] = I
N , where p
is the place connected with the arc d;
I : P → EXPR ∅ is an initialisation function that assigns an initialisa-
C(p)
tion expression to take each place p such that Type[I(p)] = I
N .
Note that, according to the utilised CPN Tools [4], EXPR V is the set
of net inscriptions (over a set of variables V , possibly empty, i.e. using only
constant values) provided by CPN ML. Moreover, by Type[e] we denote
the type of values obtained by the evaluation of expression e. The set of
free variables in an expression e is denoted by V ar[e], while the type of v
by Type[v]. The setting of a particular value to free variable v is called a
100
binding b(v). We require that b(v) ∈ Type[v] and denote with the use of hi
lled by the list of valuations and written next to the element to whom it
relates. The set of bindings of t is denoted by B(t). The binding element
is a transition t together with a valuation b(t) of all the free variables
related to t. We denote it by (t, b), for t ∈ T and b ∈ B(t).
A marking M in coloured Petri nets is a function which assigns to each
p ∈ P a multiset of tokens M (p) ∈ INC(p) . An initial marking is denoted
by M0 and de ned for each p ∈ P as follows: M0 (p) = I(p)hi.
A binding element (t, b) is enabled at a marking M if G(t)hbi is true
and at each place p ∈ P there are enough tokens in M to ful l the eval-
uation of the arc expression function E(p, t)hbi. The resulting marking
is obtained by removing from M (p) the tokens given by E(p, t)hbi and
adding those given by E(t, p)hbi for each p ∈ P .
In the following sections we show how to utilize coloured Petri nets
to reverse transitions in accordance with the three considered semantics:
backtracking, causal reversing and out-of-causal-order reversing. In fact,
we indicate how to obtain CPNs behaving analogously to RPNs.
5 Transformation local history
In this section we embark on constructing a procedure to transform an
acyclic RPN, as presented in De nition 1, to an equivalent CPN. As a rst
step we consider the history function H , which we transform into a set of
additional places. Speci cally, we introduce one place for every transition
and one place for every pair of transitions. This way, for each pair of tran-
sitions in a path π we are able to reconstruct the history of the pair and
using it we may reconstruct the whole history of RPN computations. The
proposed mechanism is local and distributed over the Petri net. Further-
more, it is universal for all types of reversing, with the assumption that
for causal-order reversing some places are not used. This is explained in
detail at the end of this section.
We construct the transformation of a RPN PR = (PR , TR , FR , AR , BR )
to CPN, namely the new coloured Petri net CR = (PC , TC , DC , ΣC , VC , CC ,
GC , EC , IC ) as follows.
The set of places PC contains all elements from PR , transition history
places assigned to each transition and connection history places assigned
to each pair of transitions: PC = PR ∪{hi | ti ∈ TR }∪{hij | ti , tj ∈ TR , i <
j}. The set of transitions of the net CR is the same as in a RPN, namely
TC = TR . New arcs have to be added to CR to connect newly added places.
Each transition is connected with its history place - as an input and an
101
output place. Every transition ti is also connected with every connection
history place hij (or hji depending on the order of i and j ) with two arcs
in opposite directions (they are at the same time input and output places
of the transition), where j is a number of transition, dierent from i.
DC = Domain(FR ) ∪ {(ti , hi ) | ti ∈ TR } ∪ {(hi , ti ) | ti ∈ TR }
∪ {(ti , hij ) | ti ∈ TR , i < j} ∪ {(ti , hji ) | ti ∈ TR , j < i}
∪ {(hij , ti ) | ti ∈ TR , i < j} ∪ {(hji , ti ) | ti ∈ TR , j < i}.
Bases in CPNs are the basic entities in a system which can also be
considered to be the atoms in a biochemical system. The set of colours
ΣC contains Base = AR ; Bond = BR ; Bases (lists of distinct bases
we can treat them as subsets of Base); Bonds (lists of distinct bonds
we can treat them as subsets of Bond); M olecule = Bases × Bonds;
HIST = {(n, i, j) | i, j, n ∈ N} (local history for a pair of transitions)
and Int (natural numbers). Here molecules, as in a biochemical system,
are considered to be a set of bases or atoms with the corresponding bond
between them.
The set of variables VC should contain all elements necessary to de-
scribe each input token of a transition.
The colour function CC assigns a molecule to every p ∈ PR , a natural
number to every hij ∈ PC , and a history HIST to every hi ∈ PC .
Markings of connection-history places are numbers, which describe
how many times transitions from the pair were executed. Namely, M (hij ) =
n means that transitions ti and tj were executed n times however the
marking does not specify how many times an individual transition was
executed. The markings of every transition history place hi are sets of
triples (n, j, i), where i and j are the numbers of two distinct transitions
and ti was n
th in a sequence of executions of t and t .
i j
The guard function GC has to be equivalent to the labels of input
arcs de ned in the reversing Petri net PR . Consequently, if a ∈ FR (p, ti )
(β ∈ FR (p, ti ), respectively) for a transition ti and its input place p, then
GC (ti ) should contain a condition, assuring that the bonding of an input
token for place p contains a (β , respectively).
The arc expression function EC for arcs between transitions ti ∈ TR
and places pi ∈ PR should be analogous to FR (ti , pi ). If ti only transfers
tokens then EC (ti , pi ) should be a union of bonds and bases of all inputs
for ti . If ti creates a bond β , then EC (ti , pi ) should be a union of bonds
and bases of all inputs for ti , together with the newly created bond β .
Places hij and hi control the history. The arc expression function is
de ned as: EC (hij , ti ) = historyij (EC (hij , tj ) = historyij ), EC (ti , hij ) =
102
historyij + 1 (EC (tj , hij ) = historyij + 1), where historyij ∈ VC and it
represents the value obtained from place hij by ti (tj ). Hence, the marking
of the connection history place hij denotes the next history value for
the pair of transitions ti and tj . For the transition history place hi , the
following arc expressions should be assigned: EC (hi , ti ) = listi , where listi
is a list of triples, which describes the previous history of the transition
ti and EC (hi , ti ) = listi ∪ {(historyij , j, i) | tj ∈ TR , M (hij ) = historyij }.
Since we assumed that each path π in a RPN is nite (as the net is acyclic),
values in places hi and hij are bounded.
(a) (b) tr1
h1 h12 h2
h1 h12 h2
t1 t1
t2 t2
Fig. 3. Adding history places to a CPN the basic construction for a CPN containing
transition history places hi , hj and connected history place hi,j (a). Introducing a re-
verse transition of ti (b). Construction appropriate for backtracking and causal-order
reversing (see Examples 1 and 2).
Example 1. Let us look at Figure 3(a). The transition ti is connected by a
self-loop with its history place hi , as well as tj is connected by a self-loop
with its history place hj . Moreover, both of them are connected with their
connection history place hij (assuming i < j ). The newly created places
and connections are depicted with the use of blue dashed arcs.
Transformation causal-order reversing. The construction described
to this point requires a re nement for causal-order reversing. In the case
of causal-order reversing, history places are created only for pairs of de-
pendent transitions, not for every possible transition pair.
De nition 13. Transitions ti , tj ∈ TR are dependent (we use the nota-
tion: (ti , tj ) ∈ Dep) if an input place of one of them is an output place of
the other: (ti , tj ) ∈ Dep ⇒ (ti ∩
• •t • •
j 6= ∅) or ( ti ∩ tj 6= ∅).
103
6 Transformation adding reverses: backtracking,
causal-order
The coloured Petri net CR described in Section 5 is prepared for reversing.
This can be achieved by adding supplementary reversal transitions. The
new CPN CR
0 = (P , T 0, D 0, Σ , V 0, C , G 0, E 0, I ) is based on C .
C C C C C C C C C R
The set of places PC and colours ΣC , the function CC and the initialization
expression IC are the same as in CR .
For every transition in CR , a new reversal transition tr is added to the
net. Hence TC
0 = T ∪ {tr | t ∈ T }. The execution of tr is equivalent to
C i i R i
a rollback of an execution of ti corresponding to tri . Each transition tri is
connected to the same set of places as ti ∈ TC but in opposite directions,
0=D
namely DC C ∪ {(tri , p) | (p, ti ) ∈ DC } ∪ {(p, tri ) | (ti , p) ∈ DC }.
The set of variables VC
0 should contain all elements necessary to de-
scribe each input token of all transitions (also reversal transitions).
The guard function GC
0 has to be modi ed to take into account the
newly created reversal transitions. The conditions used in the guard func-
tion for transitions tri should guarantee that the transition ti was the
last one executed in a system (for backtracking) or no other dependent
transition was executed after ti (for causal-order reversing). All necessary
information about an execution of ti can be obtained from the history
place hi assigned to ti and connection history places hij and hji .
The arc expression function EC
0 for arcs between transitions tr and
i
places pi ∈ PR should describe the reversal of the execution of ti . Hence,
if ti is just a transfer transition, then the arc description should contain
only the transfer of molecules. If ti creates a bond β = a − b then dur-
ing the execution of tri the bond should be broken. This results in the
production of two separate molecules, one of them including a while the
other one including b. Hence EC (pi , tri ) should contain only transfer of a
molecule, and EC (tri , pj ) should contain transfer of a molecule obtained
after breaking bond β = a−b, which includes a (b, respectively) if a (b,
respectively) has been transferred from the place pj during execution of
ti . It can be done using the CPN semantics in combination with the use
of functions, allowed in CPN ML.
The arc expression function for the pair (hi , tri ) (i.e. EC (hi , tri )) should
assign only transfer of the ti execution history. For arcs in the opposite
direction the arc expression function should return the history token to
hi with the last execution of ti excluded. Be aware that for acyclic RPNs
the last execution of a transition is the only execution of that transition.
For connection history places hij (hji respectively) values in those places
104
should be decreased by one during tri execution, and this operation should
be described by the arc expression function.
Example 2. Figure 3 depicts a net containing the newly created history
places (a), as well as the same net with the addition of the reverse tri of
the transition t (b). As one can see, the reverse transition is connected to
exactly the same places as t, but the arrows turn in the opposite direction.
The newly created part is depicted in dashed blue.
105
7 Transformation - adding reverses: out-of-causal-order
In the previous section constructions for backtracking and causal-order
reversing have been presented. Below we provide a similar construction
for out-of-causal-order reversing. Based on CR , let us de ne another CPN
CR 00 = (PC , TC 00, DC 00, ΣC 00, VC 00, CC 00, GC 00, EC 00, IC 00). Only the set PC re-
mains untouched, all other components of the CPN CR are adjusted.
A new colour smol set of molecules (represented as a list) is added
00 00 00
to ΣC . Hence ΣC = ΣC ∪ {smol}. CC assigns smol to places p ∈ PR .
00
For places from PC \ PR , functions CC and CC are the same. The change
is caused by the need to distinguish between an empty place and a place
with an empty molecule, represented by the empty set. In some cases the
empty list of molecules has to be transferred to or from a place. We need
extra arcs from and to those places, in directions opposite to the original
ones (the arcs are depicted with red dashed lines in Figure 4(a) since the
colour set function CC
00 for places of the original RPN has changed (see
below).
For every transition ti in CR , a new reversal transition tri is added to
the net. The execution of tri is equivalent to the rollback of the execution
of transition ti . Hence TC
00 = T ∪ {tr | t ∈ T }.
C i i C
As in the previous case, each transition tri is connected in opposite
direction to all places connected with ti . However, we also need to add
connections which allow to place accurately all molecules obtained during
breaking a bond that has been created by ti (or reversing a transfer).
For every ti ∈ TC we de ne a set of atoms Atomsti which contains all
bases related to ti , such that a ∈ Atomsti if a is present in the set of arc
• •
function values EC ( ti , ti ) (recall that a ∈ EC (ti , q) ⇒ a ∈ EC ( ti , ti )).
Then, for every ti ∈ TC we de ne a set of places T Pti (Transition's Places )
as follows: q ∈ T Pti if some base from Atomsti is present in q during
some computation of the net. It is possible to de ne the T Pti set using
the structure of RPNs. The reversal transition tri is connected in both
directions with every place from T Pti .
Transition tri is also connected in both directions with every transi-
tion history place and every connection history place. Those places are
necessary to give the reversal transition access to the complete history of
the RPN computations. Since CC
00 is dierent than in C , additional arcs
R
should be added from every transition ti ∈ TR to all its input places. This
is required to maintain correctly a token consisting of a list of molecules.
If a transition consumes a molecule from its input place, it has to transfer
the whole list and then put back the list without the respective molecule.
106
The similar goes for its output places. Summarising, in CR
00 every tran-
sition t ∈ TR is connected with its original input and output places with
two arcs in opposite directions.
(a) (b) tr1
h1 h12 h2
h1 h12 h2
t1 t1
t2 t2
Fig. 4. Adding a reverse tr1 to transition t1 . Construction appropriate for out-of-causal-
order reversing (see Example 3).
Example 3. Consider the nets depicted in Figure 4. Part (a) presents a net
with additional history places and connections (dotted blue), as well as
the additional arcs from t1 and t2 to their input places, and arcs directed
to t1 and t2 from their output places (dashed red). Part (b) shows the net
obtained in (a) (black), with the addition of tr1 being a reverse of t1 and
all needed connections from and to tr1 . Note that the connections marked
in dashed green need to be added according to the de nition of the set
T Pt1 .
The set of variables VC
00 should contain all elements necessary to de-
scribe each input token of every transition (also the reversal ones). The
guard function GC
00 has to be modi ed to take into account reversal tran-
sitions. The conditions used for transitions tri should guarantee that the
transition ti has been executed before reversing its history cannot be
empty, hence its transition history place hi cannot contain an empty list.
During out-of-causal reversing we have to analyse a set of transitions
which use a particular base. Hence, for every base a ∈ A, we de ne a set
of transitions ATa = {t ∈ TC | ∃q∈PR a ∈ EC (q, t)} (Atom's Transitions ).
Therefore ATa contains transitions which require base a to be executed,
i.e. base a is included in the description of at least one input arc of every
transition from ATa .
107
The function EC
00 requires the largest adjustment. It has to describe
the whole procedure of reversing. If transition ti creates a bond a−b then
we need to nd a molecule Z , which contains base a. By the construction
of RP N , only one base of each type can be present. The molecule has to
be found among places from T Pti due to the construction of T Pti . For
every p ∈ T Pti , the arc expressions EC
00(p, tr ) must be de ned to transfer
i
a token from p. If the molecule transferred from p does not contain a,
then it is moved back to p a suitable expression should be added to
EC 00(tri , p). If the molecule contains a, then it is the sought molecule Z .
The following step is to determine a set of bases from the found molecule
C = Z \ {a, b}, connected to a after breaking the bond a−b recall that it
is denoted by con(a, C). Subsequently the last transition executed in the
S
considered computation among transitions from
S c∈con(a,C) ATc \ {ti } has
to be determined (if the set c∈con(a,C) ATc \ {ti } is not empty). This can
be done using a total order represented in a distributed way as markings
of transition history places and connection history places. Later on we
S
take the maximal element from the ordered set c∈con(a,C) ATc \ {ti } and
denote it as ta . We need also to take into account the output place of ta
(from PR ) and we denote it as pa (notice that every transition from TC
S
has only one output place from PR ). If c∈con(a,C) ATc \ {ti } is empty we
take as pa the initial place for base a (a place where a was present in
the initial marking). The molecule con(a, C) should be moved into pa . If
b 6∈ con(a, C) then we repeat the same procedure for b (con(b, C) from Z
and tb should be determined and con(b, C) should be placed into pb ). The
case when ti only transfers base a is almost the same as the previous case,
but con(a, Z) is equivalent to the whole molecule which contains a, hence
similar procedure can be used. Although it seems complicated, all those
operations can be expressed using CPN semantics with the use of graph
operations and included in EC
00(tr , p), where p ∈ P .
i R
One more thing has to be explained in details. Transition tri transfers
con(a, Z) to pa , but how can we be sure that transition tri is connected
to pa ? We know that tri is connected with every place from T Pti and the
following reasoning justi es that pa ∈ T Pti . We assume that transition ti
creates a bond a − b or transfers a base a, and it is reversed. Note that
a ∈ Atomsti according to the de nition of Atomsti . If pa is the initial
place for base a then naturally pa ∈ T Pti . Let us assume that pa is an
output place of transition ta .
If ∃q∈PR a ∈ EC (q, ta ) then transition ta requires base a to be executed
and it cannot consume any base (according to de nition of RPNs), hence
108
it has to put base a into its output place pa . According to the construction
of T Pti , base a can be in place pa , hence pa ∈ T Pti .
Now let us consider the case when ∀q∈PR a ∈
/ EC 00(q, t ). Since t ∈
S a a
AT \ {t } , it must be that ∃ d ∈ E 00(q, t ). The
c∈con(a,C) c i d∈con(a,C) C a
00
molecule in CR can be seen as a graph, where vertices represent bases and
edges bonds. Because d ∈ con(a, C) there exists a path e between a and
d in molecule con(a, C). Let us assume that transition tk has created the
last bond α in e (it has added the last edge to the path). If transition ta
was executed before tk (according to the total order), then ta cannot be the
S S
maximal in the set c∈con(a,C) ATc \{ti }, because tk ∈ c∈con(a,C) ATc \{ti }
(tk has created α between some bases in con(a, C)). If transition ta was ex-
ecuted after tk , then path e between a and d was present in the molecule,
when transition ta was executed. During its execution, transition ta trans-
00
fers base d because d ∈ EC (q, ta ) (it may also transfer it and create a
bond between d and other base). Hence, in the considered execution, it
had to transfer also base a to pa (because a and d are connected). Since
base a was present in pa , according to the de nition, pa ∈ T Pti . If ta = tk ,
transition ta has transferred both bases a and d to pa to add the last bond
present in path e, hence pa ∈ T Pti .
For all connection history places hjk the arc expression EC
00(h , tr )
jk i
should include the relocation of a token from hjk , because it is necessary
to extract the total order of transitions' executions. If i 6= j and i 6= k then
the token is not changed and put back into hjk it should be expressed
by EC
00(tr , h ). If i = j or i = k then E 00(tr , h ) has to contain an
i jk C i jk
expression decreasing the value of the token from hjk by 1 and transferring
it to hjk .
For the transition history place hi related to transition ti (the transi-
tion to be reversed) information about the last execution of the transition
should be removed from the token and this operation should be described
by EC
00(tr , h ) and E (h , tr ). Since the considered PN is acyclic, the last
i i C i i
execution is the only one. Hence, after the execution of tri , hi has to con-
tain only an empty list. For the other transition history places hj , i 6= j ,
00(h , tr ) should include transfer of a token from h .
the arc expression EC j i j
00
The expression EC (tri , hj ) should contain the modi cation of the token
value. Since the last execution of transition ti has not yet been reversed,
the triple (n, i, j) is for sure present in the token. We also need to nd a
corresponding triple (m, j, i) in the local history of transition ti obtained
from place hi . If n is larger than m, the arc expression EC
00(tr , h ) should
i j
exchange the value of triple (n, i, j) by (n − 1, i, j). No matter whether
109
the value of the token is modi ed or not, it needs to be transfer back to
the place hj .
8 Conclusions
In this paper we deal with two models of concurrent computations allow-
ing action reversing. Namely, we provide a transformation from reversing
Petri nets into coloured Petri nets. This way we enable backtracking,
causal reversing and out-of-causal-order reversing with the use of the well
known and widely investigated model of coloured Petri nets. The model
can encode reversing Petri nets without the need of a history utilizing
arbitrarily large values nor global control.
As future work we plan on implementing an algorithmic translation
that transforms RPNs to CPNs in an automated manner using the trans-
formation techniques discussed in this paper. Another goal is to investigate
systems which allow cycles. Note that the addition of cycles can in fact
be achieved within RPNs by adopting stack histories for each transition
that record all previous occurrences of a transition that is inside a cy-
cle and it remains to be seen how this type of histories can be encoded
within the CPN model. We also aim to explore how our framework ap-
plies in elds outside computer science, since the expressive power and
visual nature oered by Petri nets coupled with reversible computation
has the potential of providing an attractive setting for analysing systems
(for instance in biology, chemistry or hardware engineering).
References
1. K. Barylska, M. Koutny, . Mikulski, and M. Pi¡tkowski. Reversible computation
vs. reversibility in Petri nets. Science of Computer Programming, 151:4860, 2018.
2. K. Barylska, . Mikulski, M. Pi¡tkowski, M. Koutny, and E. Erofeev. Reversing
transitions in bounded Petri nets. Fundamenta Informaticae, 157:341357, 2018.
3. L. Cardelli and C. Laneve. Reversible structures. In Proceedings of CMSB 2011,
pages 131140. ACM, 2011.
4. CPN Tools project website, http://cpntools.org/.
5. V. Danos and J. Krivine. Reversible communicating systems. In Proceedings of
CONCUR 2004, LNCS 3170, pages 292307. Springer, 2004.
6. V. Danos and J. Krivine. Transactions in RCCS. In Proceedings of CONCUR
2005, LNCS 3653, pages 398412. Springer, 2005.
7. V. Danos and J. Krivine. Formal molecular biology done in CCS-R. Electronic
Notes in Theoretical Computer Science, 180(3):3149, 2007.
8. K. Jensen and L. M. Kristensen. Coloured Petri Nets - Modelling and Validation
of Concurrent Systems. Springer, 2009.
9. S. Kuhn and I. Ulidowski. A calculus for local reversibility. In Proceedings of RC
2016, LNCS 9720, pages 2035. Springer, 2016.
110
10. R. Landauer. Irreversibility and heat generation in the computing process. IBM
Journal of Research and Development, 5(3):183191, 1961.
11. I. Lanese, M. Lienhardt, C. A. Mezzina, A. Schmitt, and J. Stefani. Concurrent
exible reversibility. In Proceedings of ESOP 2013, LNCS 7792, pages 370390.
Springer, 2013.
12. I. Lanese, C. A. Mezzina, and J. Stefani. Reversibility in the higher-order π -
calculus. Theoretical Computer Science, 625:2584, 2016.
13. T. Murata. Petri nets: Properties, analysis and applications. InProceedings of the
IEEE 77.4, 541580, 1989.
14. A. Philippou and K. Psara. Reversible computation in Petri nets. To appear in
the Proceedings of RC 2018.
15. I. Phillips and I. Ulidowski. Reversing algebraic process calculi. In Proceedings of
FOSSACS 2006, LNCS 3921, pages 246260. Springer, 2016.
16. I. Phillips, I. Ulidowski, and S. Yuen. A reversible process calculus and the mod-
elling of the ERK signalling pathway. In Proceedings of RC 2012, LNCS 7581,
pages 218232. Springer, 2012.
17. I. Phillips, I. Ulidowski, and S. Yuen. Modelling of bonding with processes and
events. In Proceedings of RC 2013, LNCS 7947, pages 141154. Springer, 2013.
18. A. V. Ratzer, L. Wells, H. M. Lassen, M. Laursen, J. F. Qvortrup, M. S. Stissing,
M. Westergaard, S. Christensen, and K. Jensen. CPN tools for editing, simulating,
and analysing coloured Petri nets. In Proceedings of ICATPN 2003, LNCS 2679,
pages 450462. Springer, 2003.
19. W. Reisig. Understanding Petri Nets - Modeling Techniques, Analysis Methods,
Case Studies. Springer, 2013.
20. I. Ulidowski, I. Phillips, and S. Yuen. Concurrency and reversibility. In Proceedings
of RC 2014, LNCS 8507, pages 114. Springer, 2014.
111