Acyclic and Cyclic Reversing Computations in Petri Nets

Reversible computations constitute an unconventional form of computing whereany sequence of performed operations can be undone by executing in reverseorder at any point during a computation. It has been attracting increasingattention as it provides opportunities for low-power computation, being at thesame time essential or eligible in various applications. In recent work, wehave proposed a structural way of translating Reversing Petri Nets (RPNs) - atype of Petri nets that embeds reversible computation, to bounded ColouredPetri Nets (CPNs) - an extension of traditional Petri Nets, where tokens carrydata values. Three reversing semantics are possible in RPNs: backtracking(reversing of the lately executed action), causal reversing (action can bereversed only when all its effects have been undone) and out of causalreversing (any previously performed action can be reversed). In this paper, weextend the RPN to CPN translation with formal proofs of correctness. Moreover,the possibility of introduction of cycles to RPNs is discussed. We analyzewhich type of cycles could be allowed in RPNs to ensure consistency with thecurrent semantics. It emerged that the most interesting case related to cyclesin RPNs occurs in causal semantics, where various interpretations of dependencyresult in different net's behaviour during reversing. Three definitions ofdependence are presented and discussed.Comment: arXiv admin note: text overlap with arXiv:2101.07066 by other author