Enforcing k-safeness in controlled state machines

We design a supervisor which enforces k-safeness in state machines, i.e. the marking of every place is not allowed to be greater than k ε N, and which is itself a Petri net. This is done by extending the control design method based on invariants to Petri nets which contain uncontrollable transitions. We show that this supervisor is maximally permissive-disables as few transitions as possible-and is minimal-contains as few control places as possible. Finally, we show that the design of the supervisor can be done using min-plus algebra