# Spatio-Temporal Framework for Verifying Safety Rules in Autonomous Vehicles

### Maksym Labzhaniia

Université Côte d'Azur,
Inria, CNRS, I3S, Kairos
Sophia Antipolis, France
maksym.labzhaniia@inria.fr

### Marie-Agnès Peraldi-Frati

Université Côte d'Azur,
Inria, CNRS, I3S, Kairos
Sophia Antipolis, France
marie-agnes.peraldi@univ-cotedazur.fr

### Julien Deantoni

Université Côte d'Azur,
Inria, CNRS, I3S, Kairos
Sophia Antipolis, France
julien.deantoni@univ-cotedazur.fr

### Frédéric Mallet

Université Côte d'Azur,
Inria, CNRS, I3S, Kairos
Sophia Antipolis, France
frederic.mallet@univ-cotedazur.fr

UNIVERSITÉ
CÔTE D'AZUR

<figure><img src="image_1.png" /></figure>

ÉCOLE UNIVERSITAIRE DE RECHERCHE
SYSTÈMES NUMÉRIQUES
POUR L'HUMAIN

<figure><img src="image_2.png" /></figure>

Initiative d'Excellence

## Abstract

With the increasing prevalence of vehicle driving automation systems (henceforth colloquially referred to as autonomous) on roads, the frequency and severity of accidents involving these vehicles have exceeded initially anticipated. It heightens global awareness of the need to enhance the safety standards of autonomous cars. One way to increase the safety of autonomous vehicles in this regard is by imposing safety rules on them, which they must respect. For instance, a safety designer could require that “the ego vehicle should always maintain a distance of at least 4 seconds from the vehicle in front.” Such safety rules often mix space and time in their expression, which makes them challenging to check via classical frameworks based on temporal logic. In this paper, we propose the definition of a formal framework dedicated to verifying spatiotemporal properties related to vehicles within a road network. One can then employ the designed framework to assess offline if a given driving scenario is safe concerning specified properties of this kind. More interestingly, one of the essential framework features is that it allows, given a current traffic configuration, to evaluate whether it is safe for the ego vehicle to perform this or that action based on projected futures under some traffic hypotheses, thus safeguarding the ego vehicle’s driving policy. While still in its infancy, the proposed framework paves the way for defining a Domain-Specific Language for specifying these safety rules; it may consequently

serve as an integral part of autonomous vehicles' safety assessment process, of both physical ones and ones within simulators.

## CCS Concepts

* Computer systems organization → Embedded and cyberphysical systems; Computing methodologies → Model verification and validation; Theory of computation → Timed and hybrid models; Software and its engineering → Specification languages.

## Keywords

driving automation system, autonomous vehicle, safety rules, spatiotemporal, formal framework, domain specific language

## ACM Reference Format:

