Non-blocking supervisory control of nondeterministic discrete event systems

In a previous paper (1994), we showed that supervisory control of nondeterministic discrete event systems, in the presence of driven events, can be achieved using prioritized synchronous composition as a mechanism of control, and trajectory models as a modeling formalism. The specifications considered previously were given by prefix-closed languages. In this paper, we extend the theory of trajectory models and prioritized synchronous composition to include markings so that nonclosed specifications and issues such as blocking can be addressed. It is shown that the usual notion of non-blocking, called language model non-blocking, is inadequate in the setting of nondeterministic systems, and a stronger notion, called trajectory model non-blocking, is introduced. Necessary and sufficient conditions for the existence of non-marking and language model non-blocking as well as trajectory model non-blocking supervisors are obtained for nondeterministic systems in the presence of driven events.