Liveness enforcing supervision for resource allocation systems with forbidden states and uncontrollable events

Although liveness enforcing supervision (LES) of sequential resource allocation systems (RAS) is currently a well-established problem in the discrete event system literature, all prior work on it has addressed the underlying LES synthesis problem under the assumption that the system event set is totally controllable. The first part of this work. seeks to relax the controllability assumption, by developing correct and scaleable LES for RAS in which some of the requested resource allocations are uncontrollable. The second part of the presented work addresses the accommodation in the original LES synthesis problem of additional logical constraints, that constitute "forbidden state" specifications and possess a linear characterization with respect to the system resource allocation state. Both problems are addressed in the context of conjunctive/disjunctive-RAS, that constitutes one of the broadest RAS classes investigated in the literature, allowing for arbitrarily structured resource allocations associated with the various process stages, and process routing flexibility.