In: Lecture Notes in Computer Science, Vol. 1346: Foundations of Software Technology and Computer Science, pages 327-341. Springer-Verlag, 1997.
Abstract: It is commonly known that every reachable marking of a finite state Petri net system is represented in its finite unfolding according to McMillan. Also the reachability of markings from each other is represented in the finite unfolding, but it is almost unknown that this information can be hidden very deep. This paper presents an efficient method for gaining this information, which is of course of great importance for potential model checkers working on finite unfoldings. All results presented in this paper also hold for a recently proposed optimized unfolding method.
Keywords: Petri nets, finite net unfoldings, reachability properties.