Formal Methods for Control of Cyber-Physical Systems: Theory, Algorithms, and Implementations

点击翻译按钮获取中文摘要

Cyber-physical systems (CPS) are physical engineering systems controlled by computer-based algorithms. Such systems are increasingly penetrating our lives: unmanned air vehicles (UAVs) executing search and rescue missions, autonomous cars navigating through busy traffic, and surgical robots performing life-saving operations---these are just a few examples of how integrations of advanced control algorithms with physical systems can lead to important applications. Many CPS, including the above motivating applications, are safety-critical: their failure can lead to catastrophic consequences. For example, the Ariane 5 rocket, which took the European Space Agency 10 years and $7 billions to produce, crashed in less than one minute due to a small error in the numerical software design. The recent failures of Tesla's AutoPilot that caused fatal accidents is another warning sign that we still significantly lack confidence in trusting automated machines. The increasingly pervasive use of machine learning algorithms also raises the fundamentally important question of AI trust in control of safety-critical CPS. Indeed, how to affordably build and efficiently certify CPS as safe, reliable, and trustworthy remains a fundamental challenge in both academia and industry. There are several factors that make control design for CPS an enormous challenge: 1) CPS usually have hybrid dynamics involving both continuous and discrete dynamics. Hybrid systems are generally more challenging to analyze and control; 2) CPS typically have complex requirements, which are beyond what can be handled by the current theory and tools of control engineering; 3) Current practices of formal methods for control of CPS often suffer from curse of dimensionality and require very accurate system models.  Motivated by these challenges, the proposed research program will develop the theoretical foundations and computational frameworks for computer-aided control design for CPS. By doing so, the proposed program will advance the-state-of-the-art of mathematical control theory and design methods for safety-critical CPS. The long-term goal is to systematically develop validated computational methods for robust design of CPS and translate them to practice. The short-term objectives (within in the next five years) are to: (O1) Explore the theoretical limits of validated computation and formal methods for control of CPS; (O2) Design efficient algorithms and tools for robust control synthesis for CPS from rigorous specifications; (O3) Exploit the synergies of control theory, learning, and optimization to overcome the curse of dimensionality and curse of modelling in control of CPS. The outcomes of the proposed research can significantly benefit several CPS sectors in Canada, including automotive, aerospace, and robotics. Students trained under this program will gain competitive skills, such as control, machine learning, and robotics, to enter the booming fields of robotics, AI, and automation.