发表机构
University of California, Berkeley（加州大学伯克利分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对安全关键系统中组合场景验证成本高的问题，提出基于场景的组合式统计模型检验框架，通过分解场景与规范、独立验证及重要性采样和核密度估计组合结果，实现高效准确验证并降低模拟成本。
AI 中文摘要
在自动驾驶等安全关键领域，系统必须在大量环境条件下进行评估，这些条件通常表示为由原始场景构建的组合场景。现有的统计模型检验（SMC）方法独立分析每个组合场景，需要大量昂贵的模拟，并且在场景共享共同结构时导致大量冗余计算。本工作引入了一种用于安全和共同安全规范的基于场景的组合式SMC框架，能够高效分析组合场景。我们的方法将场景分解为原始场景，将规范分解为子规范，独立验证每个原始场景，并使用重要性采样和核密度估计组合所得的统计估计。我们的实证评估表明，所提出的框架能够准确回答先前未见过的组合场景的验证查询，同时通过并行化和轨迹重用降低模拟成本。
英文摘要
In safety-critical domains such as autonomous driving, systems must be evaluated across a large number of environment conditions, often represented as composite scenarios built from primitive scenarios. Existing statistical model checking (SMC) approaches analyze each composite scenario independently, requiring many expensive simulations and resulting in substantial redundant computation when scenarios share common structure. This work introduces a scenario-based compositional SMC framework for safety and co-safety specifications, enabling efficient analysis of composite scenarios. Our approach decomposes scenarios into primitives and specifications into sub-specifications, verifies each primitive independently, and composes the resulting statistical estimates using importance sampling and kernel density estimation. Our empirical evaluation shows that the proposed framework can accurately answer verification queries for previously unseen composite scenarios while reducing simulation cost through parallelization and trace reuse.
Comments24 pages, 8 figures, 5 tables. Extended version of paper accepted to The 26th International Conference on Runtime Verification (RV 2026)
