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.

该项目提出了一种新颖而严格的方法，用于安全关键网络物理系统（CPS）的嵌入式控制软件的设计，该系统具有复杂且可能未知的动态，包括控制理论，计算机科学中的形式验证和机器学习中的高斯过程（GP）。嵌入式控制软件构成了自主交通、交通网络、电力网络、航空航天系统以及健康和辅助生活的主要核心。这些应用程序是CPS的示例，其中软件组件与具有复杂动态的物理系统紧密交互。传感器、存储器和通信技术的最新技术进步为CPS提供了前所未有的机会，可以无处不在地收集高细节和大规模的数据。在这些尺度上利用数据对CPS的严格分析和设计提出了重大挑战，特别是考虑到数据驱动的控制信号引入系统行为的附加固有不确定性。事实上，到目前为止，这种效应还没有得到很好的理解，主要是由于机器学习中的数据分析技术与严格系统设计中动力系统的底层物理之间缺少联系。此外，在文献中提出的CPS的正式验证或合成的现有结果中的大多数是基于模型的，而在许多应用中，模型可能并不总是可用的，或者对于当前的技术可能太复杂。本计画探讨一种新颖的构造校正控制器综合方案，以因应复杂且可能未知的动态特性，借由包含来自全球定位系统的想法。特别地，给定CPS的时序逻辑要求（例如，表示为线性时序逻辑公式或由ω正则语言表示的时序逻辑要求），它们将基于表示这些属性的自动机的类型被分解为更简单的可达性任务。然后，该项目开发了一种方法来解决这些简单的任务，通过计算所谓的控制障碍函数及其相应的混合控制器使用回归的GP未知CPS。此外，研究人员开发了一种自适应迁移学习方法，该方法利用以前学习的GP，并将其用作学习新GP的信息来源，特别是在训练数据有限的情况下。该项目开发了一个方案，将为旧GPS设计的控制器转移到新的控制器，或者在飞行中安全地修改它们，同时正式保证它们对新GPS的正确性。这些算法被应用到设计软件工具中，并在实际的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

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 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

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

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