Complexity of the deadlock problem for Petri nets modeling resource allocation systems

Petri nets are widely used to model and analyze Resource Allocation Systems (RASs). Since they are a kind of structuralized formal method, they can well describe the allocation/release of resources and their markings can directly reflect whether an RAS enters a (partial) deadlock caused by misallocating resources. In general, the key step of preventing/avoiding deadlocks is to decide if deadlocks occur or not in an RAS. This paper is about the complexity of deciding the deadlock problem for Petri nets modeling RAS. We define a very general class of Petri nets called Petri Nets of Resource Allocation (PNRA) to model as many RASs as possible. PNRAs not only focus on the resources shared by processes also pay attention to the interaction/collaboration among processes. We show that the deadlock problem is PSPACE-complete for PNRAs. This paper also proves that for the well-known G-system as a subclass of PNRAs, the deadlock problem is NP-complete.