A Spatial Logic for Modeling and Verification of Collision-Free Control of Vehicles
Bingqing Xu, Qin Li · 2016
Spatio-temporal information is essential for specifying and verifying Internet of Vehicles (IoV). Multi-lane spatial logic (MLSL) is a real-time spatial logic that can specify constraints in traffic manoeuvres on multi-lane motorways. It turns out to be a promising way to specify the properties of traffic manoeuvres because of its domain specificity and simplicity in modeling and reasoning. In this paper, we extend MLSL by introducing vertical lanes that intersect with the horizontal lanes. And this allows us to specify more complex road conditions including turning, crossroads and blocked road. The application of the extended spatial logic and the enriched traffic control model is then demonstrated on traffic scenes like T-junction to check safety properties such as collision avoidance.