Symbolic computation of boundary unsafe states in complex resource allocation systems using partitioning techniques

In some recent work, we proposed a binary decision diagram (BDD-) based approach for the development of the maximally permissive deadlock avoidance policy (DAP) for complex resource allocation systems (RAS), that is based on the identification and the explicit storage of a set of critical states in the underlying RAS state-space. The work presented in this paper seeks to extend the applicability of the aforementioned results by coupling them with a partitioning technique for the more efficient storage and processing of the BDD that encodes the underlying state space. The reported numerical experimentation demonstrates the increased efficiency of the new algorithm w.r.t. its space and time complexity, compared to the previous method that uses a more monolithic representation of the RAS state-space. The last part of the paper also discusses some further potential advantages of the presented method, including its amenability to a parallelized implementation and its ability to cope effectively and efficiently with uncontrollable behavior.