Combining structural and enumerative techniques for the validation of bounded petri nets

Abstract

We propose a new validation algorithm for bounded Petri Nets. Our method combines state enumeration and structural techniques in order 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 behaviors. 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 allows 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 [ABC+95, CM97, MCC97]. Our algorithm returns exact results in all the 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 specification of the initial marking. © Springer-Verlag Berlin Heidelberg 2001.