Abstraction-Based Safety Verification and Control of Cooperative Vehicles at Road Intersections

This article considers the problem of designing a centralized controller for vehicle collision avoidance at road junctions and intersections. The controller supervises a set of vehicles, and overrides their inputs when necessary to prevent side and rear-end collisions. By supervising vehicles, rather than taking full control, we obtain a system that can work with semiautomated human-driven vehicles. The price to pay is in complexity: an override is only necessary if, without an intervention, all future input signals will result in a collision. Thus, deciding overrides requires verification of the full reachability set, rather than the computation of a single collision-free trajectory. Our approach to speeding this step up is to use an abstraction of the (concrete) system, which is suitably discretized to obtain a mixed-integer programming problem. We deduce the solution of the original verification problem (VP) from that of the abstraction-based VP by proving an approximate simulation relation between the abstract and concrete systems. The resulting supervisor provably guarantees safety of the concrete system. We also evaluate the approximation error of the supervisor due to the use of an abstraction. Computer simulations show that the supervisor exhibits computationally better performances than other existing controllers applicable to realistic intersection scenarios.