バリア証明を用いた自動運転車の形式的な安全保証
Formal Safety Guarantees for Autonomous Vehicles using Barrier Certificates
バリア証明と解釈可能な衝突指標（TTC）を組み合わせ、SMTソルバで安全性を検証する適応制御を提案。実データで危険な相互作用を最大40%削減した。
著者: Oumaima Barhoumi, Mohamed H Zaki, Sofiène Tahar
分類: cs.RO, cs.AI, cs.SE
原文アブストラクト
Modern AI technologies enable autonomous vehicles to perceive complex scenes, predict human behavior, and make real-time driving decisions. However, these data-driven components often operate as black boxes, lacking interpretability and rigorous safety guarantees. Autonomous vehicles operate in dynamic, mixed-traffic environments where interactions with human-driven vehicles introduce uncertainty and safety challenges. This work develops a formally verified safety framework for Connected and Autonomous Vehicles (CAVs) that integrates Barrier Certificates (BCs) with interpretable traffic conflict metrics, specifically Time-to-Collision (TTC) as a spatio-temporal safety metric. Safety conditions are verified using Satisfiability Modulo Theories (SMT) solvers, and an adaptive control mechanism ensures vehicles comply with these constraints in real time. Evaluation on real-world highway datasets shows a significant reduction in unsafe interactions, with up to 40\% fewer events where TTC falls below a 3 seconds threshold, and complete elimination of conflicts in some lanes. This approach provides both interpretable and provable safety guarantees, demonstrating a practical and scalable strategy for safe autonomous driving.