For the most recent entries see the Petri Nets Newsletter.

Symbolic, Symmetry, and Stubborn Set Searches.

Tiusanen, M.

In: Valette, R.: Lecture Notes in Computer Science, Vol. 815; Application and Theory of Petri Nets 1994, Proceedings 15th International Conference, Zaragoza, Spain, pages 511-530. Springer-Verlag, 1994.

Abstract: The state space explosion problem is the proliferation of states to be considered during the verification of a finite state system. This paper proposes ways to combine methods that have successfully been used to alleviate this problem during the reachability analysis of safe Petri nets (or ones with known bounds for all places): symbolic model checking employing data stsructures for binary-decision diagrams (BDDs), the symmetry equivalence method of Jensen et al, and the stubborn set method of Valmari. The use of Petri nets as the basis extends the scope of the BDD-based analysis beyond hardware verification. The reachability graph of Petri nets is slightly generalized to allow for multiple initial markings, in order to correspond to the symbolic state space search using BDDs. The generalization is useful in itself if the initial marking of the system is not fully defined, e.g. for fault-tolerant systems. A subborn set selection algorithm of Valmari is generalized to apply to sets of current markings instead of one marking at a time. This will provide the combination of the subborn set method and symbolic state space generation using BDD. The combination of the symmetry equivalence method with the stubborn set method is discussed: this turn out to be as straightforward as claimed by Valmari. Using BDDs to benefit in the symmetry equivalence method is also discussed


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography