In: Margaria, T.; Steffen, B.: Lecture Notes in Computer Science, Vol. 1055; Tools and Algorithms for the Construction and Analysis of Systems, Second Int. Workshop, TACAS'96, Passau, Germany, pages 87-106. Springer-Verlag, March 1996.
Abstract: McMillan has recently proposed a new technique to avoid the state explosion problem in the verification of systems modelled with finite-state Petri nets. The technique requires to construct a finite initial part of the unfolding of the net. McMillan's algorithm for this task may yield initial parts that are larger than necessary (exponentially larger in the worst case). We present a refinement of the algorithm which overcomes this problem.