CAREER: A Data-Driven Approach for Verification and Control of Cyber-Physical Systems

职业：用于验证和控制网络物理系统的数据驱动方法

• 批准号: 2145184
• 负责人: Majid Zamani
• 金额: $ 53.23万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-06-15 至 2027-05-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2145184&HistoricalAwards=false
• 关键词: CAREER; Data; Driven; Approach; Verification

This CAREER project develops formal verification and controller synthesis schemes for complex cyber-physical systems (CPS) with unknown closed-form models by embracing ideas from control theory, computer science, and operations research. Emerging examples of such systems include autonomous cars, autonomous transportation networks, smart grids, and integrated medical devices. The main novelty of this project lies in bypassing the model identification phase and directly verifying or synthesizing control software for CPS against complex safety requirements using just data collected from their behaviors. This project also quantifies rigorously a confidence guarantee on the verification outcomes or the correctness of synthesized control software, which can be improved based on the amount of data. Given an acceptable confidence, unfortunately, the required number of data grows rapidly with the size of the system. This is known as the sample complexity. To tackle this issue, particularly, for large-scale CPS, the project finally proposes a divide and conquer strategy by breaking the data-driven verification or controller synthesis problems into semi-independent ones, where solving each subproblem requires a much smaller amount of data. The research outcomes of this project will contribute to the long term education plan of the PI by i) developing unified courses on CPS with an “end-to-end view,” starting from the foundations of control and discrete systems theory and moving to hardware/software implementations; ii) bringing hands-on learning to those courses by the platforms and benchmarks developed in this project; and iii) finally, improving undergraduate retention rates by leveraging the outreach programs at the University of Colorado Boulder to recruit first generation and underrepresented engineering students and engage them in the platforms used in this project.This project proposes a scalable data-driven approach for formal verification and synthesis of control software for CPS with unknown models (a.k.a. black-box systems). To do so, given temporal logic requirements (e.g., those expressed as linear temporal logic formulae) for CPS, they will be decomposed into simpler tasks based on the structures of automata representing them. Then, those simpler tasks are tackled by constructing so-called barrier functions using data collected from the systems. Particularly, the conditions over barrier functions for those simpler tasks are first formulated as robust convex programs (RCP) which are technically semi-infinite linear programs. Solving those RCP directly are not tractable due to unknown models. Instead, this project considers a set of data collected from the system and solves scenario convex programs (SCP), which are finite linear programs. Barrier functions resulted by solving SCP are combined to verify the given requirement or to provide a controller enforcing it. The project also quantifies rigorously a confidence (a.k.a. out-of-sample performance guarantee) on the verification outcomes or the correctness of synthesized controllers. To tackle the underlying sample complexity for large-scale CPS, this project proposes an adaptive sampling and a modular data-driven schemes by exploiting the natural structure present in the system. Finally, the proposed algorithms will be implemented into open-source software tools to automate the proposed data-driven techniques and evaluated on Artificial Pancreas systems and a team of scale-model autonomous vehicles.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）开发形式验证和控制器综合方案，此类系统的新兴示例包括自动驾驶汽车、自动运输。该项目的主要新颖之处在于绕过模型识别阶段，仅使用从其行为收集的数据来直接验证或合成 CPS 的控制软件。信心验证结果或综合控制软件的正确性的保证，可以根据数据量进行改进，不幸的是，所需的数据数量随着系统的规模而迅速增长。为了解决这个问题，特别是对于大规模CPS，该项目最终提出了一种分而治之的策略，将数据驱动的验证或控制器综合问题分解为半独立的问题，其中解决每个子问题都需要大量的时间。本项目的研究成果较少。将为 PI 的长期教育计划作出贡献：i) 以“端到端视角”开发 CPS 统一课程，从控制和离散系统理论基础开始，转向硬件/软件实现；通过该项目开发的平台和基准将实践学习带入这些课程；iii) 最后，通过利用科罗拉多大学博尔德分校的外展计划来招募第一代和代表性不足的工程专业学生并让他们参与其中，从而提高本科生的保留率；使用的平台该项目提出了一种可扩展的数据驱动方法，用于对未知模型（又称黑盒系统）的 CPS 控制软件进行形式化验证和合成，在给定时间逻辑要求（例如，表示为线性时间逻辑的要求）的情况下实现这一点。对于 CPS，它们将根据代表它们的自动机的结构分解为更简单的任务，然后，通过使用从系统收集的数据构造所谓的障碍函数来解决这些更简单的任务。这些更简单任务的障碍函数首先被表述为鲁棒凸程序（RCP），从技术上讲，这些程序是半无限线性程序，由于未知模型，直接求解这些 RCP 是不易处理的。系统并求解场景凸程序（SCP），这是通过求解 SCP 产生的有限线性程序，组合起来验证给定的要求或提供执行它的控制器。该项目还严格量化置信度。 （又名样本外性能保证）验证结果或合成控制器的正确性为了解决大规模 CPS 的潜在样本复杂性，该项目通过利用自然特性提出了自适应采样和模块化数据驱动方案。最后，所提出的算法将被实施到开源软件工具中，以自动化所提出的数据驱动技术，并在人工胰腺系统和比例模型自动车辆团队上进行评估。该奖项由 NSF 授予。法定使命，并通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

A Scenario Approach for Synthesizing k -Inductive Barrier Certificates

合成 k 感应势垒证书的场景方法

• DOI: 10.1109/lcsys.2022.3184661
• 发表时间: 2022
• 期刊: IEEE Control Systems Letters
• 影响因子: 3
• 作者: Murali, Vishnu;Trivedi, Ashutosh;Zamani, Majid
• 通讯作者: Zamani, Majid

Estimation of Infinitesimal Generators for Unknown Stochastic Hybrid Systems via Sampling: A Formal Approach

通过采样估计未知随机混合系统的无穷小生成器：一种形式方法

• DOI: 10.1109/lcsys.2022.3186167
• 发表时间: 2023
• 期刊: IEEE Control Systems Letters
• 影响因子: 3
• 作者: Nejati, Ameneh;Lavaei, Abolfazl;Soudjani, Sadegh;Zamani, Majid
• 通讯作者: Zamani, Majid

Constructing MDP Abstractions Using Data With Formal Guarantees

使用具有正式保证的数据构建 MDP 抽象

• DOI: 10.1109/lcsys.2022.3188535
• 发表时间: 2023
• 期刊: IEEE Control Systems Letters
• 影响因子: 3
• 作者: Lavaei, Abolfazl;Soudjani, Sadegh;Frazzoli, Emilio;Zamani, Majid
• 通讯作者: Zamani, Majid

Data-Driven Stability Verification of Homogeneous Nonlinear Systems with Unknown Dynamics

未知动力学齐次非线性系统的数据驱动稳定性验证

• DOI: 10.1109/cdc51059.2022.9992739
• 发表时间: 2022
• 期刊: The 61st Conference on Decision and Control (CDC
• 作者: Lavaei, Abolfazl;Esfahani, Peyman Mohajerin;Zamani, Majid
• 通讯作者: Zamani, Majid

Safety Verification of Stochastic Systems: A Repetitive Scenario Approach

随机系统的安全验证：重复场景方法

• DOI: 10.1109/lcsys.2022.3186932
• 发表时间: 2023
• 期刊: IEEE Control Systems Letters
• 影响因子: 3
• 作者: Salamati, Ali;Zamani, Majid
• 通讯作者: Zamani, Majid