In: Lecture Notes in Computer Science, Vol. 1091; Proc. 17th International Conference in Application and Theory of Petri Nets (ICATPN'96), Osaka, Japan, pages 346-365. Springer-Verlag, June 1996.
Abstract: This paper suggests a way for Petri Net analysis by checking the ordering relations between places and transitions. The method is based on unfolding the original net into an equivalent acyclic description. In an unfolding the ordering relations can be determined directly by the structure of an underlying graph. We improved on the previously known cutoff criterion for truncating the unfolding. No restrictions are imposed on the class of general PNs. The new criterion significantly reduces the size of unfolding obtained by PN. The PN properties for analysis can be various: boundedness, safety, persistency etc. The practical example of the suggested approach is given in application to the asynchronous design. The circuit behavior is specified by an interpreted Petri net, called Signal Transition Graph (STG) which is then analyzed for the implementability by asynchronous hazard-free circuit. The implementability conditions are formulated in such a way that they can be checked by analysis of ordering relations between signal transitions rather than by traversal of states. This allows avoiding the state explosion problem for highly parallel specifications. The experimental results show that for highly parallel STGs checking the implementability by unfolding is one to two orders of magnitude less time-consuming than checking it by symbolic BDD traversal of the corresponding State Graph.
Back to the Petri Nets Bibliography