From Security Enforcement to Supervisory Control in Discrete Event Systems: Qualitative and Quantitative Analyses

Abstract:

Recently, Cyber-Physical Systems have been widely investigated in both theories and applications. Those systems usually involve a huge number of physical components, such as automobiles, aircraft or smart grids, and are monitored by multiple computational units which exchange information through a communication network. The increasing demands for safety, security and performance improvement of these critical systems put stringent constraints on their design and necessitate the use of formal model-based methods to synthesize provably correct tools to enforce some important properties of them. This dissertation aims to tackle two classic problems in Discrete Event Systems (DES), an important class of cyber-physical systems. The first problem is system security in terms of opacity. We apply an interface-based approach called insertion/edit function to enforce opacity under the potential inference of malicious intruders. We study different enforcement scenarios and solve the problems in the frameworks of qualitative and quantitative games on finite graphs. The second problem is performance optimization by supervisory control under partial observation. Another information structure is developed to transform the control problem to a two-player quantitative game on the graph. We analyze the game and propose a novel approach to synthesize supervisors. The content of this dissertation reveals the inner connection between control theory and formal methods.