Reversing Computations Modelled by Coloured Petri Nets

Abstract

Reversible computation is an unconventional form of computing where any sequence of performed operations can be executed in reverse order at any point during computation. It has recently been attracting 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-causalorder reversing), to Coloured Petri Nets (CPNs), an extension of traditional 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 computation, can be emulated in CPNs. The transformation can be automated and utilized for the analysis of reversible systems using CPN Tools.