Liveness enforcing supervision for resource allocation systems with process synchronizations

This paper considers the problem of establishing live resource allocation in workflows with synchronization stages, i.e., stages where sub-processes re-combine through merging and/or splitting and then continue as a new set. Establishing live yet efficient resource allocation in this class of systems is extremely difficult since even the problem of process "quasi-liveness"-i.e., assessing whether a given level of resource capacities is sufficient to complete any single process-is NP-complete. Using the Petri net formalism of Generalized Augmented Marked Graphs to rigorously define the considered class of resource allocation systems (RAS), the presented work develops a methodology that, given any instance from the considered RAS class, (i) it assesses the quasi-liveness of the involved processes, and (ii) in case that the system processes are found to be quasi-live, it synthesizes a (computationally) efficient liveness enforcing supervisor for it, by pertinently reducing the original supervisory control problem to its counterpart for disjunctive/conjunctive resource allocation systems; the latter has already been investigated in the literature, and a number of controller design methods and results are available for it.