Bi-reachability in Petri nets with data

Petri nets with equality data is 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. The most fundamental decision problem for Petri nets, the reachability problem, asks, given a net together with source and target configurations, if there is a run from source to target. The decidability status of this problem for equality data still remains an intriguing open question. On the other hand, the coverability problem (where we ask if there is a run from source to a configuration that possibly extends target by some extra tokens) is decidable for equality data. As widely known, coverability easily reduces to reachability. Furthermore, the reachability problem is decidable for equality data, in the special case of reversible Petri nets (where transitions are closed under reverse), as recently shown by Ghosh and Lasota.

We study a relevant decision problem, sandwiched between reachability and the two latter decidable ones: the bi-reachability problem. It asks, for a net and two its configurations, if each of the configurations is reachable from the other one. In other words, the problem asks if two given configurations are in the same bi-reachability equivalence class. As our main result we prove decidability of this problem for equality data domain. This pushes further the decidability border for Petri nets with equality data. The decision procedure for bi-reachability is inspired by the classical decomposition approach used to decide reachability in plain Petri nets.

This is a joint work with Sławek Lasota.