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

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

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.