Synthesis of forcing/locking controllers based on net condition/event systems

We present a method for controller synthesis for forbidden state problems in net condition/event systems. Forbidden states are not only prevented by a purely permissive, locking controller. The controller synthesized enables and disables transitions as well as forces transitions in the plant model. In contrast to other work on that problem, our algorithm does not require the complete enumeration of the whole state space of the plant model. Instead of that we use structural properties which we can extract from the causal structure of our plant model. We illustrate the algorithm by means of a running example