A BDD-Based Approach for Designing Maximally Permissive Deadlock Avoidance Policies for Complex Resource Allocation Systems

In order to develop a computationally efficient implementation of the maximally permissive deadlock avoidance policy (DAP) for complex resource allocation systems (RAS), a recent approach focuses on the identification of a set of critical states of the underlying RAS state-space, referred to as minimal boundary unsafe states. The availability of this information enables an expedient one-step-lookahead scheme that prevents the RAS from reaching outside its safe region. The work presented in this paper seeks to develop a symbolic approach, based on binary decision diagrams (BDDs), for efficiently retrieving the (minimal) boundary unsafe states from the underlying RAS state-space. The presented results clearly demonstrate that symbolic computation enables the deployment of the maximally permissive DAP for complex RAS with very large structure and state-spaces with limited time and memory requirements. Furthermore, the involved computational costs are substantially reduced through the pertinent exploitation of the special structure that exists in the considered problem. Note to Practitioners-A key component of the real-time control of many flexibly automated operations is the management of the allocation of a finite set of reusable resources among a set of concurrently executing processes so that this allocation remains deadlock-free. The corresponding problem is known as deadlock avoidance, and its resolution in a way that retains the sought operational flexibilities has been a challenging problem due to: (i) the inability to easily foresee the longer-term implications of an imminent allocation and (ii) the very large sizes of the relevant state spaces that prevent an online assessment of these implications through exhaustive enumeration. A recent methodology has sought to address these complications through the offline identification and storage of a set of critical states in the underlying state space that renders efficient the safety assessment of any given resourc- allocation. The results presented in this paper further extend and strengthen this methodology by complementing it with techniques borrowed from the area of symbolic computation; these techniques enable a more compressed representation of the underlying state spaces and of the various subsets and operations that are involved in the pursued computation.