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.

这个CAREER项目通过拥抱控制理论，计算机科学和运筹学的思想，为具有未知封闭形式模型的复杂网络物理系统（CPS）开发正式验证和控制器综合方案。此类系统的新兴示例包括自动汽车、自动交通网络、智能电网和集成医疗设备。该项目的主要新奇在于绕过模型识别阶段，直接使用从其行为中收集的数据来验证或合成CPS控制软件以满足复杂的安全要求。该项目还严格量化了对验证结果或合成控制软件正确性的置信度保证，可以根据数据量进行改进。不幸的是，给定可接受的置信度，所需的数据数量随着系统的大小而快速增长。这被称为样本复杂度。为了解决这个问题，特别是对于大规模CPS，该项目最终提出了一种分而治之的策略，将数据驱动的验证或控制器综合问题分解为半独立的问题，其中解决每个子问题需要更少量的数据。该项目的研究成果将通过以下方式为PI的长期教育计划做出贡献：i）从控制和离散系统理论的基础开始，转向硬件/软件实施，以“端到端观点”开发CPS统一课程; ii）通过本项目开发的平台和基准，为这些课程带来实践学习;以及iii）最后，通过利用科罗拉多大学博尔德分校的外展计划来招募第一代和代表性不足的工程专业学生，并让他们参与本项目中使用的平台，从而提高本科生的保留率。本项目提出了一个可扩展的数据-驱动方法的形式验证和合成的控制软件的CPS与未知模型（a.k.a.黑箱系统）。为此，给定时间逻辑要求（例如，表示为线性时序逻辑公式的那些），它们将基于表示它们的自动机的结构被分解为更简单的任务。然后，通过使用从系统收集的数据构建所谓的障碍函数来解决这些更简单的任务。特别地，对于那些简单的任务，障碍函数的条件首先被公式化为鲁棒凸规划（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

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

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