Efficient reachability set generation and storage using decision diagrams

Abstract

We present a new technique for the generation and storage of the reachability set of a Petri net. Our approach is inspired by previous work on Binary and Multi-valued Decision Diagrams but exploits a concept of locality for the effect of a transition’s firing to vastly improve algorithmic performance. The result is a data structure and a set of manipulation routines that can be used to generate and store enormous sets extremely efficiently in terms of both memory and execution time.