In: IEICE Trans. on Fundamentals in Electronics, Communications and Computer Science, Vol. E79-A, No. 11, pages 1809-1816. 1996.
Abstract: Petri nets are widely recognized as a powerful model for discrete event systems. Graphical features of nets provide an environment to design and to comprehend discrete event systems. Mathematical aspects of nets provide methods for analysis for verification properties of such systems. Several analysis techniques have been proposed, such as reachability analysis, a matrix equation approach. reduction or decomposition methods, a symbolic model method, and an unfolding method. The unfolding method was introduced to avoid generating the reachability graph. Unfoldings are often focused on an analysis of finite state systems, i.e., bounded nets, and discuss a reachability problem and an upper bound problem. Relations between these two problems and an unfolding have been clarified to provide a novel method the resolve these problems.
Keywords: Petri nets, discrete event systems, net unfolding, occurrence nets, reachability analysis.