On the transformation of maximally permissive marking-based liveness enforcing supervisors into monitor supervisors

A marking-based Petri net supervisor restricts a Petri net´s behavior by disabling controllable transitions. Monitors are control places that enforce generalized mutual exclusion constraints. A long standing question concerns the relationship between marking-based supervisors and monitors. There are necessary and sufficient conditions for the existence of maximally permissive marking based supervisors enforcing liveness, but associated monitor solutions may not be maximally permissive. This paper proves that for a bounded Petri net, a maximally permissive liveness enforcing marking based supervisor can always be transformed into a monitor supervisor. Specific conditions are identified that characterize when the resulting monitor supervisor will or will not be maximally permissive. Several examples are used to illustrate these results