# Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance

Jesse Reimann, Nico Mansion, James Haydon, Benjamin Bray, Agnishom Chattopadhyay, Sota Sato, Masaki Waga, Étienne André, Ichiro Hasuo, Naoki Ueda, et al.

► To cite this version:

Jesse Reimann, Nico Mansion, James Haydon, Benjamin Bray, Agnishom Chattopadhyay, et al. Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance. 39th ACM/SIGAPP Symposium On Applied Computing (SAC 2024), Apr 2024, Avila, Espagne, Spain. pp.186-195, 10.1145/3605098.3636014. hal-04654301

HAL Id: hal-04654301

https://hal.science/hal-04654301v1

Submitted on 20 Mar 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
# Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance*

Jesse Reimann†‡

TU Delft
Delft, The Netherlands

Nico Mansion†‡

Saarland University
Saarbrücken, Germany

James Haydon

National Institute of Informatics
Tokyo, Japan

Benjamin Bray

National Institute of Informatics
Tokyo, Japan

Agnishom Chattopadhyay‡

Rice University
Houston, Texas, USA

Sota Sato

NII & SOKENDAI
Tokyo, Japan

Masaki Waga

Kyoto University & NII
Kyoto, Japan

Étienne André

Université Sorbonne Paris Nord,
LIPN, CNRS, UMR 7030, F-93430
Villetaneuse, France

Ichiro Hasuo

NII & SOKENDAI
Tokyo, Japan

Naoki Ueda

Mitsubishi Electric Corporation
Kamakura, Japan

Yosuke Yokoyama

Mitsubishi Electric Corporation
Kamakura, Japan

## ABSTRACT

As the development of autonomous vehicles progresses, efficient safety assurance methods become increasingly necessary. Safety assurance methods such as monitoring and scenario-based testing call for formalisation of driving scenarios. In this paper, we develop a temporal-logic formalisation of an important class of critical scenarios in the ISO standard 34502. We use signal temporal logic (STL) as a logical formalism. Our formalisation has two main features: 1) modular composition of logical formulas for systematic and comprehensive formalisation (following the compositional methodology of ISO 34502); 2) use of the RSS distance for defining danger. We find our formalisation comes with few parameters to tune thanks to the RSS distance. We experimentally evaluated our formalisation; using its results, we discuss the validity of our formalisation and its stability with respect to the choice of some parameter values.

## CCS CONCEPTS

* Theory of computation → Modal and temporal logics; Logic and verification; * Computer systems organization → Real-time system specification.

## KEYWORDS

automated driving, temporal logic, formal methods, safety, monitoring

## ACM Reference Format:

Jesse Reimann, Nico Mansion, James Haydon, Benjamin Bray, Agnishom Chattopadhyay, Sota Sato, Masaki Waga, Étienne André, Ichiro Hasuo, Naoki Ueda, and Yosuke Yokoyama. 2024. Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance. In *The 39th ACM/SIGAPP Symposium on Applied Computing (SAC '24), April 8–12, 2024, Avila, Spain*. ACM, New York, NY, USA, 10 pages. https://doi.org/10.1145/3605098.3636014

## 1 INTRODUCTION

To increase social acceptance of automated driving vehicles (ADVs), addressing safety concerns is vital. The safety vision of the UNECE World Forum for Harmonization of Vehicle Regulations (WP.29) states that the level of safety should be such that ADVs "shall not cause any traffic accidents resulting in injury or death that are reasonably foreseeable and preventable" [8].

One path towards realising this vision is scenario-based testing of vehicle controllers [21]. For this approach, a library of critical scenarios is compiled, and the behaviour of the path-planning algorithm in these situations is observed through simulations. Compared to a posteriori analysis of recorded driving data, this allows for cost-efficient testing and adjustments of controllers, as it is not necessary to record new driving data after algorithmic changes.

Efforts towards standardising test-scenario based ADV safety evaluations include ISO Standard 34502 [12]. This standard derives relevant scenarios by systematically identifying risk factors related to vehicle perception, traffic conditions, and vehicle control. Combining these factors yields a large number of critical scenarios.

Most efforts towards specifying critical scenarios use a combination of natural language descriptions and suitably chosen parameter value ranges, see e.g. [20]. An alternative is formalisation of critical

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

<footnote>*The work is partially supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST START Grant (No. JPMJST2213), and JST CREST Grant (No. JPMJCR2012). J. Reimann is supported by a fellowship of the German Academic Exchange Service (DAAD). É. André is partially supported by ANR-NRF ProMiS (ANR-19-CE25-0015) and ANR BisoUS (ANR-22-CE48-0012).</footnote>

<footnote>†Equal contribution</footnote>

<footnote>‡Work done during the stay at National Institute of Informatics (NII), Tokyo, Japan</footnote>
scenarios, in some formal language with a rigorously defined semantics, so that 1) the content of each scenario is mathematically well-defined, and 2) those scenarios can be *mechanically processed* by software. A typical example of such processing is *monitoring*, i.e. detecting occurrences of scenarios automatically in a driving log.

A class of formal languages particularly suitable for this purpose is temporal logics, pioneered by Pnueli [23]. Temporal logics can be thought of as extensions of propositional logics with so-called temporal operators, allowing for statements that refer to temporal relationships such as *always* or *eventually* in the future. Well-known examples of temporal logics are LTL, CTL and CTL\*; they all have discrete notions of time. For the purpose of formalising critical scenarios, their extensions to continuous time are suited, such as *metric temporal logic (MTL)* [14] and *signal temporal logic (STL)* [19].

In this paper, we provide a logical formalisation in STL of an important class of critical scenarios in ISO 34502, namely *traffic disturbance scenarios* for general vehicles on highways. Our formalisation has two unique characteristics. The first one is its modularity: a common template of the formulas for different scenarios is first fixed, and then the component formulas in the template are instantiated. This construction—it mirrors the top-down compositional methodology in ISO 34502—aids systematic, comprehensive formalisation. The second characteristic is the use of the *RSS distance* [28], a distance considered safe between two moving vehicles, for defining danger. We find that this makes our formalisation more stable by reducing the number of parameters to be tuned. We also report our use of our tool called *STL Debugger* to improve our workflow.

In general, a formalisation of critical scenarios in temporal logic has two main usages: *scenario-based testing* (where a vehicle controller and a scenario are given and we search for a traffic situation in which the controller behaves as specified in the scenario) and *monitoring* (where a driving log and a scenario are given and we search for those segments of the log which match the scenario). We note that there are a body of sophisticated tools that accept STL formulas, for scenario-based testing [1, 5, 32, 33] and for monitoring [30]. Our formalisation can be readily utilised by these tools.

*Contributions.* Our technical contributions are as follows.

* We provide a set of logical formulas describing traffic disturbance scenarios based on ISO 34502.

* The two unique characteristics of our formalisation (namely modularity and the use of the RSS distance) suggest a general methodology for formalising various driving scenarios, beyond those in ISO 34502.

* We evaluate the adequacy of the traffic disturbance scenario descriptions in ISO 34502 and propose an extension.

* Experimental evaluation of our formulas demonstrates that we detect nearly all traffic disturbances in a given dataset.

*Organisation.* We introduce the conceptual and logical framework of our formalisation in §2 and §3. Our formalisations *ISO34502-STL* and *ISO34502-STL-ext* and the formulas used to construct them are introduced in §4. We describe the experimental evaluation of our formulas in §5, and summarise our results in §6.

Towards of our formalisation, we used our tool *STL Debugger* for deriving and debugging STL formulas. The tool and our use of it is discussed in [25, Appendix B].

*Related work.* The RSS framework [28] is based on the assumption that all vehicles comply with pre-defined proper responses to potentially critical scenarios. In our work, we use the RSS framework to obtain a safety metric suitable to the logical formalisation of critical scenarios without the notion of responsibility implied by the proper responses. Some proper responses from [28] were formalised in STL in [11]. Suitable parameter ranges for calibrating the RSS distance are studied e.g. in [13]. On the use of RSS for verifying safety, recent developments are found e.g. in [10].

There are several efforts to formalise traffic rules in temporal logic, such as selected laws from the German StVO relating to interstate roads [18], dual carriageways [6], and intersections [17], as well as marine laws [16]. These works formalise rules to be obeyed and thus use the *always* modality often, while ours is about *disturbance* and thus primarily uses the *eventually* and *until* modalities.

There are existing methods of detecting critical scenarios that rely on metrics such as time-to-collision (TTC) or jerk. In [22, 26, 34], critical scenarios resulting from cut-ins and braking are detected in monitored data. A more general workflow based on detecting critical thresholds for jerk and time-to-collision is proposed in [29]. The Virtual Assessment of Automation in Field Operation (VAAFO) [31] method uses, among other metrics, a weighted sum across potential driving paths is used to identify critical scenarios where a human driver is assisted by a Highly Automated Driving (HAD) system. Our logical formalisation is independent of our specific choice of a safety metric (namely the RSS distance); use of other metrics such as TTC is well possible. That said, we believe the choice of RSS distance is another contribution of ours: it is known to be one of the advanced and robust metrics, and can easily be accommodated in temporal-logic formalisation.

