Hierarchical reachability graph generation for Petri nets

Reachability analysis is the most general approach to the analysis of Petri nets. Due to the well-known problem of state-space explosion, generation of the reachability set and reachability graph with the known approaches often becomes intractable even for moderately sized nets. This paper presents a new method to generate and represent the reachability set and reachability graph of large Petri nets in a compositional and hierarchical way. The representation is related to previously known Kronecker-based representations, and contains the complete information about reachable markings and possible transitions. Consequently, all properties that it is possible for the reachability graph to decide can be decided using the Kronecker representation. The central idea of the new technique is a divide and conquer approach. Based on net-level results, nets are decomposed, and reachability graphs for parts are generated and combined. The whole approach can be realized in a completely automated way and has been integrated in a Petri net-based analysis tool.