A class of non-deterministic specifications for supervisory control (Q1365652)

The authors show how a certain type of non-deterministic specification for discrete event systems can be used in the framework of 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 behavior of the system. The sharing of the resources is modeled by interleaving the users, which results in a certain kind of nondeterministic specification, with a single initial-state and possibly multiple identically labeled 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.