## 2 PRELIMINARIES

### 2.1 ISO Standard 34502

ISO 34502 [12] is a proposal of safety evaluation procedures of automated driving systems, based on a joint industry effort by Japanese automotive manufacturers [27]. *Critical scenarios*, defined in ISO 34502 as “scenario[s] including one or more risk factors”, are systematically constructed in a top-down manner by combining three categories of risk factors. They correspond to the three phases in the common automated driving pipeline, namely perception, planning, and control:

A *perception disturbance* includes intrinsic or extrinsic factors that can cause disturbance of sensors and cameras, such as light reflections or roadside objects. *Traffic disturbances* arise from road geometry or the behaviour of other traffic participants, such as dangerous cut-ins or braking. *Vehicle control disturbances* describe internal or external factors that impact the feasibility of certain maneuvers, such as vehicle weight distribution or strong winds.

By refining and systematically combining these risk factors, a large number of critical scenarios arises. This can be considered a set of reasonably foreseeable critical scenarios in which an ADV is expected to avoid collisions or minimise unavoidable accidents.

In this paper, we focus on *traffic disturbance scenarios* as defined in ISO 34502 for general vehicles on highways. They are composed of the following three components:
<figure><img src="image_3.png" /><figcaption>**Figure 1:** Left: Numbering of possible POV locations relative to SV. The fields numbered as "+1" are only relevant in three-vehicle scenarios. Right: Combinations of POV positions and behaviours that may cause critical scenarios. These are from [12].</figcaption></figure>

The first component is *road geometry*: On highways, one may assume that there are no intersections, roundabouts, or unstructured roads. The relevant road shapes for highways are thus non-intersection segments (straight or curved), merge zones where two roads merge into a single road, and departure zones, where an additional road branches off the main road.

The second component is *subject vehicle (SV) behaviour*. It is classified into either keeping the current lane (*lane keep*) or changing lanes (*lane change*). It is assumed that all vehicles behave reasonably, hence backwards driving or U-turns are not considered.

The last of the three components is *principle other vehicle (POV) behaviour*: The behaviour of the vehicles surrounding SV is assumed to cause a dangerous situation for the vehicles involved. Here, these behaviours are classified into either 1) changing into the lane of SV (*dangerous cut-in*), 2) leaving the lane of SV (*dangerous cut-out*), 3) driving dangerously fast behind SV (*acceleration*), or 4) driving dangerously slow in front of SV (*deceleration*). The location of POV relative to SV is used to exclude non-critical behaviours, e.g. SV will not be endangered if POV drives faster in front of it. For critical combinations of POV behaviours and vehicle locations, see Fig. 1.

Combining these three components results in 24 traffic disturbance scenarios, see Table 1. While SV may be surrounded by several POVs, traffic disturbance scenarios can generally be composed of subscenarios involving only two vehicles, thus a formalisation of the 24 scenarios in Table 1 is the foundation of more comprehensive sets of formalised scenarios, including many-vehicle scenarios.

However, a *three-vehicle cut-out* is included in Table 1, namely Scenario 2: There are two vehicles ahead of SV in the same lane as SV. The POV directly ahead of SV changes lanes, whereas the other POV remains in the lane. This scenario is critical when the POV remaining in the lane is slower than SV could reasonably expect, causing risk of collision.

## 2.2 STL

We formalise the traffic disturbance scenarios in ISO 34502 using *signal temporal logic* (STL) in a rigorous manner that can be used for monitoring purposes and scenario generation. STL [19] is an extension of temporal logics such as LTL (see e.g. [2]) that is designed

<figure><img src="image_4.png" /><figcaption>**Table 1:** General vehicle traffic disturbance scenarios on highways in ISO Standard 32502 [12] (the table is from [12]). The white vehicle represents SV, the darker vehicles the POVs, the arrows indicate the (intended) motion of the vehicles. The rightmost four columns refer to POV behaviour.</figcaption></figure>

to specify the behaviour of continuous-time signals in a succinct manner that nevertheless maintains readability for humans. The familiar propositional logic using the operators $\neg$, $\vee$, $\wedge$ is extended by adding temporal operators $G$, $F$, $U$ denoting the temporal notions always (or globally), eventually (or finally), and until. Formulas in STL are constructed inductively from the following grammar, where we let $f: \mathbb{R}^n \to \mathbb{R}$, $x \in \mathbb{R}^n$, $n \in \mathbb{N}$, and $J \subseteq \mathbb{R}$ an interval.

$$ \varphi ::= \top | \bot | f(x) > 0 | \neg\varphi | \varphi_1 \lor \varphi_2 | \\ \qquad \varphi_1 \land \varphi_2 | \varphi_1 U_j \varphi_2 | G_j \varphi | F_j \varphi. $$

Here, the subscript *J* denotes the restriction of an operator to a time interval *J* relative to the current time. As an example, consider a formula $G_{[2,3]}(v > 5)$. This formula is true at time *T* if the value of *v* is greater than 5 always from time *T* + 2 to time *T* + 3. If no interval *J* is specified, the formula is treated as if $J = [0, \infty)$.

The meaning of STL formulas is defined by their Boolean semantics, inductively defined in Table 2. The relationship $\sigma \models \varphi$ means that the formula $\varphi$ is true under a signal $\sigma: [0, \infty) \to \mathbb{R}^n$, $n \in \mathbb{N}$.

Particularly important in our formalisation are the semantics of the *until* operator $U$. For a formula $\varphi_1 U \varphi_2$ to be true at time *T*, it must hold that 1) $\varphi_1$ is true at some time $T' \ge T$ and 2) $\varphi_1$ is constantly true throughout the time interval $[T, T')$. Note that $\varphi_1$ is not required to be true at the time $T'$ when $\varphi_2$ first becomes true; the formula $\varphi_1 U \varphi_2$ is thus trivially true at time *T* if $\varphi_2$ is true at time *T*. This becomes important in our formalisation, see §4.3.

## 2.3 Road Network and Vehicle Configuration

To model our road network, we use lanelets [3] and their logical formalisation in [18], so that our formulas can be applied to a wide range of road shapes. A rigorous description of our road network can be found in [25, Appendix A].

