A New Framework for Discrete-Event Systems

Real-world problems are often formulated as diverse properties of different types of dynamical systems. Hence property verification and synthesis (i.e., enforcement) have been long-standing research interests. The motivations of writing this monograph lie in two aspects. First, we will develop an open-loop property enforcement framework for discreteevent systems. Second, we will propose a new model — labeled weighted automata over monoids. The supervisory control framework initialized by Ramadge, Wonham, and Lin in the 1980s provides a closed-loop property enforcement framework for discrete-event systems which usually consist of discrete states and transitions between states caused by spontaneous occurrences of labeled (i.e., partially-observed) events. This framework can be fully realized in labeled finite-state automata (LFSAs). Plenty of theoretical and applied results under this framework have been obtained during the past three decades. However, there are several drawbacks in this framework which restrict the application of the framework to large-scale systems, e.g., all enforceable properties can be enforced in LFSAs in at least exponential time, showing that the enforcement algorithms in this framework do not scale well; this framework cannot be fully realized in more complicated models such as labeled Petri nets and labeled timed automata, because supervisors/controllers in such models are generally not computable (with any complexity upper bound), which narrows the application range of this framework. In this monograph, we will develop an open-loop property enforcement framework for discrete-event systems which scales better and can be implemented in more models. In order to implement this new framework, we develop a tool called concurrent composition, and use this tool to unify plenty of inference-based properties (e.g., detectability, diagnosability, predictability) and concealment-based properties (e.g., various notions of opacity) in discrete-event systems.1 The negations of such properties are equivalently represented by the existence of special runs in the concurrent composition of two variants of a plant. Then, a property of interest can be enforced by choosing controllable events/transitions to disable in order to cut off all such runs violating the property. Our open-loop framework can be implemented in LFSAs in polynomial time for polynomially verifiable properties (e.g., strong detectability, diagnosability, predictability), and can also be fully realized (at least) in labeled Petri nets and labeled timed automata for decidable inference-based and concealment-based properties. In the second aspect, we propose a new model called labeled weighed automata over monoids (LWAMs). LWAMs provide a natural generalization of LFSAs in the sense that each transition therein carries a weight from a monoid, the weight of a run (a sequence of consecutive transitions) is the product of the weights of the run's transitions. When weights are nonnegative real numbers, they could be interpreted as the time consumptions of the transitions’ executions, so that LWAMs could be regarded as real-time systems. When weights are real vectors (hence the entries of the vectors could be negative), they can be interpreted as position deviations of a moving object along with the transitions’ executions. We develop original techniques to compute three basic tools — concurrent composition, observer, and detector in LWAMs, and then design algorithms for verifying various notions of detectability. The research in LWAMs has just started. With these three tools, plenty of results in LFSAs obtained in the past three decades can be extended to LWAMs, including results on inference-based properties and concealment-based properties, as well as results obtained in the supervisory control framework. Our open-loop property enforcement framework, of course, can be fully implemented in LWAMs. Compared with LFSAs, LWAMs provide more accurate modeling scheme, hence have more applications. A challenging future direction lies in extending the formal verification and synthesis framework of cyber-physical systems from the core part of LFSAs-based to LWAMs-based.