Formal Translation from Reversing Petri Nets to Coloured Petri Nets

要約

可逆計算は、計算中の任意の時点で一連の操作を逆の順序で実行できるようにする新しいコンピューティング パラダイムです。
その魅力は、低電力計算の可能性と、化学反応、量子計算、ロボット工学、分散システムなどの幅広いアプリケーションとの関連性にあります。
逆ペトリ ネットは、最近提案されたペトリ ネットの拡張であり、可逆性の 3 つの主な形式、つまりバックトラッキング、因果関係の逆転、および因果関係の順序外の逆転を実装します。
それらの際立った特徴は、結合を形成するために結合できる名前付きトークンの使用です。
名前付きトークンと履歴機能は、過去の行動を記憶する手段を構成し、逆転を可能にします。
最近の研究では、RPN のサブクラスから、トークンがデータ値を運ぶ従来のペトリ ネットの拡張であるカラー ペトリ ネット (CPN) のモデルへの構造変換を提案しました。
この論文では、システム内に同じタイプの複数のトークンが存在できるようにするモデルである個別トークン解釈の下で、トークンの多重度を持つ RPN を処理できるように変換を拡張します。
3 つのタイプの可逆性をサポートするために、トークンはその因果関係の履歴に関連付けられており、同じタイプのトークンは前進する場合には同様に遷移を起動する資格がありますが、後退する場合には以前に起動した遷移のみを元に戻すことができます。
新しい翻訳では、トークンの一意性に関する制限を解除することに加えて、3 種類の可逆性のそれぞれをインスタンス化できる統合アプローチを通じて、RPN を CPN に変換するための洗練されたアプローチが示されています。
この論文では、この変換を実装するツールについても報告し、CPN ツールを使用した可逆システムの自動変換と分析への道を開きます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google