State Space Characterization of Disjunctive Single-Unit Resource Allocation Systems

A deluge of approaches has been proposed to implement and deploy a computationally effective and maximally permissive liveness-enforcing supervisor for sequential resource allocation systems (RASs). However, they are stalled by the computational complexity of a large state space that grows exponentially with respect to the size of an underlying RAS. The attention of this work is restricted to a special class of RASs: Disjunctive/Single-unit (D/SU)-RASs. Given an initial resource configuration of a D/SU-RAS, a complete state enumeration can be obtained through pure algebraic operations on this configuration with the pre-computed initial basis state space. When an explicit and complete enumeration of reachable states is impossible (due to the limited memory and storage space), we propose the exact number of reachable states. In this case, given a state vector, its reachability can be decided by an algebraic method. Experimental studies demonstrate the efficiency of the proposed approach.