Safety verification and control for collision avoidance at road intersections

Abstract

Car crashes cause a large number of fatalities and injuries, with about 33,000 people killed and 2.3 million injured in the United States every year. To prevent car crashes, the government and automotive companies have taken initiatives to develop and deploy communications among vehicles and between vehicles and infrastructure. By using such communications, we design centralized coordinators at road intersections, called supervisors, that monitor the dynamical state of vehicles and the current input of drivers and override them if necessary to prevent a collision. The primary technical problem in the design of such systems is to determine if the current drivers' input will cause an unavoidable future collision, in which case the supervisor must override the drivers at the current time to prevent the collision. This problem is called safety verification problem which is known to be computationally intractable for general dynamical systems. Our approach to solving the safety verification problem is to translate it to a computationally more tractable scheduling problem. When modeling an intersection as a single conflict area inside which the paths of vehicles intersect, we exactly solve the scheduling problem with algorithms that can handle a small number of vehicles in real-time. For a larger number of vehicles or with more complex intersection models, we approximately solve it within quantified approximation bounds by using mixed integer linear programming (MILP) formulations that, despite the combinatorial complexity, can be solved in real-time by available software such as CPLEX. Based on the solutions to the safety verification problem, we design a supervisor and prove that it ensures safety and is nonblocking, another major challenge of verification-based algorithms. We validate the supervisor using computer simulations and experiments.