In the current work, the relevance of lanelets is quite limited: they are used only in the very beginning of our workflow, for the purpose of mapping physical positions to lane coordinates. After that, the description of a disturbance scenario is independent of
<table><caption>Table 2: Boolean semantics of STL</caption><tr><td>σ ⊢ ⊤</td><td>↔ true</td></tr><tr><td>σ ⊢ ⊥</td><td>↔ false</td></tr><tr><td>σ ⊢ (f(x) > 0)</td><td>↔ f(σ(0)) > 0</td></tr><tr><td>σ ⊢ ¬φ</td><td>↔ σ ∄ φ</td></tr><tr><td>σ ⊢ φ<sub>1</sub> ∨ φ<sub>2</sub></td><td>↔ σ ⊢ φ<sub>1</sub> or σ ⊢ φ<sub>2</sub></td></tr><tr><td>σ ⊢ φ<sub>1</sub> ∧ φ<sub>2</sub></td><td>↔ σ ⊢ φ<sub>1</sub> and σ ⊢ φ<sub>2</sub></td></tr><tr><td>σ ⊢ φ<sub>1</sub>U<sub>j</sub>φ<sub>2</sub></td><td>↔ ∃t ∈ J : σ(· + t) ⊢ φ<sub>2</sub><br>and σ(· + t') ⊢ φ<sub>1</sub> for all t' < t in J</td></tr><tr><td>σ ⊢ F<sub>j</sub>φ</td><td>↔ ∃t ∈ J : σ(· + t) ⊢ φ</td></tr><tr><td>σ ⊢ G<sub>j</sub>φ</td><td>↔ ∀t ∈ J : σ(· + t) ⊢ φ</td></tr></table>

<figure><img src="image_5.png" /><figcaption>Figure 2: A sample road section (departure zone) constructed from lanelets forming two main road lanes (grey, attr(l) = main) and one departure lane (blue, attr(l) = departure). All depicted lanelets satisfy zone(l) = departZone. The driving direction is indicated by the arrow. The departure lane is adjacent to the lower main road lane but not adjacent to the upper main road lane.</figcaption></figure>

road geometry; this is seen e.g. in Table 3. In any case, here we give an informal overview of lanelets. For an illustration, see Fig. 2.

Lanelets are atomic road segments described by their (piecewise straight) left and right bounds. Each lanelet has an associated attribute, denoting whether it belongs to a main road lane or to a merge/departure lane, and an associated zone, stating whether the lanelet is part of an overall merge/departure zone of the road.

A lane is then defined as the set of all lanelets of the same attribute that pre- or succeed each other. Note that by this construction, a single lane cannot branch out and lead in two different directions; however, two lanes may overlap. We call two lanes $L_1$ and $L_2$ adjacent if there are some lanelets $l_1 \in L_1, l_2 \in L_2$, such that $l_1$ and $l_2$ share a boundary line but do not overlap.

We further follow [18] and model the dynamics of our vehicles as point masses described by $x = (s, v, a, d, \theta) \in \mathbb{R}^5$. Here $s$ denotes the position of the vehicle along a fixed reference path $\Gamma$ (typically the boundary of an outer lane), $v$ its velocity, and $a$ its acceleration. The lateral distance of the vehicle to $\Gamma$ is denoted by $d$, and its orientation relative to $\Gamma$ by $\theta$, see Fig. 3.

For different vehicles, we use subscripts for the variables: $x_\square = (s_\square, v_\square, a_\square, d_\square, \theta_\square)$ for a vehicle $\square$, where $\square$ is typically either $SV$ or $POV$; e.g. $v_{SV}$ is the velocity of $SV$. In formulas, we refer to $x_{SV}$ and $x_{POV}$ simply as $SV$ and $POV$. When no confusion with the acceleration is possible, we refer to generic vehicles as $a$ and $b$.

To define the occupancy of a vehicle, we associate a box of length $length(a)$ and width $width(a)$ with each vehicle $a$. We choose the front-left corner of this box as the point of which the location and dynamics are tracked, and define $occ(a, l)$ to be true if any part of the box associated with vehicle $a$ is within the road segment described

<figure><img src="image_6.png" /><figcaption>Figure 3: Curvilinear coordinates, with the reference path $\Gamma$ being the lower road boundary. Here, $s_a$ denotes the coordinate of the vehicle $a$ along the $\Gamma$, $d_a$ the distance of $a$ from $\Gamma$, and $\theta_a$ the orientation of the vehicle relative to $\Gamma$. See Section 2.3 for the definition of rear(a).</figcaption></figure>

by lanelet $l$, and false otherwise. Furthermore, we can define the coordinates front(a), rear(a) as the projection of the front and rear end of the vehicle onto the reference path. By construction, we have $front(a) = s_a$. On highways, we may assume that road segments are locally straight, hence we assume rear(a) $\approx s_a - length(a)$.

Longitudinal and lateral velocities of the vehicle relative to the reference path are given by $v_{long} := v \sin(\theta)$, $v_{lat} := v \cos(\theta)$.

### 3 TRAFFIC DISTURBANCE SCENARIO FORMALISATION

We follow the modular approach of ISO 34502 (§2.1) in our STL formalisation of its traffic disturbance scenarios for general vehicles on highways (Table 1). That is, we first fix a template of STL formulas that express traffic disturbance scenarios, and by varying the "parameters" (i.e. component subformulas) of the template, we systematically obtain the formalisation of different scenarios.

Our top-level formulas are scenario$_i$, for $i = 1, 2, \dots, 24$, each of which represents one of the traffic disturbance scenarios in Table 1. The format for these formulas scenario$_i$ is the following:

$$ \begin{aligned} \text{scenario}_i(SV, POV, L) &:= \text{initSafe}(SV, POV) \\ &\quad \wedge \text{roadSector}_i(SV, POV) \\ &\quad \wedge \text{disturb}_i(SV, POV, L). \end{aligned} \quad (1) $$

Here initSafe(SV, POV) is a formula—common to all scenarios—stating that there is no hazard at the start of the scenario for the duration of a pre-defined time interval; its definition is given in §4.3. The formula disturb$_i$ (SV, POV, L) expresses the content of the actual disturbance and is specific to each traffic disturbance scenario. Here, L denotes a lane relative to which the scenario is formalised.

We emphasise the importance of the formula initSafe(SV, POV). In fact, it was absent in our early trials, causing most disturbance formulas to be trivially true for certain traces. In particular, this problem occurs with traces that either start with danger between the observed vehicles or in which the monitored interval leading up to danger is too short; we return to this discussion in §5.3.

The formula roadSector$_i$ (SV, POV) corresponds to the road geometry component in §2.1, i.e. main road, merge zone, or departure zone. For details, see §4.6.

We label the set $\{\text{scenario}_i | i = 1, \dots, 24\}$ ISO34502-STL.
<caption>Table 3: Formalisation ISO34502-STL of general vehicle traffic disturbance scenarios of ISO 34502 (cf. §2.1) in STL. For definitions of initSafe and danger see §4.3, for all other subformula definitions see the section indicated in the corresponding column heading. For a discussion of the formulas see §4.6.</caption>

$\text{scenario}_i(\text{SV}, \text{POV}, L) := \text{initSafe}(\text{SV}, \text{POV}) \land \text{roadSector}_i(\text{SV}, \text{POV}) \land \text{disturb}_i(\text{SV}, \text{POV}, L), i = 1, \dots, 24 \text{ (cf. this is (1). initSafe is from §4.3)}$

$\text{disturb}_i(\text{SV}, \text{POV}, L) := \text{initialCondition}_i(\text{SV}, \text{POV}, L) \land \text{behaviourSV}_i(\text{SV}, L) \land \text{behaviourPOV}_i(\text{POV}, \text{SV}, L), i = 1, \dots, 24 \text{ (cf. (2) in §3)}$

<table><thead><tr><th>i</th><th>roadSector<sub>i</sub> (cf. §4.1)</th><th>i</th><th>initialCondition<sub>i</sub> (cf.§4.2)</th><th>behaviourSV<sub>i</sub> (cf.§4.4)</th><th>behaviourPOV<sub>i</sub> (cf.§4.5)</th></tr></thead><tbody><tr><td rowspan="8">1 – 8</td><td rowspan="8">mainRoad(SV, POV)</td><td>1</td><td>⊤</td><td>laneKeep(SV, L)<br>U danger(SV, POV)</td><td>cutIn(POV, SV)</td></tr><tr><td>2</td><td>sameLane<sub>3</sub>(SV, POV<sub>1</sub>, POV<sub>2</sub>, L)<br>∧aheadOf(SV, POV<sub>1</sub>)<br>∧aheadOf(POV<sub>1</sub>, POV<sub>2</sub>)</td><td>laneKeep(SV, L)<br>U (¬sameLane(SV, POV<sub>1</sub>, L))</td><td>leavingLane(POV<sub>1</sub>, L)<br>∧(laneKeep(POV<sub>2</sub>, L)<br>U (¬sameLane(POV<sub>2</sub>, POV<sub>1</sub>, L)<br>∧danger(SV, POV<sub>2</sub>)))</td></tr><tr><td>3</td><td>aheadOf(POV, SV)<br>∧(sameLane(SV, POV, L)<br>∀inAdjLanes(SV, POV, L))</td><td>laneKeep(SV, L)<br>U danger(SV, POV)</td><td>accel(POV, SV, L) U danger(SV, POV)</td></tr><tr><td>4</td><td>aheadOf(SV, POV)<br>∧(sameLane(SV, POV, L)<br>∀inAdjLanes(SV, POV, L))</td><td>laneKeep(SV, L)<br>U danger(SV, POV)</td><td>decel(POV, SV, L) U danger(SV, POV)</td></tr><tr><td>5</td><td>⊤</td><td>leavingLane(SV, L)</td><td>cutIn(POV, SV)</td></tr><tr><td>6</td><td>⊤</td><td>leavingLane(SV, L)</td><td>cutOut(POV, SV, L)</td></tr><tr><td>7</td><td>aheadOf(POV, SV)</td><td>enteringLane(SV, L)</td><td>accel(POV, SV, L) U danger(SV, POV)</td></tr><tr><td>8</td><td>sameLane(SV, POV, L)<br>∧aheadOf(SV, POV)</td><td>leavingLane(SV, L)</td><td>decel(POV, SV, L) U danger(SV, POV)</td></tr><tr><td>9–16</td><td>mergeZone(SV, POV)</td><td>9–16</td><td>initialCondition<sub>i–8</sub></td><td>behaviourSV<sub>i–8</sub></td><td>behaviourPOV<sub>i–8</sub></td></tr><tr><td>17–24</td><td>departZone(SV, POV)</td><td>17–24</td><td>initialCondition<sub>i–16</sub></td><td>behaviourSV<sub>i–16</sub></td><td>behaviourPOV<sub>i–16</sub></td></tr></tbody></table>

The general structure of our disturbance formulas $\text{disturb}_i$ is

$$ \begin{aligned} \text{disturb}_i(\text{SV}, \text{POV}, L) := & \text{initialCondition}_i(\text{SV}, \text{POV}, L) \\ & \land \text{behaviourSV}_i(\text{SV}, L) \quad (2) \\ & \land \text{behaviourPOV}_i(\text{POV}, \text{SV}, L) \end{aligned} $$

corresponding roughly to the latter two of the three components in §2.1, namely SV behaviour and POV behaviour. Each component of the template (2) is as follows.

* The formula $\text{initialCondition}_i(\text{SV}, \text{POV}, L)$ specifies initial conditions, e.g. initial lanes and vehicle order (see Fig. 1). In some traffic disturbance scenarios (such as in Scenarios 1, 5, or 6), no such initial conditions are necessary, in which case we set $\text{initialCondition}_i(\text{SV}, \text{POV}, L) = \top$. By the semantics of $\top$ (see Table 2), this subformula is thus trivially true.

* The formula $\text{behaviourSV}_i(\text{SV}, L)$ corresponds to the SV behaviour component in §2.1, i.e. keeping the current lane L, or changing from lane L into a different lane.

* The formula $\text{behaviourPOV}_i(\text{POV}, SV, L)$ corresponds to the POV behaviour component in §2.1, namely cut-in, cut-out, acceleration, and deceleration. Note that SV behaviour is also relevant here; the formula thus has as arguments SV and the lane L relative to which the behaviour of SV is described. Notably, POV behaviour formulas always contain a subformula of the form

$$ \varphi_1(\text{SV}, \text{POV}) \mathcal{U} (\varphi_2(\text{SV}, \text{POV}) \land \text{danger}(\text{SV}, \text{POV})) $$

$$ \text{or } \mathcal{F}(\varphi_2(\text{SV}, \text{POV}) \land \text{danger}(\text{SV}, \text{POV})), $$

expressing that POV behaviour is dangerous relative to SV.

The overall structure of the formula $\text{disturb}_i$ (2) is as follows. It requires that a general notion of danger is true at a certain stage (recall that $\varphi_1 \mathcal{U} \varphi_2$ requires $\varphi_2$ becoming true at some time); the formulas $\text{behaviourSV}_i$ and $\text{behaviourPOV}_i$ specify the behaviours of the vehicles in the period leading to that dangerous moment. Some additional initial conditions are expressed in $\text{initialCondition}_i$.

There is, however, an initial condition that is common to all critical scenarios, namely that danger must happen after no danger has been observed for some time. This is entirely and exclusively described by initSafe in (1).

The STL formulas $\text{disturb}_i$ for the traffic disturbance scenarios in Table 1 are collected in Table 3. The subformulas occurring there (such as e.g. laneKeep and cutIn) are introduced in §4; after that we will review the formulas and see that they indeed correspond to the natural language descriptions in the ISO 34502 standard.

In the following section, we describe the formulas from which our formalisation of the traffic disturbance scenarios is composed.

# 4 DEFINITIONS OF FORMULAS

## 4.1 Vehicle Positions

We say that a vehicle $a$ is in a given lane $L$ if it occupies any lanelet of that lane, where $\text{occ}(a, l)$ is from §2.3.

$$ \text{atLane}(a, L) := \bigvee_{l \in L}(\text{occ}(a, l)). $$

A vehicle $a$ may occupy multiple lanes at once, for example during a lane change. To characterise the road sector a vehicle $a$ is in, we refer to the zone of the lanelets the vehicle occupies, where the disjunction is indexed over all lanelets $l$ with the corresponding
associated zone:

$$
\begin{align*}
\text{onMainRoad}(a) &:= \bigvee_{\text{zone}(l)=\text{mainZone}} \text{occ}(a, l), \\
\text{inMergeZone}(a) &:= \bigvee_{\text{zone}(l)=\text{mergeZone}} \text{occ}(a, l), \\
\text{inDepartZone}(a) &:= \bigvee_{\text{zone}(l)=\text{departZone}} \text{occ}(a, l).
\end{align*}
$$

We can now define the relevant road sector for a scenario by

$$
\begin{align*}
\text{mainRoad}(\text{SV}, \text{POV}) &:= \text{onMainRoad}(\text{SV}) \wedge \text{onMainRoad}(\text{POV}), \\
\text{mergeZone}(\text{SV}, \text{POV}) &:= \text{inMergeZone}(\text{SV}) \vee \text{inMergeZone}(\text{POV}), \\
\text{departZone}(\text{SV}, \text{POV}) &:= \text{inDepartZone}(\text{SV}) \vee \text{inDepartZone}(\text{POV}).
\end{align*}
$$

4.2 Relationship between Vehicles

We express a difference in (longitudinal) position or velocity of two
vehicles *a* and *b* by

$$
\begin{align*}
aheadOf(a, b) &:= front(a) \le rear(b), \tag{3} \\
fasterThan(a, b) &:= v_a < v_b,
\end{align*}
$$

using the vehicle parameters *front*, *rear*, and *v* defined in §2.3. Using *atLane* from §4.1 and *adjLanes*(*L*) from [25, Appendix A], we further define formulas expressing that vehicles *a*, *b*, *c* are in the same lane or in adjacent lanes as

$$
\begin{align*}
\text{sameLane}(a, b, L) &:= \text{atLane}(a, L) \wedge \text{atLane}(b, L), \\
\text{inAdjLanes}(a, b, L) &:= \text{atLane}(a, L) \wedge \bigvee_{L' \in \text{adjLanes}(L)} \text{atLane}(b, L'), \\
\text{sameLane}_3(a, b, c, L) &:= \text{sameLane}(a, b, L) \wedge \text{sameLane}(b, c, L).
\end{align*}
$$

4.3 Danger

In Table 3, the formula *danger*(*SV*, *POV*) is a general formula that states that *POV* poses a danger to *SV*. It is among our key findings that this formula *danger*(*SV*, *POV*) can be the same in all critical scenarios—scenario-specific features can be expressed in other components of a formula. At the same time, we found that a good definition of *danger* is critical to the quality of our formalisation: initially we had a looser condition as *danger*, which matched many traces in which *POVs* are hardly relevant to *SV* (see also [25, Appendix B]).

Our definition of *danger*, described below, is based on the notion of *RSS distance* [28]. It is defined as the smallest distance such that, if the lead vehicle brakes at its maximal braking rate, the rear vehicle can avoid a crash by braking at a pre-defined comfortable braking rate. According to [28] (see also [9]), the RSS distance is defined by

$$
dRSS_{lon}(v_r, v_f) := \max \left( 0, v_r \rho + \frac{a_{max} \rho^2}{2} + \frac{(v_r + a_{max} \rho)^2}{2b_{min}} - \frac{v_f^2}{2b_{max}} \right). \quad (4)
$$

Here, $v_r, v_f$ are the velocities of the rear and front vehicle respectively, $\rho$ is the reaction time after which the rear vehicle starts braking, $a_{max}$ is the maximum acceleration of the rear vehicle, $b_{min}$ is the maximum comfortable braking rate of the rear vehicle, and $b_{max}$ is the maximum possible braking rate of the front vehicle.

For multi-lane scenarios, we additionally need a notion of lateral
danger. This lateral RSS distance, following [28], is given by

$$
\begin{align}
dRSS_{\text{lat}}(v_1, v_2) &:= \nonumber \\
&\quad \max\left(0, (v_1 - v_2)\rho + a_{\text{max}}^{\text{lat}}\rho^2 + \frac{(v_1 + \rho a_{\text{max}}^{\text{lat}})^2 + (v_2 - \rho a_{\text{max}}^{\text{lat}})^2}{2b_{\text{min}}^{\text{lat}}}\right), \tag{5}
\end{align}
$$

where Vehicle 1 is assumed to be to the left of Vehicle 2, $v_1, v_2$ denote their lateral velocities, $a_{\text{max}}^{\text{lat}}$ the maximum lateral acceleration rate the vehicles can apply, and $b_{\text{min}}^{\text{lat}}$ their maximum comfortable lateral braking rate. (For simplicity, we ignore the stability factor in [28].)

Using the above functions for RSS distances, we go on to define
our formulas for danger. Following the RSS framework, we define
a dangerous situation as a violation of the RSS distance between
two vehicles. Our main formula *danger* is hence defined by

$$
\text{danger}(\text{SV}, \text{POV}) := \mathcal{G}_{[0, \min\text{Danger}]} \text{rssViolation}(\text{SV}, \text{POV}); \quad (6)
$$

it requires the formula `rssViolation(SV, POV)` to last at least for the time `minDanger`. The time duration `minDanger` is a parameter that should be suitably chosen; the effect of its choice is investigated in our experiments in §5. Note that `minDanger = 0` does not imply that there is no danger present; by the semantics of `G[0,0]` (see §2.2), it means that `danger(SV, POV)` is true at time `T` if `rssViolation(SV, POV)` is true at time `T`; i.e. if one chooses `minDanger = 0`, then `danger(SV, POV) = rssViolation(SV, POV)`.

By construction, *danger* stands for durable danger; the notion
of instantaneous danger, used in its definition (6), is defined as a
violation of both the lateral and longitudinal RSS distance by

$$
\text{rssViolation}(a, b) := \text{rssViolation}_{\text{lon}}(a, b) \wedge \text{rssViolation}_{\text{lat}}(a, b). \quad (7)
$$

The component formulas therein are defined as follows, using RSS
distances from (4–5).

$$
\text{rssViolation}_{\text{lon}}(a, b) := \text{dangerAhead}(a, b) \vee \text{dangerAhead}(b, a), \quad (8)
$$

$$
\begin{align}
\text{dangerAhead}(a, b) &:= \nonumber \\
&\quad s_b - s_a \ge 0 \wedge s_b - s_a \le \text{length}(b) + d\text{RSS}_{\text{lon}}(v_{\text{lon},a}, v_{\text{lon},b}); \tag{9}
\end{align}
$$

$$
\text{rssViolation}_{\text{lat}}(a, b) := \text{dangerLeft}(a, b) \vee \text{dangerLeft}(b, a), \quad (10)
$$

$$
\begin{equation}
\begin{split}
\text{dangerLeft}(a, b) &:= \\
&\quad d_b - d_a \ge 0 \wedge d_b - d_a \le \text{width}(b) + d\text{RSS}_{\text{lat}}(v_{\text{lat},b}, v_{\text{lat},a}).
\end{split}
\tag{11}
\end{equation}
$$

The formulas *length* and *width* are from §2.3.

Similarly, we introduce a durable notion of safety, i.e. safety for
the duration of *minSafe*. It is called *initSafe* because we use it for
the “safe in the beginning” requirement in our template (1).

$$
\text{initSafe}(\text{SV}, \text{POV}) := \mathcal{G}_{[0, \min\text{Safe}]} \text{instSafe}(\text{SV}, \text{POV}), \quad (12)
$$

$$
\text{instSafe}(a, b) := \neg \text{rssViolation}(a, b). \quad (13)
$$

When we use robust semantics of STL for quantitative notions
of truth [7], we find some modification of the formula `rssViolation`
more useful. See [25, Appendix C].

4.4 SV Behaviour

For readability we set

$$
\text{laneKeep}(a, L) := \text{atLane}(a, L),
$$

where *a* denotes a vehicle, *L* a lane, and *atLane* is from §4.1. This formula *laneKeep* is used as part of *behaviour* SV<sub>*i*</sub> in Table 3.

To formalise scenarios in which *SV* is changing its lane, it is suffi-
cient to specify only the initial or target lane, and that it eventually
changes its lane. For a vehicle *a* and a lane *L* we thus define

$$
\text{leavingLane}(a, L) := \text{atLane}(a, L) \wedge \mathcal{F}(\neg \text{atLane}(a, L)),
$$

$$
\text{enteringLane}(a, L) := \neg \text{atLane}(a, L) \wedge \mathcal{F}(\text{atLane}(a, L)).
$$

4.5 POV Behaviour

To distinguish POV’s dangerous cut-in or cut-out maneuvers from
regular lane changes (see §4.4), the formulas for the former contain
a term F danger to stress that these behaviours lead to danger. Fur-
thermore, these formulas need the lane currently occupied by the
SV as input. Lastly, we require that POVs complete their lane change when (or shortly after) danger occurs, in order to tie the danger to the change of lanes. This is represented by the $\mathcal{F}_{[0,minDanger]}(\dots)$ part of the following formulas. Overall, we obtain

$$ 
\begin{align*}
\text{cutIn}(\text{POV}, \text{SV}, \text{L}) &:= \\
&\quad \neg \text{sameLane}(\text{POV}, \text{SV}, \text{L}) \wedge \mathcal{F}(\text{danger}(\text{SV}, \text{POV}) \\
&\quad \wedge \mathcal{F}_{[0,minDanger]}(\text{sameLane}(\text{SV}, \text{POV}, \text{L}) \wedge \text{aheadOf}(\text{SV}, \text{POV}))), \\
\text{cutOut}(\text{POV}, \text{SV}, \text{L}) &:= \\
&\quad \text{sameLane}(\text{POV}, \text{SV}, \text{L}) \\
&\quad \wedge \mathcal{F}(\text{danger}(\text{POV}, \text{SV}) \wedge \mathcal{F}_{[0,minDanger]}[\neg \text{atLane}(\text{POV}, \text{L})]).
\end{align*}
$$

Here, atLane is from §4.1 and sameLane and aheadOf are from §4.2. Note that by the semantics of $\mathcal{F}$ in Table 2, a formula of the form $\mathcal{F}(\varphi_1 \wedge \mathcal{F}_{[0,t]}\varphi_2)$ is true at time $T$ if 1) there exists a time $T' \ge T$ such that $\varphi_1$ is true at time $T'$ and 2) $\varphi_2$ is true at some time during the interval $[T', T' + t]$.

