标题： 通过仿射向量空间推理随机向量加法系统中的罕见事件可达性 显示英文标题

标题： Reasoning about Rare-Event Reachability in Stochastic Vector Addition Systems via Affine Vector Spaces

摘要： 在随机向量加法系统（VAS）中，罕见事件具有重要研究价值，因为尽管它们极其不可能发生，但可能代表有害的行为，可能会产生不良影响。 它们的低概率和潜在的巨大状态空间对现有的概率模型检查和随机罕见事件模拟技术构成了挑战。 特别是在化学反应网络（CRNs）中，一种通常以VAS表示的化学动力学语言，罕见事件的影响可能是病理性的。 我们提出了两种新的启发式方法，用于优先级优先的部分状态空间扩展和轨迹生成，专门针对VAS中罕见事件概率的瞬态分析：迭代子空间缩减（ISR）和单距离优先（SDP）。 这两种方法都构建一个包含所有解状态的闭合向量空间。 SDP然后仅优先考虑到这个“解空间”的较短距离，而ISR构建一组嵌套的子空间，其中短且高概率的满足轨迹很可能依次通过。 每种方法产生的部分状态图包含通往罕见事件状态的可能轨迹，使得高效的概率模型检查能够计算出感兴趣罕见事件的下限概率。 这些方法是确定性的、快速的，并在具有挑战性的CRN模型上表现出显著的性能。 显示英文摘要

摘要： Rare events in Stochastic Vector Addition System (VAS) are of significant interest because, while extremely unlikely, they may represent undesirable behavior that can have adverse effects. Their low probabilities and potentially extremely large state spaces challenge existing probabilistic model checking and stochastic rare-event simulation techniques. In particular, in Chemical Reaction Networks (CRNs), a chemical kinetic language often represented as VAS, rare event effects may be pathological. We present two novel heuristics for priority-first partial state space expansion and trace generation tuned to the transient analysis of rare-event probability in VAS: Iterative Subspace Reduction (ISR) and Single Distance Priority (SDP). Both methods construct a closed vector space containing all solution states. SDP then simply prioritizes shorter distances to this ``solution space'', while ISR constructs a set of nested subspaces, where short and highly-probable satisfying traces are likely to pass through in sequence. The resulting partial state graph from each method contains likely traces to rare-event states, allowing efficient probabilistic model checking to compute a lower-bound probability of a rare event of interest. These methods are deterministic, fast, and demonstrate marked performance on challenging CRN models.