Reversible computation is an emerging computing paradigm that allows any sequence of operations to be executed in reverse order at any point during computation. Its appeal lies in its potential for lowpower computation and its relevance to a wide array of applications such as chemical reactions, quantum computation, robotics, and distributed systems. Reversing Petri nets are a recently-proposed extension of Petri nets that implements the three main forms of reversibility, namely, backtracking, causal reversing, and out-of-causal-order reversing. Their distinguishing feature is the use of named tokens that can be combined together to form bonds. Named tokens along with a history function, constitute the means of remembering past behaviour, thus, enabling reversal. In recent work, we have proposed a structural translation from a subclass of RPNs to the model of Coloured Petri Nets (CPNs), an extension of traditional Petri nets where tokens carry data values. In this paper, we extend the translation to handle RPNs with token multiplicity under the individual-token interpretation, a model which allows multiple tokens of the same type to exist in a system. To support the three types of reversibility, tokens are associated with their causal history and, while tokens of the same type are equally eligible to fire a transition when going forward, when going backwards they are able to reverse only the transitions they have previously fired. The new translation, in addition to lifting the restriction on token uniqueness, presents a refined approach for transforming RPNs to CPNs through a unifying approach that allows instantiating each of the three types of reversibility. The paper also reports on a tool that implements this translation, paving the way for automated translations and analysis of reversible systems using CPN Tools.

翻译：逆向计算是一种新兴的计算范式，允许在计算的任意阶段以逆序执行任何操作序列。其优势在于低功耗计算的潜力，并广泛应用于化学反应、量子计算、机器人和分布式系统等领域。逆向Petri网是近期提出的Petri网扩展，实现了三种主要的可逆形式，即回溯、因果逆序和超因果逆序。其显著特征在于使用可相互结合形成键的命名令牌。命名令牌与历史函数共同构成了记忆过去行为的手段，从而支持逆向操作。在之前的工作中，我们提出了一种从RPNs子类到着色Petri网（CPNs）模型的结构化翻译——CPNs是传统Petri网的扩展，其中令牌携带数据值。本文将该翻译扩展至处理个体令牌解释下具有令牌多重性的RPNs，这种模型允许系统中存在多个同类型令牌。为支持三种可逆类型，令牌关联其因果历史：前向推进时同类型令牌具有相同的使能过渡资格，而逆向回溯时仅能逆转其先前激发过的过渡。新翻译不仅消除了令牌唯一性的限制，还通过统一方法实现了对三种可逆类型的实例化，从而完善了RPNs到CPNs的转换。本文同时报告了实现该翻译的工具，为使用CPN Tools进行可逆系统的自动化翻译与分析铺平了道路。