Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking

TL;DR

This paper introduces HSTL, a hybrid spatiotemporal logic tailored for automotive safety, with optimized model-checking algorithms that significantly improve performance in common driving scenarios.

Contribution

The paper presents a novel hybrid spatiotemporal logic for automotive safety and develops optimized model-checking algorithms with exponential performance gains.

Findings

Optimized algorithms reduce search space based on reachable states.

Exponential performance improvement observed in evaluations.

Effective modeling of scenarios like safe following and overtaking.

Abstract

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.