In ISO 34502 [12], it is stated that “acceleration or deceleration categories actually imply relative velocity differences with respect to the subject vehicle.” We therefore define our formulas accel and decel using the fasterThan formula from §4.2. We further add laneKeep from §4.4 to distinguish this POV behaviour from the dangerous cut-ins and cut-outs defined previously.

$$ \text{accel}(\text{POV}, \text{SV}, \text{L}) := \text{fasterThan}(\text{SV}, \text{POV}) \wedge \text{laneKeep}(\text{POV}, \text{L}), $$

$$ \text{decel}(\text{POV}, \text{SV}, \text{L}) := \text{fasterThan}(\text{POV}, \text{SV}) \wedge \text{laneKeep}(\text{POV}, \text{L}). $$

## 4.6 Our Formalisation ISO34502-STL

Our set of formulas ISO34502-STL := $\{\text{scenario}_i | i = 1, \dots, 24\}$, describing the traffic disturbance scenarios of Table 1, is composed of the subformulas defined in §4.1–4.5. Their construction proceeds in the following steps.

The top-level formula is scenario$_i$; its format is given in (1) (see also the top line of Table 3). Its first component initSafe is common and is defined in (12). For its second component roadSector$_i$, we set

$$ \text{roadSector}_i(\text{SV}, \text{POV}) := \begin{cases} \text{mainRoad}(\text{SV}, \text{POV}), & i = 1, \dots, 8, \\ \text{mergeZone}(\text{SV}, \text{POV}), & i = 9, \dots, 16, \\ \text{departZone}(\text{SV}, \text{POV}), & i = 17, \dots, 24, \end{cases} $$

