A reachability graph construction algorithm based on canonical transition firing count vectors

The construction of the reachability graph 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-net models. We define the main concept for this new marking representation, then we present performance results in terms of comparisons of space and time resources against the standard GreatSPN (Great Stochastic Petri Nets) solver.