Formal Safety Guarantees for Autonomous Vehicles using Barrier Certificates
This addresses safety challenges for autonomous vehicles by providing interpretable and provable guarantees, though it is incremental as it builds on existing formal methods.
The paper tackled the problem of ensuring safety for autonomous vehicles in dynamic, mixed-traffic environments by developing a formally verified framework using Barrier Certificates and Time-to-Collision metrics, resulting in up to 40% fewer unsafe interactions and complete elimination of conflicts in some lanes.
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.