Decision Problems for Petri Nets with Names

11 years 12 months ago
Decision Problems for Petri Nets with Names
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 prove that -PN are Well Structured Transition Systems. In particular, we obtain decidability of coverability and termination, so that the expressive power of Turing machines is not reached. Moreover, they are strictly Well Structured, so that the boundedness problem is also decidable. We consider two properties, width-boundedness and depth-boundedness, that factorize boundedness. Width-boundedness has already been proved to be decidable. We prove here undecidability of depth-boundedness. Finally, we obtain Ackermann-hardness results for all our decidable decision problems. Key words: Petri nets, pure names, Well Structured Transition Systems, decidability
Fernando Rosa Velardo, David de Frutos-Escrig
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2010
Where CORR
Authors Fernando Rosa Velardo, David de Frutos-Escrig
Comments (0)