Model-based monitoring of discrete-event systems

A Discrete Event System (DES) is a dynamic system in which the state of the system changes instantaneously in response to the occurrence of events. DESs arise as models of many modern man-made systems, including manufacturing systems, communication networks, computer systems, digital sequential circuits, and traffic systems. An important problem in the modeling, analysis and control of DESs is the problem of on-line monitoring, which plays a key role in performance evaluation, fault tolerance, verification, debugging, security, and control of DESs. A monitoring system performs the tasks of gathering, interpreting, and reacting to the information on the behavior of a system. Among these tasks, data interpretation is the central task of the monitoring system when there is limited observation. In this thesis, we consider the problem of model-based monitoring of DESs, and concentrate on the task of data interpretation where only limited observation is available. Specifically, we consider the problem of extracting information on events in a timed DES from partial observations, a process we refer to as inversion. We adopt two popular models for DESs: automata (finite-state machines) and Petri nets. We develop necessary and sufficient conditions for invertibility. These conditions provide a basis for efficiently determining whether a given DES with an observation scheme is invertible. For invertible systems, we provide an algorithm to perform inversion. We also consider d-invertibility, which is less restrictive than invertibility in that it allows delay of d occurrences of events in inversion. To circumvent the complexity problem that arises in dealing with very complex DESs, we develop an approach for inversion based on a distributed model. We investigate the problem of designing an observation scheme to make a given system invertible, which is as important a problem as that of checking invertibility. Finally, we consider the problem of fault detection and identification in untimed DESs. We approach the problem using the techniques developed for invertibility