with the zone subformulas defined in §4.1.

The third component disturb$_i$ is the scenario-specific main part. Its template is given in (2) (see also the second line of Table 3). Its components initialCondition$_i$, behaviourSV$_i$, and behaviourPOV$_i$ are shown in Table 3. Note that the disturbance descriptions are independent of road geometry, thus it suffices to define them for the scenarios $i = 1, 2, \dots, 8$.

Our component subformulas initialCondition$_i$, behaviourSV$_i$, and behaviourPOV$_i$ for each scenario are mostly straightforward conjunctions, following their description in ISO 34502 (see Table 1 and Fig. 1). Nevertheless, the following points are worth noting.

* In Scenario 2, a three-vehicle cut-out is performed, see §2.1. Note that this maneuver cannot simply be composed of laneKeep(SV, L) and cutOut(POV₁, SV, L), since the cutOut subformula implies danger between SV and the POV performing the cut-out maneuver (see §4.5), whereas danger in this scenario occurs between SV and POV₂.

* In nearly all scenarios, the input lane L refers to the lane SV occupies at the beginning of the scenario. The only exception

is Scenario 7, where we use the lane that SV enters as the input lane. This is due to the fact that in Scenario 7, the SV behaviour is described by the formula enteringLane rather than leavingLane, see §4.4.

## 4.7 Extended Formalisation ISO34502-STL-ext(A)

In our experiments (§5), we found that natural interpretation of some of the ISO 34502 descriptions potentially overly restrictive. Specifically they concern 1) acceleration/deceleration and 2) relative vehicle positions. Our formalisation ISO34502-STL follows such natural (potentially overly restrictive) interpretation; in this section, we suggest its relaxation. We call it ISO34502-STL-ext. For experimental comparison of our two formalisations, see §5.3.

The first point of relaxation is about the definition of accel and decel. We chose to include vehicle acceleration (resp. deceleration) as an alternative to relative velocity differences and define

$$ \text{accel}_{\text{ext}}(\text{POV}, \text{SV}, \text{L}) := (\text{fasterThan}(\text{SV}, \text{POV}) \vee \text{accelerates}(\text{POV}) \wedge \text{laneKeep}(\text{POV}, \text{L})), $$

$$ \text{decel}_{\text{ext}}(\text{POV}, \text{SV}, \text{L}) := (\text{fasterThan}(\text{POV}, \text{SV}) \vee \text{decelerates}(\text{POV}) \wedge \text{laneKeep}(\text{POV}, \text{L})), $$

$$ \text{accelerates}(\text{POV}) := a_{\text{POV}} > 0, $$

