从可逆 Petri 网到有色 Petri 网的正式翻译

可逆计算是一种新兴的计算范式，允许在计算过程中的任意时刻按逆序执行任何操作序列。其吸引力在于低功耗计算的潜力，以及其与化学反应、量子计算、机器人与分布式系统等广泛的相关性。可逆 Petri 网是最近提出的 Petri 网扩展，实现了三种主要的可逆形式，即回溯、因果可逆与超因果序可逆。其特征是使用可组合形成键的命名令牌。命名令牌与历史函数一起，构成了记忆过去行为的手段，从而实现逆转。在近期工作中，我们提出了从一类可逆 Petri 网（RPN）到有色 Petri 网（CPN）模型的结构化翻译，CPN 是传统 Petri 网的扩展，其中令牌携带数据值。本文扩展了该翻译以处理在个体令牌解释下具有令牌多重性的 RPN，该模型允许系统中存在多个同类型令牌。为支持三种可逆类型，令牌与其因果历史相关联，并且虽然同类型令牌在前向触发转移时具有同等资格，但在反向时仅能逆转其先前已触发的转移。新翻译除了解除令牌唯一性限制外，还提出了一种通过统一方法将 RPN 转换为 CPN 的精炼方法，该方法可实例化三种可逆类型中的每一种。本文还报告了一个实现该翻译的工具，为使用 CPN Tools 进行可逆系统的自动化翻译与分析铺平了道路。