The deadlock structure character in Petri net models of Sequential Resource Allocation Systems with Multiple Resource Acquisitions and Flexible Routings

Sequential Resource Allocation Systems with Multiple Resource Acquisitions and Flexible Routings ((C/D)RAS) are a kind of common system with higher complexity. This paper concerns the Petri net models of (C/D)RAS named marked S³PGR² (N,M₀). The concepts of marked modified S³PGR² nets and cyclic structures are introduced. It is addressed that the cyclic structure can reflect the situation of resource maintenance and the cyclic waiting. Hence force, cyclic structures are the character structures of occurrence of system deadlocks. The transaction is described in detail as follows. If (N,M₀)is not live, it must has a reachable marking M, which is a partial deadlock, i.e., there is a deadlock transition. A total deadlock M1 can be derived in the marked modified S³PGR² net (N_m, M). As a matter of fact, M1 can also be reached in (N,M₀). Finally, it is proved that a cyclic structure can be located in (N,M₁).