dorsal/arxiv
View SchemaFormal Safety Guarantees for Autonomous Vehicles using Barrier Certificates
| Authors | Oumaima Barhoumi, Mohamed H Zaki, Sofiène Tahar |
|---|---|
| Categories | |
| ArXiv ID | 2601.09740vv1 |
| URL | https://arxiv.org/abs/2601.09740 |
| License | http://creativecommons.org/licenses/by-nc-nd/4.0/ |
Abstract
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.
{
"annotation_id": "d397b817-4beb-4f18-a3fd-2c97d66db653",
"date_created": "2026-02-17T05:53:24.171000Z",
"date_modified": "2026-02-17T05:53:24.171000Z",
"file_hash": "c7cad27e8f7e014d449cd0814ae91b8152835f246ebb02640441ce56aa46dc91",
"private": false,
"record": {
"abstract": "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.",
"arxiv_id": "2601.09740",
"authors": [
"Oumaima Barhoumi",
"Mohamed H Zaki",
"Sofi\u00e8ne Tahar"
],
"categories": [
"cs.RO",
"cs.AI",
"cs.SE"
],
"license": "http://creativecommons.org/licenses/by-nc-nd/4.0/",
"title": "Formal Safety Guarantees for Autonomous Vehicles using Barrier Certificates",
"url": "https://arxiv.org/abs/2601.09740",
"version": "v1"
},
"schema_id": "dorsal/arxiv",
"source": {
"execution_id": "fd9c080b-343e-4214-bad7-6eadf5ac2c91",
"id": "arXiv Dataset",
"type": "Model",
"variant": "snapshot-2026-01-17",
"version": "0.1.0"
},
"user_id": 1000002
}