Research

Supervisory control of discrete event systems under cyber security constraints

• Sponsor: National Natural Science Foundation of China (Young Scientists Fund)

• Role: principle investigator

• Amount: 300,000 CNY

• Start: 2024

Supervisory control theory has been widely used in control of discrete event systems (DES) and is a typical formal methods based design paradigm. The supervisory control architecture is becoming increasingly networked-based and the control systems are deployed in more open environments, which render the supervisory control systems more vulnerable to malicious outside cyber attacks. Therefore, it is critical to achieve the control specifications with high information security assurance. Little research has yet been done, which jointly considers cyber security and logic control goals in supervisory control theory. To address this issue, this project primarily focuses on supervisor synthesis under cyber security constraints. Specifically, information flow based opacity is applied to capture the information security requirements imposed on the control system. In addition, quantitative linear temporal logic formulas are employed to model the logic control specifications. Then a game theoretic supervisory control framework is proposed to model the interactions between the supervisor and the environment, where we specify the goals of both players, construct the game graph and analyze the mechanism of the interaction. By solving the game, we propose a supervisor synthesis method, which is later generalized to the decentralized control case. The ultimate theoretical goal of the project is to develop a systematic modeling, analysis and supervisor synthesis framework of game theoretic supervisory control theory under information security constraints. On the practical perspective, the theoretical results of this project will also provide controller design methods for applications such as autonomous systems task planning in cyber security critical environments

Safe decision-making and planning methods of autonomous driving under formal temporal logic constraints

• Sponsor : National Natural Science Foundation of China (General Program)

• Role: co-principle investigator (with Tongji University, China)

• Amount: 500,000 CNY

• Start: 2024

A safe and trustworthy decision and planning system is the foundation for ensuring the intended functional safety of autonomous vehicles. This project aims to address the industry challenge of undefined functional requirements and difficulty in quantitatively evaluating the safety performance of decision-making systems in unknown and unsafe autonomous driving scenarios. The research focuses on two scientific problems: “encoding and modeling of signal temporal logic” and “driving decision planning under temporal logic constraints.”

The project will establish a probability-based modeling and encoding method of signal temporal logic for traffic rules and driving tasks, determine the safety quantification indicators required for decision planning strategies in risky scenarios, and develop risk quantification acceptable criteria that meet the expected functional safety requirements. It will also propose a receding-horizon optimization algorithm based on the fusion of data and knowledge to satisfy formal temporal logic constraints, and obtain the optimal driving decision and planning strategy that meets the risk quantification criteria of rigorously covered scenarios. Finally, virtual and real-world closed-loop testing of autonomous driving data will be conducted on a complex traffic road environment. Through the implementation of the project, the real-time challenge of formal modeling and safety quantification decision-making for autonomous driving will be addressed, which will help achieve the intended functional safety of autonomous driving and solve the safety long-tail problem for high-level autonomous driving.

Formal analysis and game-theoretic control of cyber physical systems under information security constraints

• Sponsor: Guangdong Province Basic and Applied Basic Research Funding Scheme (General Program)

• Role: principle investigator

• Amount: 150,000 CNY

• Start: 2024

Cyber-physical systems (CPS) are typical hybrid dynamic systems widely applied in various critical engineering and societal fields. As the architecture of these systems becomes increasingly networked and open, they are more susceptible to external attacks during operation, leading to potentially severe consequences. Therefore, achieving control objectives while ensuring information security is of paramount importance. Existing methods lack a comprehensive study of the discrete and continuous dynamic characteristics across systems and are challenging to apply to large-scale nonlinear and stochastic systems. To address these challenges, this project first proposes an information flow approximation of opacity to describe the information security characteristics of the system and introduces quantitatively measurable linear temporal logic to characterize the system's logical control tasks. Subsequently, a finite abstraction method that maintains information security equivalence is proposed to establish a symbolic system model, integrating the security of information space and physical space within a unified formal analysis framework. Furthermore, a formal verification method for information security and a controller design algorithm based on dynamic games are proposed to ensure that the closed-loop system meets information security requirements while fulfilling control tasks. This project aims to develop formal analysis and control theories focused on information security in cyber-physical systems, providing verifiable guarantees for safe system operation and solutions for practical issues related to information security in tasks such as unmanned systems planning.