Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915894707355648 |
|---|---|
| author | Tulcan, Radu-Florin Bohrer, Rose Montacute, Yoàv Zhou, Kevin Kawamoto, Yusuke Hasuo, Ichiro |
| author_facet | Tulcan, Radu-Florin Bohrer, Rose Montacute, Yoàv Zhou, Kevin Kawamoto, Yusuke Hasuo, Ichiro |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_24443 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking Tulcan, Radu-Florin Bohrer, Rose Montacute, Yoàv Zhou, Kevin Kawamoto, Yusuke Hasuo, Ichiro Logic in Computer Science 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. |
| title | Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2603.24443 |