$$ \text{decelerates}(\text{POV}) := a_{\text{POV}} < 0. $$

In ISO34502-STL-extA, we replace accel and decel by accel$_{ext}$ and decel$_{ext}$. This affects scenario$_i$, $i = 3, 4, 7, 8$; all other formulas remain unchanged.

The second point of relaxation is the formula aheadOf (cf. §4.2), in order to (partially) include positions 4 and 7 in Fig. 1. We define

$$ \text{aheadOf}_{\text{ext}}(a, b) := \text{front}(a) < \text{front}(b). $$

In ISO34502-STL-ext, we further extend ISO34502-STL-extA by removing aheadOf from the definition of cutIn (cf. §4.5) completely (thus redefining dangerous cut-ins to include POV entering SV's lane behind SV dangerously), and replacing aheadOf by aheadOf$_{ext}$ in all other formulas.

# 5 EXPERIMENTAL EVALUATION

In this section, we seek to quantitatively evaluate our formalisation. In related work on the formalisation of traffic rules in temporal logic, experiments focussed on the percentage of vehicles in a given dataset obeying the formalised traffic rules, see e.g. [17, 18]. Similarly, we will evaluate our formulas on a set of recorded vehicle traces to gain insight into how often our formulas are true.

We aim to address the following research questions:

* RQ1 Are ISO 34502's original descriptions of traffic disturbance scenarios adequate for detecting traffic disturbances?

* RQ2 Are ISO 34502's original descriptions of traffic disturbance scenarios adequate for classifying traffic disturbances?

* RQ3 How does our formalisation perform in terms of precision and recall?

* RQ4 How does the choice of the duration minDanger in (6) affect the recall of our formalisation?

* RQ5 How does our formalisation compare to existing works, in terms of detection of common disturbance scenarios?

To answer RQ3, we use two sets of ground truths. We will define them later in §5.3.
## 5.1 Experiment Setup

We evaluate our formulas for traffic disturbance scenarios on the highD dataset [15], which consists of drone-recorded vehicle traces on main road sections of German highways. The vehicle parameter values needed to define the RSS distance in §4.3 are chosen similarly to [11, 18] as $ρ = 0.6$, $a_{max} = 5$, $b_{min} = 6$, $b_{max} = 8$, $a_{max, lat} = 1.5$, $b_{min, lat} = 1.5$. We chose $b_{min}$ such that our RSS distance roughly corresponds to the "halber Tacho" rule-of-thumb used in Germany, stating that on highways, a safe distance (in meters) to the preceding vehicle is given by half the current velocity (in kilometers per hour); e.g. at a velocity of 100km h⁻<fnref n="1" />, we consider 50m a safe distance.

In our evaluation, we first filter the data traces and focus only on those in which there arises a danger in its middle. Specifically, we first collect all pairs of cars<fnref n="1" /> that violate the RSS distance between them eventually. Next, we evaluate the semantics of the formula

$$ \begin{gathered} \mathit{dangerArises}(SV, POV) := \\ \mathcal{F}(\mathit{initSafe}(SV, POV) \land \mathcal{F}(\mathit{danger}(SV, POV))). \end{gathered} \tag{14} $$

over all vehicle pairs (SV, POV) found in the previous step. Those traces which do not satisfy $\mathit{dangerArises}(SV, POV)$ are discarded. Since the implication $\mathit{scenario}_i \Rightarrow \mathit{dangerArises}$ is logically valid, the truth of $\mathit{dangerArises}$ is a necessary condition for any of the formulas in $ISO34502-STL(-ext)$ (see §4.6–4.7); therefore we are not discarding any traces that are relevant to our formalisation. We then shorten the remaining traces so that they only contain information relevant to our formulas: we discard the part before $\mathit{initSafe}$ is true and the part after the last danger interval ends. Finally, we discard all data about vehicles other than SV and POV.

The result of this filtering of the highD dataset is the set of traces where danger arises, i.e. those relevant to the ISO 34502 traffic disturbance scenarios. This trace set is referred to as $\mathit{disturbTraces}$.

The evaluation of our formalisations $ISO34502-STL(-ext)$ was conducted by computing the semantics of the formulas $\mathit{scenario}_i$, for $i = 1, 3, 4, \dots, 8$, over each trace $\sigma \in \mathit{disturbTraces}$. Here,

* we exclude $\mathit{scenario}_2$ since our implementation is limited to two-car scenarios ($\mathit{scenario}_2$ involves three cars and dealing with it is future work); and

* we exclude $\mathit{scenario}_9, \dots, \mathit{scenario}_{24}$ since the highD dataset only has main road traces.

## 5.2 Results

In our filtering of the highD dataset as discussed above, we first identified 99656 pairs (SV, POV) between which danger according to formula (6) occurs at some point. Here we used $minDanger = 0$ for the formula danger in (6) to be the most inclusive. From these pairs (SV, POV), we created two variations of the set $\mathit{disturbTraces}$, by applying the formula $\mathit{dangerArises}$ in (14) with the following parameter values.

* $\mathit{disturbTraces}_1$: using $minSafe = 0.6$ and $minDanger = 0$, and

* $\mathit{disturbTraces}_2$: using $minSafe = 0.6$ and $minDanger = 0.6$.

On these trace sets $\mathit{disturbTraces}_1$, $\mathit{disturbTraces}_2$, we evaluate our sets of formulas $ISO34502-STL$ and $ISO34502-STL-ext(A)$ (see §4.6 and §4.7). In this evaluation, the value of the parameter $minDanger$

in the formulas $\mathit{scenario}_i$ is chosen to match the considered set of traces, that is, $minDanger = 0$ for traces in $\mathit{disturbTraces}_1$ and $minDanger = 0.6$ for traces in $\mathit{disturbTraces}_2$. For the lane L in the formulas $\mathit{scenario}_i$ (1), we use the initial lane of POV for $\mathit{scenario}_7$, and the initial lane of SV for $\mathit{scenario}_i$, $i = 1, 3, 4, 5, 6, 8$.

The results of evaluating the STL formulas $\mathit{scenario}_i$ on the traces in $\mathit{disturbTraces}_j$, $j = 1, 2$ are collected in Table 4. Using our prototype implementation, the evaluation of all formulas $\mathit{scenario}_i$, $i = 1, 3, \dots, 8$, over all traces in $\mathit{disturbTraces}_1$ took around 2 hours on a laptop (Windows 10, Intel Core i7 @ 2.60GHz, 16GB RAM).

## 5.3 Discussions

In this section, we address our previously stated research questions.

**RQ1:** Are ISO 34502's original descriptions of the traffic disturbance scenarios adequate for detecting critical scenarios? While the original descriptions are not adequate, our extension (see §4.7) is indeed suitable for the purpose of detecting critical scenarios. By comparing the performance of our formalisations ISO34502-STL and ISO34502-STL-ext in Table 4, it is evident that a significant number of traces are not detected with the strict interpretation of acceleration and deceleration following ISO 34502, suggesting that their definitions should be clarified. With our extension ISO34502-STL-ext, we detect over 96% of all traces in $\mathit{disturbTraces}$. This conclusion holds regardless of $minDanger$, see RQ4.

**RQ2:** Are ISO 34502's original descriptions of the traffic disturbance scenarios adequate for classifying critical scenarios? The descriptions are not adequate for classification purposes. This is to be expected; the ISO 34502 scenario set in Table 1 is not designed for the purpose of classification but rather for a comprehensive coverage of all traffic disturbances. As an example, consider SV keeping its lane, while POV performs a dangerous cut-in maneuver while driving at a slightly slower speed than SV throughout the maneuver. This clearly matches Scenario 1 in Table 1; however it may also match Scenario 4 if danger arises shortly after POV has entered SV's lane. Refining the scenario descriptions (and accordingly their formalisation) for the purpose of classification is future work.

**RQ3:** How does our formalisation perform in terms of precision and recall? We recall the definitions of precision and recall from [24], namely $precision = \#truePositives/(\#truePositives + \#falsePositives)$, and $recall = \#truePositives/(\#truePositives + \#falseNegatives)$. For our experiments, a true positive denotes a disturbance trace for which one of our formulas is true, a false positive is a disturbance-free trace for which one of our formulas is true, and a false negative denotes a disturbance trace for which none of our formulas are true. Precision and recall for individual scenario-formulas are outside the scope of our experiments, as this would require the dataset to contain labels denoting the type of traffic disturbance scenario.

We have a precision of 100%—false positives cannot occur in our formalisation, as our definition of a disturbance trace as a trace for which the formula $\mathit{dangerArises}$ (see §5.1) is eventually true has been exactly implemented into all our formulas.

The recall of ISO34502-STL, and particularly of ISO34502-STL-ext, relative to the sets $\mathit{disturbTraces}_i$, $i = 1, 2$ is very high, see Table 4. This notion of recall is exactly what we discussed in RQ1.

We note that the use of $\mathit{initSafe}$ (see §4.3) is important. Indeed, if we omit the filtering using $\mathit{dangerArises}$ (14) and merely filter

<footnote n="1">¹In the highD dataset, a vehicle is either a car or a truck. In our experiments, we focus on cars, for the reason that different physical characteristics of trucks should lead to different scenario descriptions. Elaboration of it is future work.</footnote>
<table><caption>**Table 4:** Quantitative results of our experiments. *Data trace set* *T* refers to the set of traces on which our formulas are evaluated. See §5.1: *disturbTraces*<sub>1</sub>, *disturbTraces*<sub>2</sub> are the sets with *minDanger* = 0, 0.6, respectively. The number of traces in *T* is denoted by |*T*|. In the *spec set* column, the evaluated set of formulas is noted (see §4.6 and §4.7). *Matching traces* denotes the total number of traces in *T* for which at least one of the considered formulas *scenario*<sub>*i*</sub>, *i* = 1, 3, ..., 8 is true. The recall column (see §5.3) refers to recall relative to |*T*| as ground truth. In each column labelled *s*<sub>*i*</sub>, *i* = 1, 3, ..., 8, we state for how many traces in *T* the corresponding formula *scenario*<sub>*i*</sub> is true.</caption><thead><tr><th>data trace set T</th><th>min-<br>Danger</th><th>no. of<br>traces |T|</th><th>spec set</th><th>matching<br>traces</th><th>recall</th><th>scenario<sub>1</sub><br>(s<sub>1</sub>)</th><th>s<sub>3</sub></th><th>s<sub>4</sub></th><th>s<sub>5</sub></th><th>s<sub>6</sub></th><th>s<sub>7</sub></th><th>s<sub>8</sub></th></tr></thead><tbody><tr><td>disturbTraces<sub>1</sub></td><td>0</td><td>32398</td><td>ISO34502-STL</td><td>24038</td><td>74.2%</td><td>4091</td><td>21941</td><td>21941</td><td>291</td><td>218</td><td>3188</td><td>924</td></tr><tr><td>disturbTraces<sub>1</sub></td><td>0</td><td>32398</td><td>ISO34502-STL-extA</td><td>30288</td><td>93.5%</td><td>4091</td><td>27652</td><td>26008</td><td>291</td><td>218</td><td>4362</td><td>969</td></tr><tr><td>disturbTraces<sub>1</sub></td><td>0</td><td>32398</td><td>ISO34502-STL-ext</td><td>31139</td><td>96.1%</td><td>9364</td><td>27652</td><td>26008</td><td>378</td><td>218</td><td>4362</td><td>969</td></tr><tr><td>disturbTraces<sub>2</sub></td><td>0.6</td><td>28881</td><td>ISO34502-STL</td><td>21564</td><td>74.7%</td><td>4076</td><td>19595</td><td>19595</td><td>283</td><td>215</td><td>3171</td><td>801</td></tr><tr><td>disturbTraces<sub>2</sub></td><td>0.6</td><td>28881</td><td>ISO34502-STL-extA</td><td>27177</td><td>94.1%</td><td>4076</td><td>24843</td><td>23328</td><td>283</td><td>215</td><td>4347</td><td>838</td></tr><tr><td>disturbTraces<sub>2</sub></td><td>0.6</td><td>28881</td><td>ISO34502-STL-ext</td><td>27963</td><td>96.8%</td><td>9312</td><td>24843</td><td>23328</td><td>361</td><td>215</td><td>4347</td><td>838</td></tr></tbody></table>

<table><caption>**Table 5:** Absolute number of the cut-in and deceleration scenarios detected in the highD dataset by [26, 34] and our formalisation (see §4.6–4.7). Definitions and danger metrics of [26] and [34] are discussed in the discussion of RQ5 in §5.3. Our danger metric RSS distance is defined in §4.3. The values in the ISO34502-STL(-ext) columns are from Table 4. For details see the discussion of RQ5 in §5.3.</caption><thead><tr><th></th><th>[26]</th><th>[26]</th><th>[34]</th><th>ISO34502-STL-ext</th></tr></thead><tbody><tr><td>danger metric</td><td>TTC</td><td>THW</td><td>none</td><td>RSS dist.</td></tr><tr><td>cut-in</td><td>144</td><td>7219</td><td>1017</td><td>9364</td></tr><tr><td>deceleration</td><td>22</td><td>112</td><td>26846</td><td>26008</td></tr></tbody></table>

using *danger* (6), our recall is quite low (around 25%) due to many false negatives. This is natural; due to the spatial limitation of the highD dataset, many traces do not fulfill *initSafe*, i.e. danger is either present from the beginning of the trace or the observed interval of safety leading up to danger is shorter than required by *initSafe*. This spatial limitation can be considered a perception disturbance (see §2.1), which is outside the scope of our formalisation.

**RQ4:** *How does the choice of minDanger in (6) affect recall of our formalisation?*

The choice of *minDanger* in (6) does not have a significant impact on recall, see Table 4. For this reason, we restrict our discussion of the other research questions to *minDanger* = 0.

One implication of the above is that our formalisation—based on the RSS-based notion of danger—is *stable*, with respect to a parameter value which is not easy to choose (namely *minDanger*).

**RQ5:** *How does our formalisation compare to existing works, in terms of detection of common disturbance scenarios?*

Here we compare the content of our formalisation with some existing works. We focus on the cut-in and deceleration scenarios, as these two scenarios have been studied many times before. Our comparison is with [26] (with two danger metrics TTC and THW) and [34], as these works evaluate their formalisation on the highD dataset. The comparison is in Table 5; here are some details.

In [26], a cut-in is defined as a lane change in which *POV* enters the lane of *SV* in front of *SV*. The notion of deceleration is defined

in [26] as hard braking (above a parameter value they choose) by the *POV* ahead of *SV* in the same lane. As danger metrics, *time to collision* (TTC < 4s) and *time headway* (THW < 2s) are used.

In [34], a cut-in is defined as in [26], with the additional restrictions that 1) the lateral velocity of *POV* must remain nonzero throughout the maneuver, and 2) a maximum longitudinal distance between *SV* and *POV* is introduced. A deceleration scenario is defined as “reduction of the headway distance between vehicles [...] caused by the deceleration of a preceding vehicle and not by the acceleration of the subject vehicle”, where *POV* is required to brake continuously throughout the scenario and to remain in its lane. In [34], matching traces are first detected without any danger metric; later the danger metrics TTC and THW are calculated for the detected traces. We restrict our discussion to the number of traces that were detected without any danger metric, as their danger metric analysis lacks absolute numbers.

