In: Proceedings of Applications and Theory of Petri Nets 2004: 25th International Conference, ICATPN 2004, Bologna, Italy, June 21-25, 2004, pages 17-34. Volume 3099 of Lecture Notes in Computer Science / Cortadella, Reisig (Eds.) --- Springer-Verlag, September 2004.
Abstract: Generating the reachability set is one of the most commonly required step when analyzing the logical or stochastic behavior of a system modeled with Petri nets. Traditional "explicit" algorithms that explore the reachability graph of a Petri net require memory and time at least proportional to the number of reachable markings, thus they are applicable only to fairly small systems in practice. Symbolic "implicit" algorithms, typically implemented using binary decision diagrams, have been successfully employed in much larger systems, but much of the work to date is based on breadth-first search techniques best suited for synchronous hardware verification. Here, instead, we describe recently-introduced data structures and algorithms particularly targeted to Petri nets and similar asynchronous models, and show why they are enormously more efficient for this application. We conclude with some directions for future research.