In: T. Margaria and W. Yi: Lecture Notes in Computer Science, Vol. 2031: 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2001, Genova, Italy. Springer., pages 435-449. April 2001.
Abstract: We propose a new validation algorithm for bounded Petri Nets. Our method combines state enumeration and structural techniques inorder to compute under-approximations of the reachability set and graph of a net. The method is based on two heuristics that exploit properties of T-semiflows to detect acyclic behaviours. T-semiflows also give us an heuristic estimation of the number of levels of the reachability graph we have to keep in memory during forward exploration. This property allow us to organize the space used to store the reachable markings as a circular array, reusing all markings outside a sliding window containing a fixed number of the last levels of the graph. We apply the method to examples taken from the literature. Our algorithm returns exact results in all experiments. In some examples, the circular memory allow us to save up to 98% of memory space and to scale up to 255 the number of tokens in the specificacion of the initial marking.
Back to the Petri Nets Bibliography