Interacting discrete event systems: Modelling, verification, and supervisory control

Within the formal language and automata settings, a modelling and analysis paradigm for multiprocess discrete event systems is proposed. The modelling structure, referred to as one of interacting discrete event systems (IDES), features explicit representation of the system components. In addition, different forms of interactions between the components can be directly represented---as interaction specification---in the modelling structure. A multilevel extension to the model is introduced. The composition and decomposition operations for multiprocess systems are extended for the IDES model to incorporate the interaction specification.; Several approaches are presented for verifying interacting discrete event systems. The proposed approaches do not require the computation of the synchronous product of the system components, and therefore avoid a major bottleneck in this class of problems. In one approach, the system is verified for internal correctness (non-blocking) by first detecting potential synchronization conflicts and then checking the reachability of the underlying states. External verification with respect to a given specification is also investigated. In certain situations, the interaction information can be used to solve the external verification problem modularly by converting the problem into an equivalent set of verification tests addressing the system components individually. In case the interaction specification does not provide enough information to verify the system modularly, an iterative procedure is presented to refine the interaction specification gradually until a solution is found.; The supervisory control problem is then investigated within the IDES setting. Two efficient procedures are presented for optimal non-blocking supervisory synthesis for multiprocess systems. In these procedures, the composition of the system components is avoided by exploring only the common traces between the system and the specification. The general case of IDES supervision is then investigated. It is shown that under certain conditions depending on the structure of the system and the given specification, optimal supervision can be achieved and implemented modularly, that is, using local supervisors for the components and a high-level supervisor for the interaction specification.