Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking
This work addresses safety verification for autonomous vehicles in highway scenarios, representing an incremental advancement in formal methods for automotive applications.
The authors tackled the problem of verifying automotive safety specifications for highway driving by introducing a hybrid spatiotemporal logic (HSTL) and developing model-checking algorithms for it. They demonstrated an exponential performance improvement with their optimized algorithms when evaluated on common driving scenarios like safe following and overtaking.
We introduce a hybrid spatiotemporal logic for automotive safety applications (HSTL), focused on highway driving. Spatiotemporal logic features specifications about vehicles throughout space and time, while hybrid logic enables precise references to individual vehicles and their historical positions. We define the semantics of HSTL and provide a baseline model-checking algorithm for it. We propose two optimized model-checking algorithms, which reduce the search space based on the reachable states and possible transitions from one state to another. All three model-checking algorithms are evaluated on a series of common driving scenarios such as safe following, safe crossings, overtaking, and platooning. An exponential performance improvement is observed for the optimized algorithms.