In: Lecture Notes in Computer Science, Vol. 1346: Foundations of Software Technology and Computer Science, pages 312-326. Springer-Verlag, 1997.
Abstract: The technique of polynomial-time many-one reductions is applied to Petri net theory. Boundedness, reachability, deadlock, liveness and some of their variations are studied. Three main results are derived. Firstly, the power of expression of reachability which can polynomially give evidence of unboundedness, is highlighted. Secondly, it is proven that reachability and deadlock are polynomially-time equivalent; this improves the known recursive reduction and it complements the result of Cheng and al. Moreover, the polynomial equivalence of liveness and t-liveness is shown. Hence, the problems are regrouped in three main classes: boundedness, reachability and liveness. Finally, an upper bound on the boundedness for post self-modified nets is given; this improves a decidability result of Valk.
Keywords: Petri nets, computational complexity, program verification.
Back to the Petri Nets Bibliography