A Class of Non-Deterministic Specifications for Supervisory Control

In this paper will be shown how a certain type of non-deterministic specification for discrete event systems can be used with the supervisory control theory. A discrete event system will be regarded as a user-resource system, with a set of resources shared by a set of users. The users are seen as a specification on the behaviour of the system. The sharing of the resources is modelled by interleaving the users, which results in a certain kind of non-deterministic specification, with a single initial-state and possibly multiple identically labelled transitions from one and the same state. It is shown that the supervisory control theory still holds in this context, with a slight modification of the definition of supervisor completeness.