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），具有复杂且可能是未知的动态，通过接受控制理论，计算机科学中的正式验证以及高斯流程（GPS）（GPS）的复杂动力学（GPS）。嵌入式控制软件构成了自主运输，交通网络，电力网络，航空系统以及健康和辅助生活的主要核心。这些应用是CP的示例，其中软件组件与具有复杂动力学的物理系统紧密相互作用。最新的感测，记忆和通信技术方面的技术进步为无处不在的CPS详细收集数据和大规模收集数据提供了前所未有的机会。在这些量表上的数据利用对CP的严格分析和设计提出了主要挑战，特别是考虑到数据驱动的控制信号引入系统行为的其他固有不确定性。实际上，到目前为止，这种效果尚未得到充分理解，这主要是由于机器学习中的数据分析技术与严格系统设计中动态系统的基础物理学之间的丝毫链接。此外，文献中有关正式验证或合成CPS合成的大多数现有结果都是基于模型的，而在许多应用中，模型可能并不总是可用，或者对于当前技术而言可能太复杂了。该项目通过拥抱GPS的思想，调查了具有复杂且可能未知动态的CP的新型CPS合成方案。特别是，给定时间逻辑要求（例如，为CPS表示为线性时间逻辑公式或欧米茄常规语言），根据代表这些属性的自动机的类型，它们将被分解为更简单的可及性任务。然后，该项目通过使用未知CPS的回归GPS计算所谓的控制屏障功能以及相应的混合控制器来开发一种方法来解决这些简单任务。此外，研究人员开发了一种自适应转移学习方法，该方法利用以前学习的GPS并将其作为学习新信息的来源，尤其是在有限的培训数据时。该项目开发了一个计划，要么将为旧GPS设计的控制器传输到新的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

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