Decidability and complexity of Petri nets with unordered data

Abstract

We prove several decidability and undecidability results for ν-PN, an extension of P/T nets with pure name creation and name management. We give a simple proof of undecidability of reachability, by reducing reachability in nets with inhibitor arcs to it. Thus, the expressive power of ν-PN strictly surpasses that of P/T nets. We encode ν-PN into Petri Data Nets, so that coverability, termination and boundedness are decidable. Moreover, we obtain Ackermann-hardness results for all our decidable decision problems. Then we consider two properties, width-boundedness and depth-boundedness, that factorize boundedness. Width-boundedness has already been proven to be decidable. Here we prove that its complexity is also non-primitive recursive. Then we prove undecidability of depth-boundedness. Finally, we prove that the corresponding “place version” of all the boundedness problems is undecidable for ν-PN. These results carry over to Petri Data Nets.