RAGTIMER 1.0：随机VAS的快速稀有事件部分状态空间构建（扩展版）
RAGTIMER 1.0: Rapid Rare-Event Partial State Space Construction for Stochastic VAS (extended version)
- Utah State University（犹他州立大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出RAGTIMER 1.0工具，通过枚举并扩展稀有事件轨迹，为连续时间随机向量加法系统构建部分状态空间，提供稀有事件概率的保证下界，优于现有概率模型检验工具并反驳了随机模拟的估计。
AI中文摘要：
对连续时间随机向量加法系统（CTSVAS）（如化学反应网络（CRNs））中稀有事件的瞬态可达性分析，已被证明对尖端工具而言是一项艰巨的挑战。CTSVAS的底层是一个连续时间马尔可夫链（CTMC），而CTMC瞬态可达性分析需要概率模型检验（PMC）。该分析要求显式表示模型的整个状态空间。稀有事件以极低的概率发生，加剧了概率分析的难度。在CRNs中，验证稀有事件的概率至关重要；即使物种浓度很低，也可能导致病理后果。本文介绍了RAGTIMER 1.0工具，它通过枚举到感兴趣稀有事件的轨迹并扩展这些轨迹以利用并发性和循环，高效地为CTSVAS构建部分状态空间，从而提供稀有事件概率的保证下界。保证下界在合成生物学应用中特别有用，因为它们指示了稀有事件如何以及何时可以被实验观察到。RAGTIMER是现有CTSVAS模型稀有事件分析方法的一个有吸引力的替代方案。它优于现有的PMC工具，并在多个具有挑战性的CRN模型上反驳了稀有事件随机模拟的多个概率估计。RAGTIMER使用优化的数据结构、简单的输入格式和内存安全的Rust代码，以提高PMC对行业专业人士的可扩展性和可访问性。
英文摘要：
Transient reachability analysis of rare events in Continuous-Time Stochastic Vector Addition Systems (CTSVAS) such as Chemical Reaction Networks (CRNs) has proven a formidable challenge to cutting-edge tools. Underlying a CTSVAS is a continuous-time Markov chain (CTMC), and CTMC transient reachability analysis calls for Probabilistic Model Checking (PMC). This analysis requires the explicit representation of a model's entire state space. Rare events occur with extremely low probability, compounding the challenge of probabilistic analysis. In CRNs, it is imperative to verify the probability of rare events; even a low concentration of a species can have pathological consequences. This paper presents the RAGTIMER 1.0 tool, which efficiently builds a partial state space for a CTSVAS by enumerating traces to a rare event of interest and expanding them to exploit concurrency and cycles, providing a guaranteed lower bound on the probability of a rare event. Guaranteed lower bounds are particularly useful in synthetic biological applications because they indicate how and when a rare event can be experimentally observed. RAGTIMER is an attractive alternative to existing rare event analysis methods for CTSVAS models. It outperforms existing PMC tools and refutes multiple probability estimates from rare-event stochastic simulation on multiple challenging CRN models. RAGTIMER uses optimized data structures, a simple input format, and memory-safe Rust code to improve the scalability and accessibility of PMC for industry professionals.
