Bi-reachability in Petri nets with data

TL;DR

This paper studies Petri nets with data, providing a decision procedure for bi-reachability, which advances understanding of the boundary between decidable and undecidable properties in these models.

Contribution

It introduces a decision procedure for bi-reachability in Petri nets with data, extending the analysis of reachability problems in these systems.

Findings

Decidability of bi-reachability in Petri nets with data.

Bi-reachability subsumes coverability and is subsumed by reachability.

Advances the boundary of decidability in Petri nets with data.

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