This work describes the research conducted in the quest for designing better software for discrete-event system (DES) control. The think-aloud data from an exploratory observational study of solving DES control problems contributed to the formulation of a list of recommendations on how to design and improve DES software. These observations, together with other relevant research, led to the proposal of a novel approach to DES problem solving, namely, the template design methodology. This methodology does not require the introduction of new control theory; it is rather an reinterpretation of the existing modelling framework. Software supporting this methodology was implemented and subsequently evaluated using twelve subjects. Significant improvements in the speed of problem solving as well as positive evaluations by the subjects were observed. The usability data do not show any drawbacks to applying the methodology. / Thesis (Ph.D, Computing) -- Queen's University, 2009-08-21 17:11:14.991

The application of Discrete-Event Systems (DES) theory to the problem of guar- anteeably enforcing concurrency constraints in multi-threaded applications has been studied under certain assumptions, namely, the assumption of a static pool of pre- existing instantiated threads, whose creation and termination are not modelled. This work proposes an extension of this case to handle dynamically instantiated and termi- nated threads using a Petri net formalism and an online limited-lookahead state-space search technique. / Thesis (Master, Computing) -- Queen's University, 2010-05-27 17:00:15.99

In this thesis, we investigate the problem of fault tolerance in the framework of discrete-event systems (DES). We introduce our setting, and then provide a set of fault-tolerant definitions designed to capture different types of fault scenarios and to ensure that our system remains controllable and nonblocking in each scenario. This is a passive approach that relies upon inherent redundancy in the system being controlled, and focuses on the intermittent occurrence of faults. Our approach provides an easy method for users to add fault events to a system model and is based on user designed supervisors and verification. As synthesis algorithms have higher complexity than verification algorithms, our approach should be applicable to larger systems than existing active fault-recovery methods that are synthesis based. Also, modular supervisors are typically easier to understand and implement than the results of synthesis. Finally, our approach does not require expensive (in terms of algorithm complexity) fault diagnosers to work. Diagnosers are, however, required by existing methods to know when to switch to a recovery supervisor. As a result, the response time of diagnosers is not an issue for us. Our supervisors are designed to handle the original and the faulted system. In this thesis, we next present algorithms to verify these properties followed by complexity analyses and correctness proofs of the algorithms. Finally, examples are provided to illustrate our approach. In the above framework, permanent faults can be modelled, but the current method was onerous. To address this, we then introduce a new modeling approach for permanent faults that is easy to use, as well as a set of new permanent fault-tolerant definitions. These definitions are designed to capture several types of permanent fault scenarios and to ensure that our system remains controllable and nonblocking in each scenario. New definitions and scenarios were required as the previous ones were incompatible with the new permanent fault modeling approach. We then present algorithms to verify these properties followed by complexity analyses and correctness proofs of the algorithms. An example is then provided to illustrate our approach. Finally, we extend the above intermittent and permanent fault-tolerant approach to the timed DES setting. As before, we introduced new fault-tolerant properties and algorithms. We then provide complexity analyses and correctness proofs for the algorithms. An example is then provided to illustrate our approach. / Thesis / Doctor of Philosophy (PhD)

The development of controls for the execution of concurrent code is non-trivial. This work shows how existing discrete-event system (DES) theory can be successfully applied to this problem. From code without concurrency controls and a specification of desired behaviours, a DES representation of the problem is obtained, and then used to generate concurrency control code. By applying rigorously proven DES theory, the resulting code comes with guarantees not present in similar works. All control schemes generated in DES are nonblocking, yielding code that is free of both livelock and deadlock. Additionally, the generated control scheme is minimally restrictive, meaning only problematic behaviours are prevented. If the specifications cannot be enforced as presented, the largest controllable subset is instead enforced. The result, which requires no further interaction to generate, is the best possible control scheme given the interaction between the specifications and the original code. Existing methods encounter difficulties when faced with multiple specifications that interact to form deadlocks. Modular DES theory is successfully applied, allowing resolution of these conflicts without requiring the user to introduce new specifications. Moreover, the approach is independent of specific programming or specification languages. A Java implementation is given, along with two problems showing the process in action. / Thesis (Master, Computing) -- Queen's University, 2008-09-25 09:03:51.593

Discrete-Event systems (DES) is a framework in which problems are modelled as finite-state automata and a solution in the form of a supervisory control scheme can be automatically synthesized via an exhaustive search through the state space of the system. Various extensions to the standard DES framework have been introduced to allow it to be applied to a greater variety of problems. When the system in question is very large or varies with time, a limited lookahead policy can be adopted, in which control decisions are made on-the-fly by looking at finite-step projections of the behaviour of the system's underlying automata. This work presents a new approach to limited lookahead supervision which incorporates many of the extensions to DES that are already present in the literature, such as event probability and string desirability. When dealing with a limited lookahead technique, the projected system behaviour is represented as a lookahead tree with some depth limit decided on by the user. It can be difficult to strike a balance between the complexities associated with storing and analyzing the trees and the amount of information available to make decisions, both of which increase with depth. This work also presents a set of methods which are designed to aid in accurately estimating the state space of lookahead trees with the intent of simplifying the process of determining a favourable depth to use. Finally, the approaches introduced herein are applied to a simulation of an infectious disease outbreak, primarily to showcase them in action, but also for the possibility of illuminating any useful information for real-world health units. / Thesis (Master, Computing) -- Queen's University, 2012-01-20 19:35:58.007

