Counterexample-Guided Safety Contracts for Autonomous Driving
Ensuring the safety of autonomous vehicles is paramount for their successful deployment. However, formally verifying autonomous driving decisions systems is difficult. In this paper, we propose a frame-work for constructing a set of safety contracts that serve as design requirements for con...
| Main Authors: | , , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
2020
|
| Online Access: | https://hdl.handle.net/1721.1/123848 |
| _version_ | 1826217846529589248 |
|---|---|
| author | DeCastro, Jonathan Liebenwein, Lucas Vasile, Cristian-Ioan Tedrake, Russell L Karaman, Sertac Rus, Daniela L |
| author2 | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
| author_facet | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science DeCastro, Jonathan Liebenwein, Lucas Vasile, Cristian-Ioan Tedrake, Russell L Karaman, Sertac Rus, Daniela L |
| author_sort | DeCastro, Jonathan |
| collection | MIT |
| description | Ensuring the safety of autonomous vehicles is paramount for their successful deployment. However, formally verifying autonomous driving decisions systems is difficult. In this paper, we propose a frame-work for constructing a set of safety contracts that serve as design requirements for controller synthesis for a given scenario. The contracts guarantee that the controlled system will remain safe with respect to probabilistic models of traffic behavior, and, furthermore, that it will fol-low rules of the road. We create contracts using an iterative approach that alternates between falsification and reachable set computation. Counterexamples to collision-free behavior are found by solving a gradient-based trajectory optimization problem. We treat these counter examplesas obstacles in a reach-avoid problem that quantifies the set of behaviors an ego vehicle can make while avoiding the counterexample. Contracts are then derived directly from the reachable set. We demonstrate that the resulting design requirements are able to separate safe from unsafe behaviors in an interacting multi-car traffic scenario, and further illustrate their utility in analyzing the safety impact of relaxing traffic rules. Keyword: Logic and Verification; Collision Avoidance; Falsification; Rules of the Road |
| first_indexed | 2024-09-23T17:10:06Z |
| format | Article |
| id | mit-1721.1/123848 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T17:10:06Z |
| publishDate | 2020 |
| record_format | dspace |
| spelling | mit-1721.1/1238482022-10-03T10:53:19Z Counterexample-Guided Safety Contracts for Autonomous Driving DeCastro, Jonathan Liebenwein, Lucas Vasile, Cristian-Ioan Tedrake, Russell L Karaman, Sertac Rus, Daniela L Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Massachusetts Institute of Technology. Department of Aeronautics and Astronautics Rus, Daniela Ensuring the safety of autonomous vehicles is paramount for their successful deployment. However, formally verifying autonomous driving decisions systems is difficult. In this paper, we propose a frame-work for constructing a set of safety contracts that serve as design requirements for controller synthesis for a given scenario. The contracts guarantee that the controlled system will remain safe with respect to probabilistic models of traffic behavior, and, furthermore, that it will fol-low rules of the road. We create contracts using an iterative approach that alternates between falsification and reachable set computation. Counterexamples to collision-free behavior are found by solving a gradient-based trajectory optimization problem. We treat these counter examplesas obstacles in a reach-avoid problem that quantifies the set of behaviors an ego vehicle can make while avoiding the counterexample. Contracts are then derived directly from the reachable set. We demonstrate that the resulting design requirements are able to separate safe from unsafe behaviors in an interacting multi-car traffic scenario, and further illustrate their utility in analyzing the safety impact of relaxing traffic rules. Keyword: Logic and Verification; Collision Avoidance; Falsification; Rules of the Road 2020-02-24T19:16:50Z 2020-02-24T19:16:50Z 2018-12 Article http://purl.org/eprint/type/ConferencePaper https://hdl.handle.net/1721.1/123848 De Castro, Jonathan et al. "Counterexample-Guided Safety Contracts for Autonomous Driving." The 13th International Workshop on the Algorithmic Foundations of Robotics, December 2018, Merida, Mexico. en_US https://parasol.tamu.edu/wafr/wafr2018/program.php Proceedings of the 13th Workshop on the Algorithmic Foundations of Robotics Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Prof. Rus |
| spellingShingle | DeCastro, Jonathan Liebenwein, Lucas Vasile, Cristian-Ioan Tedrake, Russell L Karaman, Sertac Rus, Daniela L Counterexample-Guided Safety Contracts for Autonomous Driving |
| title | Counterexample-Guided Safety Contracts for Autonomous Driving |
| title_full | Counterexample-Guided Safety Contracts for Autonomous Driving |
| title_fullStr | Counterexample-Guided Safety Contracts for Autonomous Driving |
| title_full_unstemmed | Counterexample-Guided Safety Contracts for Autonomous Driving |
| title_short | Counterexample-Guided Safety Contracts for Autonomous Driving |
| title_sort | counterexample guided safety contracts for autonomous driving |
| url | https://hdl.handle.net/1721.1/123848 |
| work_keys_str_mv | AT decastrojonathan counterexampleguidedsafetycontractsforautonomousdriving AT liebenweinlucas counterexampleguidedsafetycontractsforautonomousdriving AT vasilecristianioan counterexampleguidedsafetycontractsforautonomousdriving AT tedrakerusselll counterexampleguidedsafetycontractsforautonomousdriving AT karamansertac counterexampleguidedsafetycontractsforautonomousdriving AT rusdanielal counterexampleguidedsafetycontractsforautonomousdriving |