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

翻译：我们研究带数据的Petri网——这是普通Petri网的扩展模型，其中令牌携带来自无限数据域的值，且变迁的可执行性受数据值间的等值条件约束。针对双向可达性问题，我们提出了一种判定程序：给定一个Petri网及其两个配置，判断这两个配置是否能够相互可达。这一研究推进了可判定性边界，因为双向可达性问题既涵盖可覆盖性问题（已知可判定），又被可达性问题所包含（其可判定性尚未明确）。