Issue No. 05 - May (1994 vol. 20)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.286423
<p>Petri nets have been proposed as a promising tool for modeling and analyzing concurrent-software systems such as Ada programs and communication protocol software. Among analysis techniques available for Petri nets, the most general approach is to generate all possible states (markings) of the system in a form of a so-called reachability graph. However, this conventional reachability graph approach is inefficient or intractable, even for a bounded Petri net, due to state explosion in many practical applications. To cope with this problem, this paper proposes a method for constructing a hierarchically organized state space called the hierarchical reachability graph (HRG). Using the HRG, we obtain necessary and sufficient conditions for reachability and deadlock, as well as algorithms to test whether a given state or marking is reachable from the initial state and whether there is a deadlock state (a state with no successor states)</p>
Petri nets; state-space methods; multiprocessing programs; software engineering; hierarchical systems; hierarchical reachability graph; bounded Petri nets; concurrent-software analysis; Ada programs; communication protocol software; markings; state explosion; efficiency; tractability; hierarchically organized state space; deadlock state; successor states
T. Murata and M. Notomi, "Hierarchical Reachability Graph of Bounded Petri Nets for Concurrent-Software Analysis," in IEEE Transactions on Software Engineering, vol. 20, no. , pp. 325-336, 1994.