Bi-reachability in Petri nets with data

TL;DR

The paper addresses mutual reachability (bi-reachability) for configurations in Petri nets with data under equality data, establishing decidability by translating to data vector addition systems with states (dvass). It introduces a two-part strategy: a testable sufficient condition for bi-reachability and a rank-based reduction algorithm that iteratively simplifies the dvass while preserving bi-reachability until a decidable base case is reached. The approach leverages orbit-finite representations, a Kosaraju-inspired decomposition, and computable coverability tools to drive correctness and termination. This work pushes the decidability boundary beyond coverability and reversible reachability in equality-data Petri nets, while highlighting open challenges for ordered data and the general reachability problem.

Abstract

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).

Figures (1)

• Figure 1: A Petri net with equality data, with places $\left\{p_1, p_2\right\}$ and transitions $\left\{t_1, t_2\right\}$. The shown configuration engages 5 tokens, carrying 3 different data values, depicted through different colors.

Theorems & Definitions (31)

• lemma 1: GHL23
• remark 1
• theorem 1
• proof
• lemma 2: Thm. 2 in Kosaraju82, Prop. 1 in Las3steps
• proof
• lemma 3
• proof
• lemma 4
• proof