CPS: Medium: Correct-by-Construction Controller Synthesis using Gaussian Process Transfer Learning

该项目提出了一种新颖而严谨的方法，用于设计具有复杂且可能未知动态的安全关键网络物理系统（CPS）的嵌入式控制软件，该方法采用了控制理论、计算机科学中的形式验证和机器学习中的高斯过程（GPs）的思想。嵌入式控制软件构成了自主交通、交通网络、电力网络、航空航天系统以及健康和辅助生活的主要核心。这些应用程序是CPS的例子，其中软件组件与具有复杂动态的物理系统紧密交互。最近在传感、记忆和通信技术方面的技术进步为CPS无处不在的高细节和大规模数据收集提供了前所未有的机会。在这些尺度上使用数据对CPS的严格分析和设计提出了重大挑战，特别是考虑到数据驱动控制信号引入系统行为的额外固有不确定性。事实上，到目前为止，这种效应还没有得到很好的理解，主要是由于机器学习中的数据分析技术与严格系统设计中动态系统的底层物理之间缺少联系。此外，文献中提出的关于CPS形式化验证或合成的大多数现有结果都是基于模型的，而在许多应用中，模型可能并不总是可用的，或者对于当前的技术来说过于复杂。本项目通过采用GPs的思想，研究了具有复杂且可能未知动力学的CPS的新型结构校正控制器合成方案。特别是，给定CPS的时间逻辑需求（例如，用线性时间逻辑公式或omega-正则语言表示的需求），它们将根据表示这些属性的自动机类型分解为更简单的可达性任务。然后，该项目开发了一种方法，通过使用未知CPS的回归GPs计算所谓的控制屏障函数及其相应的混合控制器来解决这些更简单的任务。此外，研究人员开发了一种适应性迁移学习方法，利用以前学习过的全科医生，并将其作为学习新全科医生的信息来源，特别是在培训数据有限的情况下。该项目开发了一种方案，可以将为旧GPs设计的控制器转移到新GPs，或者在正式保证其对新GPs的正确性的同时安全地对其进行动态修改。将算法实现到设计软件工具中，并在实际的CPS平台（即自主水下航行器和空中机器人）上进行评估。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

This project proposes a novel and rigorous methodology for the design of embedded control software for safety-critical cyber-physical systems (CPS) with complex and possibly unknown dynamics by embracing ideas from control theory, formal verification in computer science, and Gaussian processes (GPs) from machine learning. Embedded control software forms the main core of autonomous transportation, traffic networks, power networks, aerospace systems, and health and assisted living. These applications are examples of CPS, wherein software components interact tightly with physical systems with complex dynamics. Recent technological advances in sensing, memory, and communication technology offer unprecedented opportunities for ubiquitously collecting data at high details and large scales for CPS. Utilization of data at these scales poses major challenges for a rigorous analysis and design of CPS, particularly in view of the additional inherent uncertainty that data-driven control signals introduce to systems behavior. In fact, this effect has not been well understood to this date, primarily due to the missing link between data analytic techniques in machine learning and the underlying physics of dynamical systems in a rigorous system design. In addition, most of the existing results proposed in the literature on the formal verification or synthesis of CPS are model-based, whereas in many applications, a model may not be always available or may be too complex for current techniques. This project investigates a novel correct-by-construction controller synthesis scheme for CPS with complex and possibly unknown dynamics by embracing ideas from the GPs. Particularly, given temporal logic requirements (e.g. those expressed as linear temporal logic formula or by omega-regular languages) for the CPS, they will be decomposed to simpler reachability tasks based on the types of automata representing those properties. Then, the project develops an approach to solve those simpler tasks by computing so-called control barrier functions together with their corresponding hybrid controllers using regressed GPs of the unknown CPS. In addition, the investigators develop an adaptive transfer learning approach that leverages previously learned GPs and emploies them as sources of information in learning new ones especially when limited training data are available. The project develops a scheme on either transferring the controllers designed for old GPs to new ones or safely modifying them on the fly while formally guaranteeing their correctness for the new GPs. The algorithms are implemented into design software tools and evaluated on actual CPS platforms, namely, autonomous underwater vehicles and aerial robots.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.