For our formalisation, we use ISO34502-STL-ext (§4.7), based on our discussion in RQ1. We identified cut-in as Scenario 1 and deceleration as Scenario 4: although Scenarios 5 and 8 also contain cut-in and deceleration components, respectively, Scenarios 1 and 4 correspond more closely to the definitions used in [26, 34]. The numbers for ISO34502-STL-ext in Table 5 are hence the numbers for Scenario 1 (cut-in) and Scenario 4 (deceleration) from the third row of Table 4, i.e. for *minDanger* = 0 and ISO34502-STL-ext.

In Table 5, the numbers for different formalisations for both the cut-in and deceleration scenarios are quite different. For each scenario, the number for our formalisation is (close to) the greatest, and we may wonder if the number is too large. We argue that this is not the case:

* the trace set *disturbTraces*<sub>1</sub> is a naturally defined one by the formula *dangerArises* in (14);

* the whole set ISO34502-STL-ext of formulas, achieving 96.1% recall for *disturbTraces*<sub>1</sub> (see RQ3), is therefore a natural one (note that precision is 100% by definition); and

* the formulas *scenario*<sub>1</sub> and *scenario*<sub>4</sub>, defined by imposing natural constraints (Table 3), are natural ones, too.

We note that a similar number of cut-ins as in our experiments is detected in [26] (7219). This is natural, since their danger metric THW < 2s is very similar to the “halber Tacho” rule we used to
calibrate our parameter values for the RSS distance (see §5.1) and their definition of a cut-in is similar to ISO 34502. On the other hand, [34] detects significantly less cut-ins (1017) even without a danger metric; this may be due to the restriction on the longitudinal distance between the two vehicles.

For deceleration scenarios, [34] detects a very similar number (26846) as our formalisations. Note that in [34], no danger metric is used, implying that deceleration on highways leads to a violation of the RSS distance (see §4.3) in nearly all cases. On the other hand, the formalisation in [26] is much stricter and hence matches significantly fewer traces (< 150).

Another point in the comparison is that *parameter-tuning is easy* in our formalisation. Our parameter-tuning is largely reduced to that for RSS in general:

* besides the RSS parameters (e.g. response time $\rho$ and maximum acceleration/braking rates, see §4.3), our formalisation only has *minDanger* and *minSafe* as parameters, and

* as seen in RQ4, the value of *minDanger* is hardly relevant.

