Structural analysis of resource allocation systems with synchronization constraints

The work presented in this paper extends recently developed in the theory of resource allocation systems (RAS) to RAS behaviors that present synchronization requirements in the underlying process flows. More specifically, the paper first provides a formal definition of the considered RAS structures and behaviors by introducing the Petri net sub-class of generalized augmented marked graphs (G-AMG), and subsequently, it proceeds to the analysis of the liveness properties of the resource allocation underlying the G-AMG operation. It is shown that similar to the case of some previously studied RAS structures, non-liveness of the resource allocation taking place in the G-AMG context can be attributed to a structural object known as resource-induced deadly marked siphon, that is developed in a properly defined projection of the net reachability space. Beyond its theoretical significance in terms of formally characterizing and understanding the nature of deadlock or livelock that can occur in the considered resource allocation context, the aforementioned result is also deemed to be important from the practical standpoint of synthesizing liveness-enforcing supervisors (LES), since it is expected to enable LES synthesis through application of the correctness verification methodology originally developed in (J. Park and S. Reveliotis, 2001); the actual potential of this approach is currently under investigation.