In: Proceedings of 9th International Workshop on Petri Nets and Performance Models, PNPM'01 Aachen, Sept. 11-14, 2001, Reinhard German and Boudewijn Haverkort (eds.), IEEE, pages 113-122. 2001.
Abstract: The construction of the reachability grah presents the problem that its size may grow exponentially with respect to the size of the Petri net model. For this reason all available tools suffer restrictions due to the limitation of the available computational resources. We present a new, efficient algorithm based on a data structure that encodes canonical firing count vectors starting from the initial marking rather than token distributions. Our new algorithm applies to bounded and consistent Petri nets models. We define the main concept for this new marking representation, then we present performance results in term of comparison in space and time resources against the standard GreatSPN solver.