Tuning the RSS parameters is a more general problem—those parameters are important beyond specific disturbance scenarios—and methods of doing so are an active field of research [13]. Such ease of parameter tuning is not the case, e.g. in [26], where “hard braking” in a deceleration scenario must be manually defined.

# 6 CONCLUSIONS AND FUTURE WORK

In this paper, we presented a temporal logic formalisation of traffic disturbance scenarios concerning general vehicles on highways as specified in ISO Standard 34502. Based on this important class of scenarios, further critical scenarios can be formalised through a modular approach. Our formalisation relies on the RSS framework, allowing for easy parameter-tuning. Experimentally, we were able to show that a small extension of the ISO standard allows for a very high rate of disturbance trace detection.

Future work includes the formalisation of further critical scenarios in ISO 34502 and beyond, such as scenarios involving motorcycles, vehicle control disturbances, and intersection scenarios.

Our current formalisation needs an initial lane as input, since STL does not support variable binding and hence does not allow us to refer to the lane initially occupies otherwise. As future work, an implementation of our formulas to an extension of STL with temporal freezing (e.g. *STL*\*, see [4]) should be considered.

# REFERENCES

[1] Y. Annpureddy, C. Liu, G. Fainekos, and S. Sankaranarayanan. 2011. S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems. In *TACAS 2011*, Vol. 6605. Springer, 254–257.

[2] C. Baier and J.-P. Katoen. 2008. *Principles of Model Checking*. The MIT Press.

[3] P. Bender, J. Ziegler, and C. Stiller. 2014. Lanelets: Efficient map representation for autonomous driving. In *IV 2014*. 420–425.

[4] L. Brim, P. Dluhoš, D. Šafránek, and T. Vejjustek. 2014. STL*: Extending signal temporal logic with signal-value freezing operator. *Information and Computation* 236 (2014), 52–67. Special Issue on Hybrid Systems and Biology.

[5] A. Donzé. 2010. Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. In *CAV 2010*, Vol. 6174. Springer, 167–170.

[6] K. Esterle, L. Gressenbuch, and A. Knoll. 2020. Formalizing Traffic Rules for Machine Interpretability. In *CAVS 2020*. IEEE, 1–7.

[7] G. E. Fainekos and G. J. Pappas. 2009. Robustness of temporal logic specifications for continuous-time signals. *Theoretical Computer Science* 410, 42 (2009), 4262–4291.

[8] E. C. for Europe Inland Transport Committee. 2019. *Framework document on automated/autonomous vehicles*. Technical Report ECE/TRANS/WP.29/2019/34/Rev.2. World Forum for Harmonization of Vehicle Regulations.

[9] I. Hasuo. 2022. Responsibility-Sensitive Safety: An Introduction with an Eye to Logical Foundations and Formalization. *CoRR* abs/2206.03418 (2022). arXiv:2206.03418

[10] I. Hasuo, C. Eberhart, J. Haydon, J. Dubut, R. Bohrer, T. Kobayashi, S. Pruekprasert, X.-Y. Zhang, E. A. Pallas, A. Yamada, K. Suenaga, F. Ishikawa, K. Kamijo, Y. Shinya, and T. Suetomi. 2023. Goal-Aware RSS for Complex Scenarios via Program Logic. *IEEE Trans. Intell. Vehicles* 8, 4 (2023), 3040–3072.

[11] M. Hekmatnejad, S. Yaghoubi, A. Dokhanchi, H. B. Amor, A. Shrivastava, L. Karam, and G. Fainekos. 2019. Encoding and Monitoring Responsibility Sensitive Safety Rules for Automated Vehicles in Signal Temporal Logic. In *MEMOCODE 2019* (La Jolla, California). ACM, New York, NY, USA, Article 6, 11 pages.

[12] ISO 34502:2022(E) 2022. *Road vehicles — Test scenarios for automated driving systems — Scenario based safety evaluation framework*. Standard. International Organization for Standardization, Geneva, CH.

[13] H. Königshof, F. Oboril, K. Scholl, and C. Stiller. 2022. A Parameter Analysis on RSS in Overtaking Situations on German Highways. In *IV 2022*. IEEE, 1081–1086.

[14] R. Koymans. 1990. Specifying real-time properties with metric temporal logic. *Real-Time Systems* 2, 4 (Nov. 1990), 255–299.

[15] R. Krajewski, J. Bock, L. Kloeker, and L. Eckstein. 2018. The highD Dataset: A Drone Dataset of Naturalistic Vehicle Trajectories on German Highways for Validation of Highly Automated Driving Systems. In *ITC 2018*. 2118–2125.

[16] H. Krasowski and M. Althoff. 2021. Temporal Logic Formalization of Marine Traffic Rules. In *IV 2021*. IEEE, 186–192.

[17] S. Maierhofer, P. Moosbrugger, and M. Althoff. 2022. Formalization of Intersection Traffic Rules in Temporal Logic. In *IV 2022*. IEEE, 1135–1144.

[18] S. Maierhofer, A.-K. Rettinger, E. C. Mayer, and M. Althoff. 2020. Formalization of Interstate Traffic Rules in Temporal Logic. In *IV 2020*. IEEE, 752–759.

[19] O. Maler and D. Nickovic. 2004. Monitoring Temporal Properties of Continuous Signals. In *Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems*. Springer Berlin Heidelberg, Berlin, Heidelberg, 152–166.

[20] H. Muslim, S. Endo, H. Imanaga, S. Kitajima, N. Uchida, E. Kitahara, K. Ozawa, H. Sato, and H. Nakamura. 2023. Cut-Out Scenario Generation With Reasonability Foreseeable Parameter Range From Real Highway Dataset for Autonomous Vehicle Assessment. *IEEE Access* 11 (2023), 45349–45363.

[21] D. Nalić, T. Mihalj, M. Baeumler, M. Lehmann, A. Eichberger, and S. Bernsteiner. 2020. Scenario Based Testing of Automated Driving Systems: A Literature Survey.

[22] J.-P. Paardekooper, S. van Montfort, J. Manders, J. M. Goos, E. de Gelder, O. O. den Camp, O. Bracquemond, and G. Thiolon. 2019. Automatic Identification of Critical Scenarios in a Public Dataset of 6000 km of Public-Road Driving.

[23] A. Pnueli. 1977. The temporal logic of programs. In *SFCS 1977*. 46–57.

[24] D. Powers. 2008. Evaluation: From Precision, Recall and F-Factor to ROC, Informedness, Markedness & Correlation. *Mach. Learn. Technol.* 2 (01 2008).

[25] J. Reimann, N. Mansion, J. Haydon, B. Bray, A. Chattopadhyay, S. Sato, M. Waga, E. André, I. Hasuo, N. Ueda, and Y. Yokoyama. 2023. Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance. (2023). Extended version with appendices, available on arXiv.

[26] P. Schneider, M. Butz, C. Heinzemann, J. Oehlerking, and M. Woehrle. 2020. Scenario-based threat metric evaluation based on the highd dataset. In *IV 2020*. IEEE, 213–218.

[27] A. D. S. Sectional Committee of AD Safety Evaluation. 2022. *Automated Driving Safety Evaluation Framework Ver. 3.0 Guidelines for Safety Evaluation of Automated Driving Technology*.

[28] S. Shalev-Shwartz, S. Shammah, and A. Shashua. 2018. On a formal model of safe and scalable self-driving cars.

[29] Q. Song, K. Tan, P. Runeson, and S. Persson. 2023. Critical scenario identification for realistic testing of autonomous driving systems. *Software Quality Journal* 31, 2 (June 2023), 441–469.

[30] D. Ulus. 2018. *Pattern Matching with Time: Theory and Applications. (Filtrage par motif temporisé: Théorie et Applications)*. Ph. D. Dissertation. Grenoble Alpes University, France. https://tel.archives-ouvertes.fr/tel-01901576

[31] C. Wang and H. Winner. 2019. Overcoming Challenges of Validation Automated Driving and Identification of Critical Scenarios. In *ITSC 2019*. 2639–2644.

[32] Z. Zhang, G. Ernst, S. Sedwards, P. Arcaini, and I. Hasuo. 2018. Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search. *IEEE Trans. on CAD* 37, 11 (2018), 2894–2905.

[33] Z. Zhang, I. Hasuo, and P. Arcaini. 2019. Multi-armed Bandits for Boolean Connectives in Hybrid System Falsification. In *CAV 2019*, Vol. 11561. Springer, 401–420.

[34] A. Zlocki, A. König, J. Bock, H. Weber, H. Muslim, H. Nakamura, S. Watanabe, J. Antona-Makoshi, and S. Taniguchi. 2022. Logical Scenarios Parameterization for Automated Vehicle Safety Assessment: Comparison of Deceleration and Cut-In Scenarios From Japanese and German Highways. *IEEE Access* 10 (2022), 26817–26829.