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

TL;DR

The paper tackles safety assurance for autonomous driving by formalising ISO 34502 traffic disturbance scenarios within the Signal Temporal Logic (STL) framework. It introduces a modular templating approach (ISO34502-STL) that instantiates 24 disturbance scenarios using a common initSafe/distance-based structure, with RSS distance defining durable danger. The authors validate the approach on the highD dataset, showing high recall (up to about 96%) and 100% precision by leveraging RSS-based danger and an initial safe period, and demonstrate practical workflow with the STL Debugger. They further propose an extended STL formulation (ISO34502-STL-ext) that relaxes acceleration/position assumptions, achieving comparable or better detection performance. Overall, the work provides a scalable, parameter-tunable method for scenario-based testing and monitoring of AV controllers, with strong potential for integration into safety verification pipelines and standardised assessments.

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.

Figures (4)

• Figure 1: Left: Numbering of possible $\mathit{POV}$ locations relative to $\mathit{SV}$. The fields numbered as "+1" are only relevant in three-vehicle scenarios. Right: Combinations of $\mathit{POV}$ positions and behaviours that may cause critical scenarios. These are from ISO34502.
• Figure 2: A sample road section (departure zone) constructed from lanelets forming two main road lanes (grey, $\mathit{attr}(l)=\mathit{main}$) and one departure lane (blue, $\mathit{attr}(l)=\mathit{departure}$). All depicted lanelets satisfy $\mathit{zone}(l)=\mathit{ 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.
• 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 \ref{['subsect:vehicleConf']} for the definition of $\mathit{rear}(a)$.
• Figure 4: STL Debugger, a screenshot. STL formulas are written in the text pane (left). Functionalities such as semantics computation and exemplifications are realised in the GUI on the right, where different nodes are connected with wires (they can be dragged for rearrangement) and results can be plotted or even animated.

Theorems & Definitions (1)

• Remark