Controller Synthesis

We describe here the procedure developed by Giua [5] for safety controllers using ``monitors.'' We present only the case where all transitions are assumed to be controllable. This method is equivalent to the safety controllers described in [27]. The reader is referred to both [5] and [27] for proofs and further details. The controller synthesis procedure is as follows:

• Construct a Petri Net model of the uncontrolled plant, and let its incidence matrix be given by .
• Describe the desired marking constraints by a GMEC . It is assumed that the initial marking satisfies this GMEC.
• The constraint can be enforced by a new place, called monitor, whose input and output edges can be determined from the row vector . The initial marking for this monitor is given by .

A few important facts and remarks should be made at this point:

1. Fact: The addition of a monitor place does not always preserve the liveness of the Petri Net.
2. Fact: Not all markings that satisfy the GMEC may be reached on the net with the addition of a monitor.
3. Fact: Even if liveness is preserved, the Petri Net may lose reversibility.
4. The new monitor place minimally restricts the behavior of the controlled Petri Net, in the sense that it prevents only the firing of transitions that lead to forbidden markings. That is, the control policy taken by the monitor place is maximally permissive.
5. For Petri Nets with uncontrollable transitions, the set of legal markings can be modified so that those markings that satisfy the GMEC, but from which a forbidden marking can be reached by firing only uncontrollable transitions, are not considered legal. It can be shown in this case, however, that there does not always exist a monitor-based solution to a given mutual exclusion problem.
6. It can be shown using the above theorem that, for safe and conservative nets, it is always possible to enforce a GMEC even in the presence of uncontrollable transitions.

For an illustration of Giua's method using monitors, see Section 6.3.