Modeling and Verification of Variable Multi-Lane Intersection Controls for Autonomous Vehicles Using Uppaal SMC

With the spread of autonomous vehicles, all vehicles may be centrally controlled in the near future and it will become important for the group controller to ensure that a fleet of autonomous vehicles runs safely and efficiently. This study models intersections with variable lanes and applies model checking and statistical model checking to show safety and efficiency of the model. By conducting verification assuming rush hour conditions, the effectiveness of the proposed control rules is demonstrated, where the uncertainty of vehicle occurrences is addressed by statistical model checking.