Symbolic, symmetry, and stubborn set searches
Mikko Tiusanen · Lecture notes in computer science · 1994
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 structures for binary-decision diagrams (BDDs), the symmetry equivalence method of Jensen et al, and the stubborn set method of Valmari.