Hierarchically organized Petri net state space for reachability and deadlock analysis

Petri nets are a versatile tool for modeling and analyzing parallel and distributed computing systems. However state explosion is a major impediment to their analysis and practical applications. To cope with this problem, this paper proposes a method for constructing hierarchically organized state space (HOSS) of a bounded Petri net. Using the HOSS, the authors obtain necessary and sufficient conditions for reachability and deadlock, and algorithms to test if a given state (marking) is reachable from the initial state and if there is a deadlock state (a state with no successor states)