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 identied 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. Specically, 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. Specically, 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) dened in [14] together with the basic denitions 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 conict 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 dened as follows: Denition 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 denition 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. Denition 2. A reversing Petri net is well-formed, if it satises 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 denition diers from Denition 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, conict 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. Denition 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 dene the eect of a transition as effect(t) = post(t) − pre(t). Remark 2. Note that the above denition contains one less clause than the associated denition from [14] (denition 3 ibidem). This clause has become obsolete by the adoption of Clause 4. in the denition of well- formedness of the present paper, forbidding forks in RPNs. Denition 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 Deni- 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: Denition 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: Denition 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 dened as follows. Denition 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: Denition 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 Denition 6. We reverse transitions in causal reversing semantics in the same man- ner as in the backtracking semantics (Denition 6). 3.3 Out-of-causal-order Reversing We are now ready to dene out-of-causal-order reversing enabledness. Denition 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 denition, in this setting, every transition which has been executed can be reversed. The following notion helps to dene the last executed transition manipulating a given set of tokens, where we write ⊥ to express that the value is undened. Denition 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 Denition 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 dened as in Denition 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 innite 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. Denition 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 dened 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 full 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 Denition 1, to an equivalent CPN. As a rst step we consider the history function H , which we transform into a set of additional places. Specically, 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 dened 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 dened 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 renement 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. Denition 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 modied 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 dene 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 dene 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 dene 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 dene 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 denition 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 modied 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 dene 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 dened 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 justies 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 denition 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 denition 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 denition, 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 modication 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 modied 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