Maximally permissive supervisor synthesis based on a new constraint transformation method

The method is proposed to design the maximally permissive and efficient supervisor for enforcing linear constraints, in which the weights of places are not negative, on ordinary Petri nets with uncontrollable transitions. First, the weakly admissible linear constraint is introduced. Second, a method is proposed to design the monitor place for enforcing a weakly admissible linear constraint on Petri nets. Third, a theorem proving that a linear constraint can be equivalently transformed at an uncontrollable transition into a disjunction of new constraints is proposed. Fourth, using this theorem, an algorithm is presented to equivalently transform a linear constraint, each place weight of which is not negative, into a disjunction of weakly admissible ones. Lastly, the supervisor, which consists of the plant net and a set of monitor places, is designed for the weakly admissible linear constraints calculated by the above algorithm.