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

CPS：中：使用高斯过程迁移学习的构造校正控制器综合

• 批准号: 2039062
• 负责人: Majid Zamani
• 金额: $ 120万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-01-01 至 2024-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2039062&HistoricalAwards=false
• 关键词: CPS; Medium; Correct; Construction; Controller

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.

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

项目成果

Synergistic Offline-Online Control Synthesis via Local Gaussian Process Regression

• DOI: 10.1109/cdc45484.2021.9683557
• 发表时间: 2021-10
• 期刊: 2021 60th IEEE Conference on Decision and Control (CDC)
• 作者: John Jackson;L. Laurenti;E. Frew;Morteza Lahijanian

Formal Synthesis of Safety Controllers for Unknown Systems Using Gaussian Process Transfer Learning

• DOI: 10.1109/lcsys.2023.3341548
• 发表时间: 2023
• 期刊: IEEE Control Systems Letters
• 影响因子: 3
• 作者: A. Awan;Majid Zamani

Transfer Learning for Barrier Certificates

• DOI: 10.1109/cdc49753.2023.10384302
• 发表时间: 2023-12
• 期刊: 2023 62nd IEEE Conference on Decision and Control (CDC)
• 作者: Alireza Nadali;Ashutosh Trivedi;Majid Zamani

Formal Abstraction of General Stochastic Systems via Noise Partitioning

通过噪声划分对一般随机系统进行形式化抽象

• DOI: 10.1109/lcsys.2023.3340621
• 发表时间: 2023
• 期刊: IEEE Control Systems Letters
• 影响因子: 3
• 作者: Skovbekk, John;Laurenti, Luca;Frew, Eric;Lahijanian, Morteza
• 通讯作者: Lahijanian, Morteza

Towards Safe AI: Sandboxing DNNs-Based Controllers in Stochastic Games

• DOI: 10.1609/aaai.v37i12.26789
• 发表时间: 2023-06
• 作者: Bingzhuo Zhong;H. Cao;Majid Zamani;M. Caccamo