A graph theoretic approach to reachability problem with Petri net unfoldings

Petri nets are widely recognized as a powerful model for discrete event systems. Petri nets have both graphical and mathematical features. Graphical feature provides an environment to design and to comprehend discrete event systems. Mathematical feature provides an analysis power for verifying several properties of such systems. Several analysis techniques have been proposed so far, such as a reachability (coverability) graph method, a matrix equation approach, reduction or decomposition techniques, a symbolic model method and an unfolding method. The unfolding method was introduced to avoid generating the reachability graph. Unfoldings are often used in the verification of asynchronous circuits. This paper focuses on an analysis of finite state systems, i.e., bounded nets, and discuss a reachability problem and a upper bound problem. Relations between these problems and an unfolding have been clarified to provide a novel method to resolve these problems.