Maksym Labzhaniia, Julien Deantoni, Marie-Agnès Peraldi-Frati, and Frédéric Mallet. 2024. Spatio-Temporal Framework for Verifying Safety Rules in Autonomous Vehicles. In *ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems (MODELS Companion '24)*, September 22-27, 2024, Linz, Austria. ACM, New York, NY, USA, 10 pages. https://doi.org/10.1145/3652620.3687813

## 1 Introduction

Autonomous vehicles have many potential benefits, positively affecting those who will directly engage with them and others indirectly, too [7]. Here and henceforth, “autonomous” and “self-driving” are colloquial and suggest driving automation.

That said, safety remains a concern for people regarding autonomous vehicles. According to a poll, most Americans (87%) believe that standards concerned with regular vehicles are inadequate for ensuring the safety and effectiveness of self-driving cars and that the latter shall conform to a higher testing standard [11]. Moreover, even though a statistic attributes the proximate reason for

MODELS Companion '24, September 22-27, 2024, Linz, Austria

© 2024 Copyright held by the owner/author(s).

This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems (MODELS Companion '24), September 22-27, 2024, Linz, Austria, https://doi.org/10.1145/3652620.3687813.
the critical pre-crash event to the driver in 94% of the crashes [16], which may make one expect self-driving cars to be substantially less involved in accidents, not everything is so rosy. For example, there have been crashes involving Teslas in Autopilot mode, i.e., Tesla's driver assistance system, and both fatalities and serious injuries definitively linked to the system [15]. Thus, despite self-driving cars inherently eliminating the risk of a driver-related crash, additional crashes have occurred, revealing some safety defects later assigned to the driver-assistance software of those vehicles or the technology overall [10].

The software of an autonomous vehicle is mission-critical, complex, and sophisticated — its verification and validation are crucial yet challenging [9]. For instance, test-driving or other statistical approaches to verify autonomous vehicles' reliability are inadequate to assure all the parties of autonomous vehicles' safety [5]. Consequently, other methods are requisite.

There is a safety standard [4] whose scope covers driving automation systems having levels of driving automation, according to [13], from driver assistance (Level 1) to full driving automation (Level 5). Its goal is to facilitate the process of ensuring the absence of unreasonable risk resulting from functional insufficiencies of intended functionalities that require proper situational awareness and thus rely on complex sensors and processing algorithms. According to the standard, one may frame the overall process of achieving the safety of the intended functionality (SOTIF) to be minimizing unsafe scenarios—where a scenario understood as a temporal sequence of scenes [17]—both known and unknown, for a driving automation system of interest, within a particular operational design domain (ODD). Although the standard only serves as a framework and guidance rather than a concrete solution, this understanding fosters the scenario-based approach to ensuring autonomous vehicle safety [12].

This paper presents a formal framework for defining safety rules and verifying compliance for autonomous vehicles.

Our framework facilitates higher-level reasoning about safety in more abstract terms, thereby avoiding the limitations associated with statistical, data-driven safety approaches. The developed framework allows operating with spatio-temporal concepts, enabling the verification of properties for the ego vehicle pertaining not only to the current configuration — which involves analyzing positions of objects, different zones, and their spatial relationships — but also to potential future configurations reachable from the current one within a specified time frame.

The designed framework features an abstraction of material road networks, i.e., an ad hoc transition system that can capture a road network's static objects. The abstraction is inspired by and consistent with ASAM OpenDRIVE [1] — a standard defining a common encoding format of static road networks. All entities utilized within the abstraction have corresponding counterparts within the standard, and the abstraction preserves the relationships between those entities as they are within OpenDRIVE. This alignment ensures compatibility and seamless integration of the presented framework with other state-of-the-art tools that, in this regard, adhere to Open-DRIVE.

Given this road network representation, one can place traffic participants, i.e., the ego vehicle and others, specifying their positions and velocities. We then introduce spatial entities, called zones,

and define the concept of a collision at a high level as an overlap of some specific zones corresponding to objects.

This paper offers a scenario safety checking procedure relative to safety rules one can specify via the designed framework to safeguard the ego vehicle's driving policy. For example, one may consider a scenario safe if, in all of its scenes, there are no crashes anticipated for the ego vehicle within the next four seconds (or another amount of time), for some (all, or most) of the possible futures and their corresponding trajectories of the ego vehicle. Therefore, the framework is to align effectively with SOTIF's iterative process.

Lastly, the framework may inherently detect incoherence within a safety specification by identifying spatial and temporal inconsistencies resulting from ensuring compliance with its rules.

The rest of the paper focuses on the framework presentation. After an overview, in section 2, of some existing contributions to scenario-based and formal methods approaches to autonomous vehicles' safety, section 3 presents the constituents of our framework, the intuition behind them as well as their formalization, and describes a scenario safety checking process involving our framework also providing a running example. Section 4 concludes the paper by summarizing the preliminary results and outlining perspectives for future work.

## 2 Related Work

This section presents some relevant contributions to the scenario-based and formal methods approaches to autonomous vehicles' safety.

In [8], the authors categorize scenarios into three tiers, arranged according to how abstract they are, i.e., functional, logical, and concrete. Functional scenarios are the most abstract ones: they comprise operating scenarios from a semantic perspective. Logical scenarios are the functional ones translated into some formalism to specify what values state space variables may assume. One obtains concrete scenarios from logical ones by substituting each variable with a specific value from the variable's range; they are integral to test cases. We show within this paper how, given a functional scenario, one may represent it as a logical one via the framework's constructs and then test whether a corresponding concrete scenario is safe.

The definitions of those tiers were initially to align with specific process steps described in the ISO 26262 standard [3]. Despite ISO 26262 addressing functional safety, which is complementary to the SOTIF aspect of safety, one may use the same scenario categorization to reason about nominal safety.

In [2], the authors classify state space variables used to represent scenes for logical and concrete scenarios, and, consequently, the entities to which those variables correspond, into five layers, i.e., *Road-level*, *Traffic infrastructure*, *Temporary manipulation of L1 and L2*, *Objects*, and *Environment*, which are numbered by numbers from 1 to 5, respectively.

In [6], the authors present a framework for setting general problem statements for testing, verification, and falsification tasks for embedded control systems. The apparatus' constituencies are a system $M$, a set of parameters $P$, a set of inputs $U$, and a property $\psi$ the system shall fulfill. Then, given parameter $p \in P$ and input $u \in U$, we denote the behavior of system $M$ under $p$ and $u$
by $\Phi(M, p, u)$. All the tasks thus boil down to determine whether $\Phi(M, p, u)$ satisfies $\psi$, which we denote by $\Phi(M, p, u) \models \psi$. Within the autonomous vehicles' safety domain, $M$ could be a driving automation system, the ego vehicle, either a physical one or within a simulator; $P$ could represent possible settings of the ego vehicle, and $U$ a set of concrete scenarios relative to a particular ODD.

In [18], the authors provide an overview of formal safety techniques for verification, validation, and certification in autonomous vehicle development.

In [14], the authors propose a mathematical model for safety assurance and describe a system design that adheres to it. They focus on nominal safety, similar to our approach, utilizing concepts such as longitudinal and lateral safe distances and proper responses.

# 3 Framework Description

This section presents the core of our contribution – a formal framework dedicated to expressing and validating safety rules for autonomous vehicles that mix realistic spatio-temporal constraints. It features different abstract entities: street network abstraction, traffic participants, spatial zones, and projecting in the future that allows, given a placing of participants within the network, anticipating their future locations within a specified time frame. Via those possible futures, one can verify spatial propositions within branching time.

We define a *street network abstraction* based on ASAM OpenDRIVE's static road network description format. The entities we introduce fall within the *Road-level* and *Traffic infrastructure* layers. We thus ensure the compatibility of our abstraction with various state-of-the-art simulators and facilitate integration with ongoing research in the field.

We then introduce the notion of a *spatial zone* that allows, given a position within a street network abstraction and longitudinal offsets both backward and forward, to define a part of the street network abstraction to which this zone corresponds.

Further, we add *road traffic participants*, which are within the scope of the *Objects* layer. We pay special attention to vehicles since they are principal on roads and include the ego vehicle, i.e., the object whose nominal safety is the primary concern of this research. The ego vehicle's lateral and longitudinal motion is integral to the framework presented within the paper; consequently, the framework is the most relevant to vehicles whose driving automation may execute the corresponding control subtasks. Road traffic participants' positions within a street network abstraction thus define a configuration. Knowing a configuration and the dimensions of the objects, one may then compute specific spatial zones, e.g., the vehicles' collision zones. Then, if the collision zones of two vehicles overlap within a given configuration, the configuration features a collision.

Last but not least, probing the future is one of the essential features of the presented framework that allows one to reason not only about the current configuration but also about reachable configurations in the future. Thus, one can define in our framework properties, i.e., *safety rules* the ego vehicle must satisfy, that incorporate, among other things, the requirements for a bounded future. We do that via a projection function, i.e., a function that, given

<figure><img src="image_3.png" /><figcaption>Figure 1: A static road network.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Figure 2: The street network abstraction corresponding to Figure 1.</figcaption></figure>

a configuration and an amount of time, provides the set of configurations reachable from that configuration within the specified time.

Lastly, we present a safety-checking process designed and exhibit an illustrative example combining all the framework constructs and featuring the rule that the ego vehicle shall not collide within some time $t$. According to the process, one can thus check a scenario's compliance with the rule and consider safe only those scenarios that satisfy it.

## 3.1 Street Network Abstraction

Here, we define the street network abstraction inspired by the ASAM OpenDRIVE standard. We inherit several attributes from OpenDRIVE, including roads, the road's reference line coordinate system – primarily the longitudinal s-axis – road partitioning into lane sections along the s-axis, and lanes with the integer representation of their lateral aspect and driving directions.
The following shall also hold

$$
\begin{equation} \tag{8}
\begin{array}{l@{\qquad}l@{\qquad}l}
\forall \text{lane}_1, \text{lane}_2, s, s', s_*, s_* &
  (\text{lane}_1, \text{lane}_2, [s, s']) \in \mathcal{T}_{\mathcal{L}}^{\text{merge}} & \wedge \\[2ex]
(\text{lane}_1, \text{lane}_2, [s_*, s_*']) \in \mathcal{T}_{\mathcal{L}}^{\text{merge}} &
  [s, s'] \cap [s_*, s_*] \neq \emptyset & \Rightarrow \\[1ex]
\phantom{(\text{lane}_1, \text{lane}_2, [s_*, s_*'])} &
  s = s_* \land s' = s_*'.
\end{array}
\end{equation}
$$

Subformula (1) ensures merging may be feasible solely from
a lane to a neighboring lane. The subformula starting at (2) and
until (3) guarantees that the s-coordinate span $[s, s']$ at which it
is possible to change lanes is indeed a non-empty segment of both
the source and the target lanes.

As for the second type of transition, equations (4) and (5) state
that only one of a lane's endpoints may serve as a contact point
of a linkage depending on whether the lane is the source or target
of the linkage and the lane's driving direction. The requirement is
necessary to guarantee the coherency of the linkage transitions:
passing from one lane to another is dynamic and thus features
instantaneous velocity; we, in turn, want this velocity to respect the
driving directions of both the source lane and the target one. Further,
the linked lanes may belong to the same or different roads. For the
former, subformula (6) requires no discontinuity between lanes. For
the latter, subformula (7) demands the source and target lanes to be
the longitudinally outermost lanes of their corresponding roads, i.e.,
comprising the minimum or maximum s-coordinate within their
corresponding roads. Lastly, formula (8) guarantees the minimality
and uniqueness of the representation of the transitions between
adjacent lanes.

These transitions are logical rather than physical, i.e., they de-
scribe the lane changes allowed by traffic rules rather than the
feasibility of a maneuver that puts a car in the other lane.

A street network abstraction (henceforth simply a street net-
work) is thus a triple ($\mathcal{L}$, $\mathcal{T}_{\mathcal{L}}^{\text{merge}}$, $\mathcal{T}_{\mathcal{L}}^{\text{linkage}}$), where $\mathcal{L}$ is a state set,
and $\mathcal{T}_{\mathcal{L}}^{\text{merge}}$ and $\mathcal{T}_{\mathcal{L}}^{\text{linkage}}$ are a merge and linkage transition set
relative to $\mathcal{L}$, respectively.

3.2 Spatial Zones

This subsection defines the concept of a zone within a street net-
work, highlighting a particular kind of zone of interest.

Preliminarily, we want to define an entity, henceforth a *spatial zone*, so that it comprises a given number of meters “behind” and a given number of meters “in front” of a given coherent position within a street network.

We first introduce longitudinally connected subnetworks. One
may think of a subnetwork as a linear graph having as vertices
lanes of a street network and as edges, though implicitly, linkage
transitions.

Definition 3.3 (of a subnetwork) . Given a state set $\mathcal{L}$, a set of link-
age transitions $\mathcal{T}_{\mathcal{L}}^{\text{linkage}}$, an origin position $(\text{lane}_{\text{from}}, s_{\text{from}}) \in$
$\text{Pos}_{\mathcal{L}}$, and a destination position $(\text{lane}_{\text{to}}, s_{\text{to}}) \in \text{Pos}_{\mathcal{L}}$, one defines
the set of all subnetworks that longitudinally connect the point
lying on $\text{lane}_{\text{from}}$ and having s-coordinate $s_{\text{from}}$ with the one on

$\text{lane}_{\text{to}}$ with $s_{\text{to}}$ as follows:

$$
\begin{align*}
& \text{subnetwork} \in \text{Subnetworks}_{(\text{lane}_{\text{to}}, s_{\text{to}})}^{(\text{lane}_{\text{from}}, s_{\text{from}})} && \Leftrightarrow \\
& \exists n \in \mathbb{N}^{+} && \\
& \text{subnetwork} = \left( (\text{lane}_1, s_1^1), (\text{lane}_1, s_1^2), \right. && \\
& \phantom{\text{subnetwork} = \left(} \text{lane}_2, \dots, \text{lane}_{n-1}, && \wedge \\
& \phantom{\text{subnetwork} = \left(} (\text{lane}_n, s_n^1), (\text{lane}_n, s_n^2) \right) && \\
(9) \quad & \text{lane}_1 = \text{lane}_{\text{from}} \wedge s_1^1 = s_{\text{from}} && \wedge \\
& \text{lane}_n = \text{lane}_{\text{to}} \wedge s_n^2 = s_{\text{to}} && \wedge \\
& \left( \text{proj}_{\mathcal{L}}^{\rightarrow} (\text{lane}_1) = 1 \Rightarrow s_1^1 \le s_1^2 \right) && \wedge \\
(10) \quad & \left( \text{proj}_{\mathcal{L}}^{\rightarrow} (\text{lane}_1) = -1 \Rightarrow s_1^1 \ge s_1^2 \right) && \wedge \\
(11) \quad & \left( n \ge 2 \right) && \Rightarrow \\
(12) \quad & \left( \text{proj}_{\mathcal{L}}^{\rightarrow} (\text{lane}_1) = -1 \right) && \Rightarrow \\
& s_1^2 = \text{proj}_{\mathcal{L}}^{\text{start}} (\text{lane}_1) && \wedge \\
(13) \quad & \left( \text{proj}_{\mathcal{L}}^{\rightarrow} (\text{lane}_1) = 1 \right) && \Rightarrow \\
& s_1^2 = \text{proj}_{\mathcal{L}}^{\text{end}} (\text{lane}_1) && \wedge \\
(14) \quad & \left( \text{proj}_{\mathcal{L}}^{\rightarrow} (\text{lane}_n) = -1 \right) && \Rightarrow \\
& s_n^1 = \text{proj}_{\mathcal{L}}^{\text{end}} (\text{lane}_n) && \wedge \\
(15) \quad & \left( \text{proj}_{\mathcal{L}}^{\rightarrow} (\text{lane}_n) = 1 \right) && \Rightarrow \\
& s_n^1 = \text{proj}_{\mathcal{L}}^{\text{start}} (\text{lane}_n) && \wedge \\
(16) \quad & \left( \forall i \in \overline{2, n-1} \text{ lane}_i \in \mathcal{L} \right) && \wedge \\
& \forall i \in \overline{2, n} && \\
(17) \quad & (\text{lane}_{i-1}, \text{lane}_i) \in \mathcal{T}_{\mathcal{L}}^{\text{linkage}}). &&
\end{align*}
$$

In other words, a subnetwork is a sequence of lanes connected
by linkage transitions leading from the source point to the target
point within a street network.

The first lane, i.e., lane₁, is where the source point, (lane<sub>from</sub>, s<sub>from</sub>), is located. The last one, lane<sub>n</sub>, is, in turn, the lane to which the target point, (lane<sub>to</sub>, s<sub>to</sub>), belongs. In general, the first lane and the last one belong to a subnetwork only partly; a subnetwork designates those parts explicitly, each by two points, s<sub>1</sub><sup>1</sup>, s<sub>1</sub><sup>2</sup>, and s<sub>n</sub><sup>1</sup>, s<sub>n</sub><sup>2</sup>, respectively, thus defining their respective segments constituting the subnetwork. Those segments shall respectively originate from the source point, i.e., (lane<sub>from</sub>, s<sub>from</sub>), and end at the target point, i.e., (lane<sub>to</sub>, s<sub>to</sub>). Also, those parts shall respect the driving directions of their corresponding lanes. All this follows from Equations (9) to (10).

At (11), we start defining conditions for subnetworks comprising
two or more lanes. The sub-formula at (12) states that the first
lane's point connecting it to the subsequent lane of a subnetwork
is the first lane's start if the first lane's driving direction is negative.
If, in turn, it is positive, according to the sub-formula at (13), the connecting point is the first lane's end. A similar is for the last lane of a subnetwork: according to the sub-formula at (14) and the one at (15), if the driving direction is negative (positive), the last lane's end (start) serves as the contact point with the previous lane within the subnetwork. The sub-formula at (16) explicitly asserts that the elements of a subnetwork other than the segments of the first and last lanes are lanes of the street network. We interpret a subnetwork as spanning its intermediate lanes in their entirety. Lastly, the sub-formula at (17) asserts the connectivity between a subnetwork's lanes.

The length of a subnetwork is the length of the first lane's segment plus the sum of all the intermediate lanes' lengths plus the length of the last lane's segment (for subnetworks of two or more lanes):

$$I_{\text{subnet}} : \text{Subnetworks}_{(\text{lane}_{to}, s_{to})}(\text{lane}_{from}, s_{from}) \to \mathbb{R}_{\ge 0}$$

$$I_{\text{subnet}} = \lambda((\text{lane}_1, s_1^1), (\text{lane}_1, s_1^2), \text{lane}_2, \dots, \\ \text{lane}_{n-1}, (\text{lane}_n, s_n^1), (\text{lane}_n, s_n^2)).$$

$$|s_1^2 - s_1^1| + [n \ge 2] \cdot |s_n^2 - s_n^1| + \sum_{i=2}^{n-1} (\text{proj}_{\mathcal{L}}^{\text{end}}(\text{lane}_i) - \text{proj}_{\mathcal{L}}^{\text{start}}(\text{lane}_i)).$$

The following criterion defines whether a coherent position lies within a given subnetwork.

**LEMMA 3.4.** *Given a coherent position within the street network (lane, s) ∈ Pos<sub>L</sub> and subnetwork, a subnetwork between two coherent positions, i.e., an element of some Subnetworks<sub>(lane<sub>to</sub>,s<sub>to</sub>)</sub>(lane<sub>from</sub>,s<sub>from</sub>), the position (lane, s) is in subnetwork subnetwork if and only if*

$$\exists n \in \mathbb{N}^+ \text{ subnetwork} = ((\text{lane}_1, s_1^1), (\text{lane}_1, s_1^2), \text{lane}_2, \dots, \\ \text{lane}_{n-1}, (\text{lane}_n, s_n^1), (\text{lane}_n, s_n^2)) \quad \wedge \\ \left( \left( \text{lane} = \text{lane}_1 \quad \wedge \quad \\ s \in [\min\{s_1^1, s_1^2\}, \max\{s_1^1, s_1^2\}] \right) \quad \vee \\ \left( \text{lane} = \text{lane}_n \quad \wedge \quad \\ s \in [\min\{s_n^1, s_n^2\}, \max\{s_n^1, s_n^2\}] \right) \quad \vee \\ \exists i \in \overline{2, n-1} \text{ lane} = \text{lane}_i \quad \wedge \\ s \in [\text{proj}_{\mathcal{L}}^{\text{start}}(\text{lane}_i), \text{proj}_{\mathcal{L}}^{\text{end}}(\text{lane}_i)] \right).$$

Thus, a position is in a subnetwork if and only if it is within the segment of its first lane, the segment of its target lane, or within any of its intermediate lanes.

The following is the definition of a general zone, which is a set of s-coordinate intervals within the lanes of the street network.

**Definition 3.5 (of a zone within the street network).** A zone relative to the street network is an element of the following set:

$$\text{Zones} = \left\{ \begin{array}{l} \text{Zones} \in \left. \begin{array}{l} \mathcal{P}\{(\text{lane}, s_1, s_2) \mid \text{lane} \in \mathcal{L} \quad \wedge \\ (\text{lane}, s_1), (\text{lane}, s_2) \in \text{Pos}_{\mathcal{L}} \quad \wedge \\ [s_1, s_2] \neq \emptyset\} \end{array} \right| \\ (18) \quad \forall \text{lane} \in \mathcal{L} \quad \forall s_1, s_2, s'_1, s'_2 \in \\ \quad [\text{proj}_{\mathcal{L}}^{\text{start}}(\text{lane}), \text{proj}_{\mathcal{L}}^{\text{end}}(\text{lane})] \\ \quad ((\text{lane}, s_1, s_2) \in \text{zone} \quad \wedge \\ (\text{lane}, s'_1, s'_2) \in \text{zone}) \quad \Rightarrow \\ \quad ([s_1, s_2] \cap [s'_1, s'_2] = \emptyset \quad \vee \\ [s_1, s_2] = [s'_1, s'_2]); \end{array} \right\}$$

we will thus denote an individual zone by zone.

The formula (18) asserts minimality, meaning that two different intervals of a zone cannot cover the same coherent position. Minimality implies uniqueness: given a set of coherent positions, exactly one zone covers it.

Two zones intersect if and only if there is an interval of the first overlapping with an interval of the second, i.e., given zone and zone' — elements of Zones, we assume they intersect and denote that by zone ∩ zone' ≠ 0, only if

$$\exists \text{lane} \in \mathcal{L} \quad \exists s_1, s_2, s'_1, s'_2 \in [\text{proj}_{\mathcal{L}}^{\text{start}}(\text{lane}), \text{proj}_{\mathcal{L}}^{\text{end}}(\text{lane})] \\ (\text{lane}, s_1, s_2) \in \text{zone} \quad \wedge \\ (\text{lane}, s'_1, s'_2) \in \text{zone}' \quad \wedge \\ [s_1, s_2] \cap [s'_1, s'_2] \neq \emptyset.$$

**Definition 3.6 (of a spatial zone).** Given $d_r, d_f \in \mathbb{R}_{>0}$ and $\text{pos} \in \text{Pos}_L$, one can define a *spatial zone*, denoted by $\text{Spatial}_{d_r}^{d_f}(\text{pos})$, as the unique *zone* satisfying the following:

$$\begin{array}{l} \forall (\text{lane}, s) \in \text{Pos}_{\mathcal{L}} \quad \left( \exists s_1, s_2 \quad s \in [s_1, s_2] \quad \wedge \right. \\ \qquad (\text{lane}, s_1, s_2) \in \text{Spatial}_{d_r}^{d_f}(\text{pos}) \quad \left. \Rightarrow \right. \\ \qquad \exists \text{pos}_r, \text{pos}_f \in \text{Pos}_{\mathcal{L}} \\ \qquad \exists \text{subnetwork}_r \in \text{Subnetworks}_{\text{pos}_r}^{\text{pos}} \\ \qquad \exists \text{subnetwork}_f \in \text{Subnetworks}_{\text{pos}}^{\text{pos}_f} \\ \qquad \begin{array}{l} I_{\text{subnet}}(\text{subnetwork}_r) = d_r \quad \wedge \\ I_{\text{subnet}}(\text{subnetwork}_f) = d_f \quad \wedge \\ ((\text{lane}, s) \text{ is in subnetwork subnetwork}_r \quad \vee \\ (\text{lane}, s) \text{ is in subnetwork subnetwork}_f). \end{array} \end{array}$$

Thus, the spatial zone $\text{Spatial}_{d_r}^{d_f}(\text{pos})$ extends $d_r$ meters behind and $d_f$ meters in front of position pos in the sense that it covers
a given position (lane, s) only if there is a subnetwork, such that pos splits it into two subnetworks, the first leading to pos and of length $d_r$ and the second originating in pos and of length $d_f$, and the given position (lane, s) is within either of them.

## 3.3 Road Traffic Participants

We now define road users confining ourselves, for the time being, only to vehicles. We denote the vehicle set by $V$ and define a function egoVehicle: $1 \to V$, where 1 is a singleton, thus distinguishing the ego vehicle from the other vehicles. We thus require $V$ not to be empty and include at least one vehicle, namely the vehicle of interest.

The state of a vehicle consists of its position within the street network and the instantaneous value of its velocity.

**Definition 3.7 (of a vehicle configuration).** A configuration of the vehicles within the street network is an element of the following set:

$$ M_{\mathcal{L}}^{V} = \left\{ \begin{array}{l} f \in (\mathcal{L} \times \mathbb{R}_{\ge 0} \times \mathbb{R}_{\ge 0} \times \{-1, 1\})^{V} \\ \forall v \in V \quad f(v) = (\text{lane, coordinate, speed, direction}) \\ \qquad (\text{lane, coordinate}) \in \text{Pos}_{\mathcal{L}}^{V} \end{array} \right\}. $$

Given a vehicle $v \in V$ and a configuration $f \in M_{\mathcal{L}}^{V}$, within the definition above, the component lane of $f(v)$ is the lane $v$ is driving on relative to $f$; the component coordinate is the s-coordinate of $v$ relative to $f$ — the pair (lane, coordinate) shall thus be a coherent position; the component direction designates whether $v$ is driving in the right or wrong direction regarding the direction of movement of lane: it assumes 1 if the vehicle drives in the right direction and -1 otherwise; lastly, speed is the longitudinal speed of $v$, and, together with direction, it defines the instantaneous velocity of $v$ relative to $f$.

We now introduce collision zones for the vehicles representing their shapes within the street network. First, we define the longitudinal dimension of a vehicle by specifying a bidirectional offset relative to its reference point, which is the vehicle's longitudinal center and whose position we capture within a configuration as the vehicle's position. We thus introduce a function Dimension: $V \to \mathbb{R}_{>0}$ that maps each vehicle to its longitudinal dimension, i.e., it specifies the number of meters the vehicle occupies longitudinally in both directions relative to its reference point. Using a vehicle's longitudinal center as its reference point, for both capturing the vehicle's position within a configuration and computing its shape within the street network, eliminates the need to reason about its orientation.

**Definition 3.8 (of a collision zone).** The collision zone of vehicle $v$ concerning configuration $f$ is determined by first applying the function described below to $f$, followed by applying the resulting image to $v$:

$$ \text{Collision: } M_{\mathcal{L}}^{V} \to \left\{ \begin{array}{l} \text{Spatial}^{d_f}(\text{pos}) \\ \left( \exists v \in V \ d_r = d_f = \text{Dimension}(v) \right) \wedge \text{pos} \in \text{Pos}_{\mathcal{L}}^{V} \end{array} \right\}^{V}, $$

such that

$$ \begin{array}{l} \text{Collision}(f)(v) = \text{Spatial}_{\text{Dimension}(v)}^{\text{Dimension}(v)}(\text{pos}_v) \wedge \\ (\text{lane}_v, \text{coordinate}_v, \_, \_) = f(v) \wedge \\ \text{pos}_v = (\text{lane}_v, \text{coordinate}_v). \end{array} $$

Let us consider, for instance, the collision zone of the ego-vehicle relative to a configuration $f$, i.e., Collision($f$)($\text{ego\_vehicle}(*)$). In its essence, the definition asserts that this collision zone is the spatial zone centered at the position of the ego vehicle's reference point relative to configuration $f$ and comprising the same number of meters, given by Dimension($\text{ego\_vehicle}(*)$), both behind and in front. As with any other spatial zone, it may combine more than one subnetwork, but only one corresponds to the ego vehicle's genuine shape within the street network. In this sense, the configurations are generally forgetful, meaning they may forget the authentic shapes of the vehicles. The ambiguity in determining the precise shape of the ego vehicle arises from a configuration capturing nothing but the position of the ego's sole point within the street network, i.e., of its reference point. Consequently, multiple variants that satisfy the conditions of Definition 3.6 exist, each corresponding to a different subnetwork. Our approach integrates all these potential shapes into a unified collision zone. Although the resulting zone generally contains some positions beyond the genuine shape, it ensures a safer representation.

**Definition 3.9 (of a collision in the street network).** Given a configuration $f$ and two vehicles, $v_1$ and $v_2$, there is a collision between them if and only if the predicate defined below evaluates to true when applied to them:

$$ \begin{array}{l} \text{are\_colliding: } M_{\mathcal{L}}^{V} \times V \times V \to \mathbb{B} \\ \text{are\_colliding}(f, v_1, v_2) = \text{true} \\ \qquad \text{Collision}(f)(v_1) \cap \text{Collision}(f)(v_2) \neq \emptyset. \end{array} $$

Thus, given a configuration, two vehicles collide according to our framework exactly when their collision zones relative to the configuration intersect.

## 3.4 Projecting Future

Given a configuration $f \in M_{\mathcal{L}}^{V}$ and a time $t \in \mathbb{R}_{>0}$, one can compute the possible future configurations attainable from configuration $f$ once the time given by $t$ elapses. To be more precise, one can do that relative to and via a projection function. A projection function may assume the empty set as its value, which is a way to say that we cannot predict that far out via the given projection function for the given configuration. We also design means for tracking the itinerary of the ego vehicle, each corresponding to a potential future configuration. We use that information to evaluate the safety implications of driving decisions concerning temporal lane changes resulting from applying linkage transitions, thereby providing crucial feedback to the driving policy.

**Definition 3.10 (of a projection function).** We introduce a projection function as

$$ \rho: M_{\mathcal{L}}^{V} \times \mathbb{R}_{>0} \to \mathcal{P}(M_{\mathcal{L}}^{V} \times (\mathcal{L} \times \mathbb{R}_{>0})^{*}), $$
Thus, a given configuration is safe concerning the given property of interest only if there is an itinerary of the ego vehicle, w, spanning four seconds, as required by the property, corresponding to a sequence of configurations, $f_0, \dots, f_n$, timestamped by the given quantities of time, $t_0, \dots, t_n$, and ordered by them, i.e., each successive configuration is reachable from its predecessor within the time that elapses between their corresponding timestamps. Further, due to the transitivity, the last one, $f_n$, is consequently reachable from the initial one, $f_0$, within four seconds, and, lastly, none of the configurations within the sequence features a collision involving the ego vehicle. Each itinerary that, if substituted for w in subformula (35), makes the subformula evaluate to true is safe. One can compute such itineraries by concatenating the itineraries between successive configurations, and that is correct, again, due to the transitivity property.

## 4 Conclusion

This paper presents a designed formal framework encompassing static and dynamic aspects of road networks and traffic participants. As for its static part, the framework abstracts a conventional road network description format provided by the ASAM OpenDRIVE standard, thus inherently ensuring and facilitating integration with and conformity to the state-of-the-art tools and practices that adhere to OpenDRIVE. The framework enables one to define safety rules featuring both time and space properties and subsequently check compliance of driving scenarios with these rules, thus determining whether the given scenarios are safe relative to the given safety specification. Given that numerous safety metrics rely on crash frequency when examining autonomous vehicles, our framework introduces a rigorous definition of a collision. The framework, however, enables one to require not only the simple absence of collisions but also more intricate conditions. One of the framework's main features is that it not only determines whether the current situation is safe but also estimates the possible futures, their safety, and potentially safe and unsafe itineraries for the ego vehicle at the moment of evaluation. In the future, we plan to develop a domain-specific language for defining safety specifications for autonomous vehicles. The language is to rely on our framework for its expressiveness and semantics. It thus shall be able to define spatial-temporal rules. Besides, the role of the framework within the planned workflow is also to test and verify scenarios regarding user specifications in our language in conjunction with autonomous driving simulators. Thus, by doing that, we anticipate being able to implement the safety-checking procedure proposed within the paper in its entirety.

## Acknowledgments

This work has been supported by the French government, through the France 2030 investment plan managed by the Agence Nationale de la Recherche, as part of the "UCA DS4H" project, reference ANR-17-EURE-0004.

## References

[1] ASAM. 2023. *OpenDRIVE*. Standard 1.8.0. Association for Standardization of Automation and Measuring Systems. https://www.asam.net/standards/detail/opendrive/

[2] Gerrit Bagschik, Till Menzel, and Markus Maurer. 2018. Ontology based Scene Creation for the Development of Automated Vehicles. In *2018 IEEE Intelligent Vehicles Symposium (IV)*. IEEE, Changshu, China, 1813–1820. https://doi.org/10.1109/IVS.2018.8500632 ISSN: 1931-0587.

[3] International Organization for Standardization. 2018. Road vehicles — Functional safety. https://www.iso.org/standard/68383.html

[4] International Organization for Standardization. 2022. Road vehicles — Safety of the intended functionality. https://www.iso.org/standard/77490.html

[5] Nidhi Kalra and Susan M. Paddock. 2016. *Driving to Safety: How Many Miles of Driving Would It Take to Demonstrate Autonomous Vehicle Reliability?* Technical Report RR-1478-RC. RAND Corporation, Santa Monica, CA, United States. 15 pages. https://doi.org/10.7249/RR1478

[6] James Kapinski, Jyotirmoy V. Deshmukh, Xiaoqing Jin, Hisahiro Ito, and Ken Butts. 2016. Simulation-Based Approaches for Verification of Embedded Control Systems: An Overview of Traditional and Advanced Modeling, Testing, and Verification Techniques. *IEEE Control Systems Magazine* 36, 6 (Dec. 2016), 45–64. https://doi.org/10.1109/MCS.2016.2602089 Conference Name: IEEE Control Systems Magazine.

[7] Todd Litman. 2023. *Autonomous Vehicle Implementation Predictions: Implications for Transport Planning*. Technical Report. Victoria Transport Policy Institute, Victoria, Canada. 49 pages. https://www.vtpi.org/avip.pdf

[8] Till Menzel, Gerrit Bagschik, and Markus Maurer. 2018. Scenarios for Development, Test and Validation of Automated Vehicles. In *2018 IEEE Intelligent Vehicles Symposium (IV)*. IEEE, Changshu, China, 1821–1827. https://doi.org/10.1109/IVS.2018.8500406 ISSN: 1931-0587.

[9] B. Padmaja, CH. V. K. N. S. N. Moorthy, N. Venkateswarulu, and Myneni Madhu Bala. 2023. Exploration of issues, challenges and latest developments in autonomous cars. *Journal of Big Data* 10, 1 (May 2023), 61. https://doi.org/10.1186/s40537-023-00701-y

[10] The Dawn Project. 2022. Critical safety issues revealed by The Dawn Project's testing of Tesla Full Self-Driving. https://dawnproject.com/critical-safety-issues-revealed-by-the-dawn-projects-testing-of-tesla-full-self-driving/

[11] Lee Rainie, Cary Funk, Monica Anderson, and Alec Tyson. 2022. *AI and Human Enhancement: Americans' Openness Is Tempered by a Range of Concerns*. Survey Analysis Report. Pew Research Center, Washington, DC, United States. 164 pages. https://www.pewresearch.org/science/2022/03/17/ai-and-human-enhancement-americans-openness-is-tempered-by-a-range-of-concerns/ Chapter 4: Americans cautious about the deployment of driverless cars.

[12] Stefan Riedmaier, Thomas Ponn, Dieter Ludwig, Bernhard Schick, and Frank Diermeyer. 2020. Survey on Scenario-Based Safety Assessment of Automated Vehicles. *IEEE Access* 8 (2020), 87456–87477. https://doi.org/10.1109/ACCESS.2020.2993730 Conference Name: IEEE Access.

[13] SAE International Recommended Practice. 2021. Taxonomy and Definitions for Terms Related to Driving Automation Systems for On-Road Motor Vehicles. https://doi.org/10.4271/J3016_202104

[14] Shai Shalev-Shwartz, Shaked Shammah, and Amnon Shashua. 2018. On a Formal Model of Safe and Scalable Self-driving Cars. https://doi.org/10.48550/arXiv.1708.06374 [arXiv:1708.06374 [cs, stat]]

[15] Faiz Siddiqui and Jeremy B. Merrill. 2023. *17 fatalities, 736 crashes: The shocking toll of Tesla's Autopilot*. Washington Post, San Francisco, United States. https://www.washingtonpost.com/technology/2023/06/10 tesla-autopilot-crashes-elon-musk/ Section: Technology.

[16] Santokh Singh. 2015. *Critical Reasons for Crashes Investigated in the National Motor Vehicle Crash Causation Survey*. Traffic Safety Facts Crash-Stats. Report DOT HS 812 115. A Brief Statistical Summary. National Highway Traffic Safety Administration, Washington, DC, United States. https://crashstats.nhtsa.dot.gov/Api/Public/ViewPublication/812115

[17] Simon Ulbrich, Till Menzel, Andreas Reschka, Fabian Schuldt, and Markus Maurer. 2015. Defining and Substantiating the Terms Scene, Situation, and Scenario for Automated Driving. In *2015 IEEE 18th International Conference on Intelligent Transportation Systems*. IEEE, Gran Canaria, Spain, 982–988. https://doi.org/10.1109/ITSC.2015.164 ISSN: 2153-0017.

[18] Tong Zhao, Ekim Yurtsever, Joel A. Paulson, and Giorgio Rizzoni. 2023. Formal Certification Methods for Automated Vehicle Safety Assessment. *IEEE Transactions on Intelligent Vehicles* 8, 1 (Jan. 2023), 232–249. https://doi.org/10.1109/TIV.2022.3170517