安全性仕様のためのシナリオベース合成統計モデル検査
Scenario-Based Compositional Statistical Model Checking for Safety Specifications
複合シナリオをプリミティブに分解し、重要度サンプリングとカーネル密度推定で統計的検証を合成することで、未見の複合シナリオでも効率的に安全性を評価するフレームワークを提案した。
著者: Abhinav Pomalapally, Arya Raeesi, Kevin Kai-Chun Chang, Beyazit Yalcinkaya, Sanjit A. Seshia
分類: cs.LO, cs.AI, cs.RO, cs.SE, eess.SY
原文アブストラクト
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.