Clarification on the Computation of Liveness-Enforcing Supervisor for Resource Allocation Systems With Uncontrollable Behavior

摘要

In previous work, an acceptable transformation of an unacceptable specification on a Petri net can be implemented through a set of mathematical programming formulations. However, such a method becomes invalid when no solution exists in practice. In this paper, we reestablish these formulations and show their correctness.