Bi-reachability in Petri nets with data

要約

私たちは、トークンが無限のデータ ドメインからの値を運び、遷移の実行可能性がデータ値間の等価性によって条件付けられる、プレーン ペトリ ネットの拡張であるデータ付きペトリ ネットを調査します。
双方向到達可能性の問題に対する決定手順を提供します。ペトリ ネットとその 2 つの構成が与えられた場合、各構成が相互に到達可能かどうかを尋ねます。
これは、双方向到達可能性問題がカバービリティ問題 (決定可能であることがわかっている) を包含し、到達可能性問題 (決定可能性のステータスが不明) に包含されるため、決定可能性の境界線を押し上げます。

要約(オリジナル)

We investigate Petri nets with data, an extension of plain Petri nets where tokens carry values from an infinite data domain, and executability of transitions is conditioned by equalities between data values. We provide a decision procedure for the bi-reachability problem: given a Petri net and its two configurations, we ask if each of the configurations is reachable from the other. This pushes forward the decidability borderline, as the bi-reachability problem subsumes the coverability problem (which is known to be decidable) and is subsumed by the reachability problem (whose decidability status is unknown).

arxiv情報

提供元, 利用サービス

arxiv.jp, Google