Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Radu-Florin Tulcan, Rose Bohrer, Yoàv Montacute, Kevin Zhou, Yusuke Kawamoto, Ichiro Hasuo

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.

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

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.

Paper Structure

This paper contains 27 sections, 10 theorems, 12 equations, 3 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Environment modeling.
  4. Hybrid and Spatiotemporal Logics.
  5. Verification of CPS.
  6. Hybrid Spatiotemporal Logic for Automotive Safety
  7. Syntax
  8. Semantics
  9. Nontrivial validities
  10. Nontrivial non-validities
  11. Modeling
  12. Model-Checking
  13. Formula evaluation
  14. Remark.
  15. Model-checkers
  16. ...and 12 more sections

Key Result

theorem 1

For every grid-graph $G$, trace $\vec{t}$, point $p_{i,j}$ in the grid-graph, and HSTL formula $\varphi$, $\texttt{Eval}(G, \vec{t}, p_{i,j}, \varphi)$ (as defined in Algorithm alg:evaluator) returns True if and only if $G, \vec{t}, p_{i,j} \models \varphi$. Furthermore, Eval terminates within $O(|\

Figures (3)

  • Figure 1: A $3\times 4$ grid-graph
  • Figure 2: A model satisfying the formula $\varphi_2$
  • Figure 3: A model satisfying the formula $\varphi_3$

Theorems & Definitions (25)

  • definition 1: Syntax
  • definition 2: Grid-graph
  • definition 3: States & traces
  • definition 4: Semantics
  • definition 5: Modeling idioms
  • theorem 1: Correctness and runtime of formula evaluator
  • theorem 2: Correctness and complexity of the motion algorithm
  • proposition 1: Commutation of orthogonal moves
  • proof
  • proposition 2: Loops on the grid
  • ...and 15 more