FET: Medium: Collaborative Research: An Efficient Framework for the Stochastic Verification of Computation and Communication Systems Using Emerging Technologies

FET：媒介：协作研究：使用新兴技术对计算和通信系统进行随机验证的有效框架

• 批准号: 1900542
• 负责人: Hao Zheng
• 金额: $ 25.7万
• 依托单位: University of South Florida
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-07-15 至 2024-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1900542&HistoricalAwards=false
• 关键词: FET; Medium; Collaborative; Research; Efficient

Synthetic biology and nanotechnology place increasing demands on design methodologies to ensure dependable and robust operation. Consisting of noisy and unreliable components, these complex systems have large and often infinite state spaces that include extremely rare error states. Stochastic model checking techniques have demonstrated significant potential in quantitatively analyzing such system models under extremely low probability. Unfortunately, they generally require enumerating the model's state space, which is computationally intractable or impossible. Therefore, addressing these design challenges in emerging technologies requires enhancing the applicability of stochastic model checking. Motivated by this problem, this project investigates an automated stochastic verification framework that integrates approximate stochastic model checking and counterexample-guided rare-event simulation to improve the analysis accuracy and efficiency. This project focuses on verifying infinite-state continuous-time Markov chain models with rare-event properties. It addresses the scalability problem by first applying property-guided and on-the-fly state truncation techniques to prune unlikely states to obtain finite state representations that are amenable to stochastic model checking. In the case of false or indeterminate verification results, stochastic counterexamples are generated and utilized to improve the accuracy of the state reductions. Furthermore, it mines these critical counterexamples as automated guidance to improve the quality and efficiency for rare-event stochastic simulations. This verification framework will be integrated within existing state-of-the-art stochastic model checking tools, and benchmarked on a wide range of real-world case studies in synthetic biology and nanotechnology.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.

合成生物学和纳米技术对设计方法提出了越来越高的要求，以确保可靠和稳健的操作。这些复杂系统由嘈杂和不可靠的组件组成，具有巨大且通常无限的状态空间，其中包括极其罕见的错误状态。随机模型检验技术在极低概率下定量分析这类系统模型方面显示出巨大的潜力。不幸的是，它们通常需要枚举模型的状态空间，这在计算上是难以处理的或不可能的。因此，在新兴技术中解决这些设计挑战需要增强随机模型检查的适用性。基于这一问题，本项目研究了一种集成近似随机模型检查和反例引导的罕见事件模拟的自动化随机验证框架，以提高分析精度和效率。本课题的重点是验证具有稀有事件性质的无限状态连续马尔可夫链模型。它解决了可伸缩性问题，首先应用属性引导和动态状态截断技术来修剪不可能的状态，以获得适合随机模型检查的有限状态表示。在验证结果错误或不确定的情况下，生成随机反例并利用其提高状态约简的准确性。此外，它挖掘这些关键的反例作为自动指导，以提高罕见事件随机模拟的质量和效率。该验证框架将集成到现有的最先进的随机模型检查工具中，并在合成生物学和纳米技术的广泛现实案例研究中进行基准测试。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

STAMINA: STochastic Approximate Model-checker for INfinite-state Analysis

• DOI: 10.1007/978-3-030-25540-4_31
• 发表时间: 2019-06
• 期刊: ArXiv
• 作者: Thakur Neupane;C. Myers;C. Madsen;Hao Zheng;Zhen Zhang

A Comparison of Weighted Stochastic Simulation Methods for the Analysis of Genetic Circuits

遗传电路分析的加权随机模拟方法比较

• DOI: 10.1021/acssynbio.2c00553
• 发表时间: 2023
• 期刊: ACS Synthetic Biology
• 影响因子: 4.7
• 作者: Ahmadi, Mohammad;Thomas, Payton J.;Buecherl, Lukas;Winstead, Chris;Myers, Chris J.;Zheng, Hao
• 通讯作者: Zheng, Hao