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.