A graph theoretical approach to the performance analysis of highly concurrent systems.

We present an algorithm which, in order to characterize the deadlock states, analyzes the invariants and the reachability graph $G$ of a Petri Net (PN). Our idea is to investigate the strong commonality between the transition invariants of the net, associated with circuits in $G$, and the concurrent processes, associated with different paths in $G$ from the initial state of the system. In particular, starting from $G$, we determine a subgraph $L$, called “restricted live reachability graph”, containing all and only the deadlock-free states of the system. Such a graph is shown to be a unique Strongly Connected Component (SCC). In this paper, the basic steps of our algorithm are presented along with an application to the performance analysis of a highly concurrent manufacturing system