The state-based approach plays an important role in modeling and control of Discrete-Event Systems (DES). Based on previous work, state feedback control of DES with nonblocking is thoroughly investigated; a general construction method for memory and the corresponding predicate is also specified. Two examples are provided in illustration. Also presented is state-based control of DES with observational abstraction. Based on the existing idea of quasi-congruence, quasi-observer, as a kind of observational abstraction, is developed; its advantages and limitations are discussed by means of simple examples. Imposing an observational partition on the state set also leads to observational abstraction. On this basis, the state-feedback controller design is introduced; in particular, the notion of high and low modeling levels for DES is proposed, based on which reachability and controllability are further discussed and compared. Finally, two simple applications are provided to show the advantage of observational partition in DES analysis and control.

The state-based approach plays an important role in modeling and control of Discrete-Event Systems (DES). Based on previous work, state feedback control of DES with nonblocking is thoroughly investigated; a general construction method for memory and the corresponding predicate is also specified. Two examples are provided in illustration. Also presented is state-based control of DES with observational abstraction. Based on the existing idea of quasi-congruence, quasi-observer, as a kind of observational abstraction, is developed; its advantages and limitations are discussed by means of simple examples. Imposing an observational partition on the state set also leads to observational abstraction. On this basis, the state-feedback controller design is introduced; in particular, the notion of high and low modeling levels for DES is proposed, based on which reachability and controllability are further discussed and compared. Finally, two simple applications are provided to show the advantage of observational partition in DES analysis and control.

Discrete event systems (DESs) are systems which involve quantities that take a discrete set of values, called states, and which evolve according to the occurrence of certain discrete qualitative changes, called events. Examples of DESs include many man-made systems such as computer and communication networks, robotics and manufacturing systems, computer programs, and automated trac systems. Supervisory control and failure diagnosis are two important problems in the study of DESs. This dissertation presents a temporal logic approach to the control and failure diagnosis of DESs. For the control of DESs, full branching time temporal logic-CTL* is used to express control specifications. Control problem of DES in the temporal logic setting is formulated; and the controllability of DES is defined. By encoding the system with a CTL formula, the control problem of CTL* is reduced to the decision problem of CTL*. It is further shown that the control problem of CTL* (resp., CTL{computation tree logic) is complete for deterministic double (resp., single) exponential time. A sound and complete supervisor synthesis algorithm for the control of CTL* is provided. Special cases of the control of computation tree logic (CTL) and linear-time temporal logic (LTL) are also studied; and for which algorithms of better complexity are provided. For the failure diagnosis of DESs, LTL is used to express fault specifications. Failure diagnosis problem of DES in the temporal logic setting is formulated; and the diagnosability of DES is defined. The problem of testing the diagnosability is reduced to that of model checking. An algorithm for the test of diagnosability and the synthesis of a diagnoser is obtained. The algorithm has a polynomial complexity in the number of system states and the number of fault specifications. For the diagnosis of repeated failures in DESs, different notions of repeated failure diagnosability, K-diagnosability, [1,K]-diagnosability, and [1,1]-diagnosability, are introduced. Polynomial algorithms for checking these various notions of repeated failure diagnosability are given, and a procedure of polynomial complexity for the on-line diagnosis of repeated failures is also presented.

In the area of Discrete Event Systems (DES), formal verification techniques are important in examining a variety of system properties including controllability and nonblocking. Nonetheless, in reality, most software and hardware practitioners are not proficient in formal methods which holds them back from the formal representation and verification of their systems. Alternatively, it is a common observation that control engineers are typically familiar with Moore synchronous Finite State Machines (FSM) and use them to express their controllers’ behaviour. Taking this into consideration, we devise a generic and structured approach to automatically translate Moore synchronous FSM into timed DES (TDES) supervisors. In this thesis, we describe our FSM-TDES translation method, present a set of algorithms to realize the translation steps and rules, and demonstrate the application and correctness of our translation approach with the help of an example. In order to develop our automatic FSM-TDES translation approach, we exploit the structural similarity created by the sampled-data (SD) supervisory control theory between the two models. To build upon the SD framework, first we address a related issue of disabling the tick event in order to force an eligible prohibitable event in the SD framework. To do this, we introduce a new synchronization operator called the SD synchronous product (||SD), adapt the existing TDES and SD properties, and devise our ||SD setting. We formally verify the controllability and nonblocking properties of our ||SD setting by establishing logical equivalence between the existing SD setting and our ||SD setting. We present algorithms to implement our ||SD setting in the DES research tool, DESpot. The formulation of the ||SD operator provides twofold benefits. First, it simplifies the design logic of the TDES supervisors that are modelled in the SD framework. This results in improving the ease of manually designing SD controllable TDES supervisors, and reduced verification time of the closed-loop system. We demonstrate these benefits by applying our ||SD setting to an example system. Second, it bridges the gap between theoretical supervisors and physical controllers with respect to event forcing. This makes our FSM-TDES translation approach relatively uncomplicated. Our automatic FSM-TDES translation approach enables the designers to obtain a formal representation of their controllers without designing TDES supervisors by hand and without requiring formal methods expertise. Overall, this work should increase the adoption of the SD supervisory control theory in particular, and formal methods in general, in the industry by facilitating software and hardware practitioners in the formal representation and verification of their control systems. / Dissertation / Doctor of Philosophy (PhD)

In this dissertation, we explore the problem of fault detection and fault diagnosis for systems modeled as condition systems. A condition system is a Petri net based framework of components which interact with each other and the external environment through the use of condition signals. First, a system FAULT is defined as an observed behavior which does not correspond to any expected behavior, where the expected behavior is defined through condition system models. A DETECTION is the determination that the system is not behaving as expected according to the model of the system. A DIAGNOSIS of this fault localizes the subsystem that is the source of the discrepancy between output and expected observations. We characterize faults as a behavior relaxation of model components. We then show that detection and diagnosis can be determined in a finite number of calculations. The exact solution can be computationally involved, so we also present methods to perform a rapid detection and diagnosis. We have also included a chapter on a conversion from the condition system framework into a linear-time temporal logic(LTL) framework.