# Assessing Test Scenarios for Autonomous Driving Using Probabilistic Model Checking

Jean-Baptiste Horel, Philippe Ledent, Radu Mateescu, Wendelin Serwe, Aline Uwimbabazi

► To cite this version:

Jean-Baptiste Horel, Philippe Ledent, Radu Mateescu, Wendelin Serwe, Aline Uwimbabazi. Assessing Test Scenarios for Autonomous Driving Using Probabilistic Model Checking. ICTSS 2025 - 37th IFIP WG 6.1 International Conference on Testing Software and Systems, Sep 2025, Limassol, Cyprus. pp.273-289, 10.1007/978-3-032-05188-2_18. hal-05267555

HAL Id: hal-05267555

https://inria.hal.science/hal-05267555v1

Submitted on 18 Sep 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
Assessing Test Scenarios for Autonomous Driving
Using Probabilistic Model Checking

Jean-Baptiste Horel¹, Philippe Ledent¹,², Radu Mateescu¹,
Wendelin Serwe¹, and Aline Uwimbabazi¹

jean-baptiste.horel@inria.fr, philippe.ledent@aedvices.com,
radu.mateescu@inria.fr, wendelin.serwe@inria.fr,
aline.uwimbabazi@inria.fr

¹ Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP*, LIG, 38000 Grenoble, France

² Aedvices Consulting

**Abstract.** Testing autonomous vehicles is a challenging task, usually carried out using test scenarios, which are often derived manually from accident statistics and real traffic datasets, relying on expert knowledge and intuition to select the most relevant ones, a cumbersome task given the large size of these datasets. In this paper, we suggest a model-based approach to compare scenarios using quantitative measures computed by probabilistic model checking of user-defined temporal logic properties characterizing interesting event sequences. This approach facilitates the selection of the scenarios having the best tradeoff between coverage and overall testing cost (both for simulation and field testing). We illustrate the approach by comparing variations of scenarios, derived from frequent situations in accident statistics, using measures such as collision probability, arrival probability, and duration.

# 1 Introduction

Scenario-based testing is the state of the art method for validation and performance evaluation of Autonomous Vehicles (AVs) [22]. To limit testing cost and complexity, recent studies [9] were conducted on road crash reports to define an abstract taxonomy of scenarios and determine the most relevant ones, with the goal of reducing the number of test executions. However, studying crash reports and identifying abstract scenarios is still a tedious manual task, which moreover must include the design of concrete scenarios, ready to be executed. A more automated solution is the extraction of scenarios from datasets obtained by recording real traffic data. But most of this data is non critical: road crash statistics show that critical situations only occur every several millions of driven kilometers, and oftentimes these situations only last a few seconds.

To some extent, automatic processes can detect road crashes (TUM crash dataset<fnref n="3" />), but although collisions are relevant scenarios for AV validation, there

<footnote>* Institute of Engineering Univ. Grenoble Alpes</footnote>

<footnote n="3">³ https://tum-traffic-dataset.github.io/tumtraf-a/</footnote>
are other kinds of critical scenarios. For instance, a scenario in which a human
driver could successfully avoid a collision would be wrongfully ignored for lack
of severe consequences. The latest results from main AV companies like Tesla
and Waymo show the need for a reliable automatic scenario assessment, able to
analyse the huge volume of available recorded data. Tesla Full Self-Driving has
driven 1B miles from January to October 2024⁴ and Waymo taxis have driven
a total of 50M miles, autonomously carrying out 100,000 paid rides per week
until December 2024⁵. Because it is unfeasible to manual checking all these data
to determine critical scenarios, techniques to increase the criticality of scenarios
have been proposed [22].

In previous work, we showed how to use formal methods—precisely, the CADP<fnref n="6" /> toolbox [6]—to automatically generate sets of test cases completely covering critical scenarios [11]. Concretely, we formally modeled a scenario, comprising the road scenery, the behaviour of dynamic obstacles (other vehicles, pedestrians, etc.), and constraints on the behaviour of the AV (e.g., traversal of the scenery). Using this model and a test purpose (e.g., observation of a collision), we applied conformance testing techniques [18] to generate a set of tests covering the test purpose completely [19]. The generated tests were then translated into behaviour trees and subsequently executed in the CARLA simulator [5], which allowed us to evaluate the correctness of a perception component [12].

Extending this work, we suggest in this paper an approach to compare scenarios based on quantitative measures computed on the formal model of the AV in its environment. Precisely, we suggest to apply probabilistic model checking to compute the probabilities of user-defined event sequences (e.g., a successful arrival, a collision with an obstacle, etc.) expressed in temporal logic. Scenarios can then be compared based on the computed probabilities: for instance, for an event sequence characterising a collision, a scenario with a higher probability is more interesting, because the corresponding tests will put more stress on the collision-avoidance systems of the AV. We explored three instantiations of probabilistic model checking: exact [20], approximate [10], and intermediate (a combination thereof). Our approach is generic, enabling the capture of a variety of situations by adapting the formal model, and provides a quantitative way of comparing scenarios, assessing their criticality, and suggesting how to improve their relevance for testing AVs. The formal modelling and verification are supported by CADP. We evaluated our approach experimentally on 30 driving scenarios, generated based on a recent study on crash reports [14].

The rest of the paper is organised as follows. Section 2 compares our approach to related work. Section 3 presents the scenarios used for experimenting our methodology. Section 4 gives an overview of the formal model. Section 5 describes the considered event sequences, both in natural language and temporal logic. Section 6 compares the scenarios according to the probabilities of event sequences computed with our methodology. Finally, Section 7 concludes.

<footnote n="4">⁴ Q3 2024 Update, https://ir.tesla.com/#quarterly-disclosure</footnote>

<footnote n="5">⁵ https://waymo.com/safety/impact/</footnote>

<footnote n="6">⁶ http://cadp.inria.fr</footnote>
## 2 Related Work

Validation of AVs through scenario-based testing has been extensively studied, from the definition of scenarios to their generation and the surrounding framework comprising the operational design domain, the key performance indicators, and the test environments (a survey is available in [9]). These studies identified the need for databases of critical scenarios that can be used to reliably test AVs in various environments (simulation, controlled environment, public roads) [22], and also the lack of formal methods to rigorously assess scenarios, as we propose.

Large datasets of real traffic data are used for benchmarking and training of AVs perception or planning models. Nuplan [2], the latest major dataset released for AV research, is made of 1500 hours of human driving data recorded in four cities and organised in scenarios (e.g., the AV following a vehicle or crossing an intersection), categorised in terms of lane changes, interactions with pedestrians at crosswalks, and interactions with obstacles in close proximity. However, Nuplan provides no way of selecting and finding critical scenarios. To overcome this, [4] used the performance results of a rule-based planner model to identify the hardest scenarios in the dataset and to limit the model evaluation to these scenarios, sparing the execution of easier ones. Contrary to our method based on formal models of scenarios, the method in [4] relies only on the results of the planner and the specific evaluation metrics used: therefore, this method is biased in the sense that it cannot provide objective insight in the scenario criticality and thus can potentially miss some relevant scenarios the model happened to handle successfully.

The TUM accident dataset<fnref n="7" /> recorded the traffic at a highway intersection, tracked vehicle trajectories, and used them to detect accidents. Across several months of recording, it was possible to detect ten accidents by identifying the corresponding collisions, but without any further assessment on the remaining data. The approach we propose, based on a formal scenario model and quantitative verification, attempts to provide additional indicators about the relevance of a scenario and its criticality (presence or lack of collisions, scenarios not complete because of the AV being stuck, not enough vehicles around the AV, etc.).

To complement extracting scenarios from real data, one can synthesize new ones in simulation, which is also the approach we consider here. In CARLA Leaderboard [5], autonomous driving agents are tasked to follow a long route in a simulated city along which they encounter many distinct scenarios (e.g., pedestrian crossing, car leaving parking lot, blocked lanes). DeepAccident [23] proposed a similar methodology, also based on the CARLA simulator, but added an optimisation algorithm to increase collision risk with the AV. In both methods, scenarios are manually designed following the NHTSA<fnref n="8" /> (National Highway Traffic Safety Administration) typology. Although these methods successfully identified contributing factors and circumstances that increase crash risk

<footnote n="7">7 https://tum-traffic-dataset.github.io/tumtraf-a/</footnote>

<footnote n="8">8 https://www.nhtsa.gov/</footnote>
or severity, they mostly rely on merely the presence of collisions as criticality indicator for scenarios.

Criticality metrics evaluate the risk of a snapshot of a driving scene, estimating the collision risk of the AV using its current state or trajectories of the AV and other actors [24]. Another metric [13] predicts trajectories of other actors to estimate the risk of the optimal AV trajectory; this metric was tested on all scenes of a dataset of recorded highway trajectories. Given that these metrics do not evaluate scenarios but snapshots, they can be used to identify critical scenes that could be subsequently linked (manually) to critical scenarios. Our method quantifies the criticality of a scenario in a flexible manner, by parameterising the set of possible trajectories of the actors surrounding the AV.

## 3 Deriving Scenarios from Critical Situations

Recent traffic accident statistics studies [14] report a number of critical situations that may lead to a collision of an AV—hereafter called *ego vehicle*—with another vehicle or a pedestrian, therefore leading to (possibly fatal) hazards, injuries, or costly damages. To evaluate the behaviour of the ego vehicle, we selected five critical situations, which are representative of most accidents: collision with another vehicle (front, rear, or side collision) and collision with a pedestrian (either visible, or occluded by another vehicle). In all cases, the collision usually occurs if driving priority rules are ignored (by the ego vehicle or the moving obstacles) and/or the ego vehicle brakes too late.

We represent the situations (under ideal conditions) using a fixed, quadratic grid called *map* of an x-shaped intersection<fnref n="9" /> of two roads (with several lanes each), delimited by buildings (static, immobile obstacles) in the corners. The map consists of cells, which are updated at each move performed by the vehicles (the ego vehicle and other moving vehicles) and pedestrians (a visible one and another one, occluded by a parked vehicle). The ego vehicle is represented by a black cell marked by “C”. Moving vehicles are represented by coloured cells (blue, green, red, white, yellow) marked by “V”. Parked vehicles are represented by pink cells marked by “IV”. Buildings, also called *scenery*, are static obstacles represented by yellow cells marked by “I”. Pedestrians crossing the map are dynamic obstacles represented by magenta cells marked by “P”. The five critical situations selected are described below.

A typical *front collision* situation occurs when two vehicles (say, a blue and a red one) move in the opposite direction of the ego vehicle, and one of them (say, the red one) tries to overtake the other (blue) vehicle, using the lane of the ego vehicle, which might not be able to brake to avoid a collision. Figure 1 shows a CARLA simulation screenshot and its corresponding map representation.

A typical *rear collision* situation occurs when the ego vehicle follows a straight line and is hit from behind by another (say, white) vehicle starting from a parking slot without taking into account the traffic. Figure 2 shows a map leading to a rear collision.

<footnote n="9">⁹ Front and rear collisions could be studied without an intersection.</footnote>
<figure><img src="image_2.png" /><figcaption>(a) CARLA simulation screenshot</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>(b) Map representation</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Fig. 2: Rear collision situation</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 3: Side collision situation</figcaption></figure>

A typical *side collision* situation occurs when another (say, green) vehicle arriving from the left and crossing the trajectory of the ego vehicle does not yield the priority to the ego vehicle, as illustrated on Figure 3.

A typical *collision with a pedestrian* occurs when a pedestrian crosses the road in front of the ego vehicle, either from left to right or in the opposite direction. A particularly interesting case of collision is with a pedestrian occluded by a parked vehicle, due to the risk of the pedestrian being perceived too late by the ego vehicle. Figures 4 and 5 illustrate the maps representing a collision with a visible or occluded pedestrian, respectively.

From these five critical situations, we derived a set of obstacles (vehicles and pedestrians), each with a specific initial position and trajectory (including the case of a static obstacle, representing a parked vehicle). Placing a subset of these obstacles in the map, we obtain a variety of 30 scenarios, differing in the number of (dynamic, moving) obstacles and kinds of collisions, as shown in Table 1. The basic scenario S0.1 involves no obstacles except the static scenery (buildings). All the other scenarios involve various obstacles and are prone to collisions or near misses (i.e., an obstacle passing in the same or an adjacent cell to the ego vehicle). Notice that in real traffic, combinations of obstacles are likely to occur; but even in the absence of obstacles, the ego vehicle might collide with the scenery.

For modelling simplicity, we consider discrete time: In each time step, an obstacle has the choice of executing a move from its (predefined) trajectory or not. Whenever the move would lead to a collision, the obstacle remains still.
<table><caption>Table 1: Scenarios derived from the critical situations</caption><thead><tr><th rowspan="2">scenario</th><th colspan="2">collision</th><th colspan="2">unrestricted LTS</th><th colspan="2">restricted LTS</th></tr><tr><th>front</th><th>rear</th><th>states</th><th>transitions</th><th>states</th><th>transitions</th></tr></thead><tbody><tr><td>S0.1</td><td></td><td></td><td>950</td><td>1,760</td><td>59</td><td>2,510</td><td>4,628</td></tr><tr><td>S1.1</td><td></td><td>r</td><td>1,316</td><td>2,440</td><td>87</td><td>2,539</td><td>5,376</td></tr><tr><td>S1.2</td><td></td><td>d</td><td>11,106</td><td>21,201</td><td>91</td><td>28,033</td><td>53,222</td></tr><tr><td>S1.3</td><td></td><td>r</td><td>15,159</td><td>46,506</td><td>92</td><td>33,712</td><td>63,550</td></tr><tr><td>S1.4</td><td>w</td><td></td><td>14,227</td><td>26,781</td><td>92</td><td>32,573</td><td>61,327</td></tr><tr><td>S1.5</td><td></td><td>g</td><td>14,661</td><td>27,622</td><td>92</td><td>33,703</td><td>63,467</td></tr><tr><td>S1.6</td><td></td><td>a</td><td>453,569</td><td>856,383</td><td>96</td><td>780,310</td><td>1,483,877</td></tr><tr><td>S2.1</td><td></td><td>gy</td><td>195,763</td><td>379,037</td><td>126</td><td>415,368</td><td>806,375</td></tr><tr><td>S2.2</td><td>w</td><td></td><td>209,567</td><td>405,483</td><td>126</td><td>416,338</td><td>807,082</td></tr><tr><td>S2.3</td><td>br</td><td></td><td>195,763</td><td>379,037</td><td>126</td><td>415,368</td><td>806,375</td></tr><tr><td>S3.1</td><td></td><td>dr</td><td>594,220</td><td>1,299,494</td><td>159</td><td>1,264,577</td><td>2,548,485</td></tr><tr><td>S3.2</td><td>w</td><td>dr</td><td>1,403,410</td><td>4,805,873</td><td>160</td><td>4,776,350</td><td>9,546,995</td></tr><tr><td>S3.3</td><td>br</td><td></td><td>2,712,675</td><td>5,383,653</td><td>160</td><td>5,069,380</td><td>10,109,357</td></tr><tr><td>S3.4</td><td>br</td><td>w</td><td>2,823,433</td><td>5,606,270</td><td>160</td><td>5,431,266</td><td>10,812,140</td></tr><tr><td>S3.5</td><td></td><td>gy</td><td>2,713,843</td><td>5,417,007</td><td>163</td><td>5,369,124</td><td>10,760,613</td></tr><tr><td>S3.6</td><td>w</td><td>gy</td><td>2,724,273</td><td>5,440,233</td><td>163</td><td>5,602,352</td><td>11,234,870</td></tr><tr><td>S4.1</td><td>br</td><td>dr</td><td>29,384,127</td><td>59,724,969</td><td>194</td><td>55,227,479</td><td>112,581,896</td></tr><tr><td>S4.2</td><td></td><td>gy</td><td>28,901,983</td><td>59,017,480</td><td>196</td><td>57,790,270</td><td>118,260,379</td></tr><tr><td>S4.3</td><td>w</td><td>gy</td><td>35,622,226</td><td>72,379,889</td><td>197</td><td>68,055,576</td><td>138,631,569</td></tr><tr><td>S4.4</td><td>br</td><td>gy</td><td>34,536,645</td><td>70,276,113</td><td>197</td><td>69,045,657</td><td>140,987,869</td></tr><tr><td>S4.5</td><td>br</td><td>w</td><td>36,352,347</td><td>73,580,850</td><td>194</td><td>62,435,531</td><td>126,797,672</td></tr><tr><td>S5.1</td><td></td><td>gy</td><td>dr</td><td>d</td><td></td><td>not available</td><td></td></tr><tr><td>S5.2</td><td>w</td><td>gy</td><td>dr</td><td></td><td></td><td>not available</td><td></td></tr><tr><td>S5.3</td><td>br</td><td>w</td><td>dr</td><td></td><td></td><td>not available</td><td></td></tr><tr><td>S6.1</td><td>br</td><td>gy</td><td>dr</td><td></td><td></td><td>not available</td><td></td></tr><tr><td>S6.2</td><td>b</td><td>w</td><td>gy</td><td>dr</td><td></td><td>not available</td><td></td></tr><tr><td>S6.3</td><td>b</td><td>gy</td><td>dr</td><td>u</td><td></td><td>not available</td><td></td></tr><tr><td>S6.4</td><td>br</td><td>gy</td><td>dr</td><td></td><td></td><td>not available</td><td></td></tr><tr><td>S7.1</td><td>br</td><td>w</td><td>gy</td><td>dr</td><td></td><td>not available</td><td></td></tr><tr><td>S8.1</td><td>br</td><td>w</td><td>gy</td><td>dr</td><td>d</td><td>not available</td><td></td></tr></tbody></table>

Each scenario named *Sm.n* involves *m* obstacles. The letters in the columns about collisions indicate the colour of the involved vehicles: blue, green, red, white, yellow. The letters in the columns about pedestrians (visible and occluded) indicate their direction: aleatory (any adjacent cell), down, right, up. The next five columns give, if available, statistics about the corresponding (un)restricted LTSs (both reduced for strong bisimulation): number of states and transitions, and the radius of the unrestricted LTS (see Sect. 5.2).
<figure><img src="image_6.png" /><figcaption>Fig. 4: Pedestrian collision</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Fig. 5: Occluded pedestrian collision</figcaption></figure>

In all scenarios, the ego vehicle moves from the right edge towards the left edge of the map: it cannot move neither backwards, up, nor down, but only left, left&up, or left&down. We distinguish two variants: the *unrestricted* one, where the ego vehicle may stop at any time, and the *restricted* one, where the ego vehicle cannot stop for more than two time steps. The ego vehicle is free to arbitrarily choose moves satisfying these constraints (even if the move leads to a collision): hence we include all possible trajectories that could be computed by a navigation system. An execution of a scenario ends when the ego vehicle reaches the left edge or collides with a static or dynamic obstacle. We call *arrival* a situation where the ego vehicle reaches the left edge of the map at the same height as its initial position.

# 4 Formal Model

To formally analyse these scenarios, we use our freely accessible formal model<fnref n="10" /> [17], which has already served for several case studies [11, 12], in particular for generating—using conformance testing tools—test scenarios to be run in the CARLA simulator [5]. This model is written in LNT [3, 7], a modern language with an imperative syntax, close to mainstream programming languages, and a formal semantics rooted in concurrency theory. Concretely, the semantics of an LNT model is defined as an LTS (Labelled Transition System), i.e., a state space in which transitions between states are labelled with events resulting from rendezvous communications between concurrent processes in the system.

Our model consists of a *generic* part defining the rules common to all scenarios (1340 lines of LNT) and a *specific* part defining the details varying between scenarios, namely the number of static and dynamic obstacles and the behaviour of the dynamic obstacles (between 93 and 216 lines of LNT, depending on the number of obstacles).

Each actor (dynamic obstacle and ego vehicle) is represented as an LNT process. In each scenario, each obstacle is characterized by its initial position and a list of moves (speed and direction) defining its behavior. Once the list of moves has been executed completely, the obstacle stops. In all scenarios, the ego vehicle

<footnote n="10">¹⁰ https://sourcesup.renater.fr/scm/viewvc.php/marsrepo/031-AutoVehicles/02-LNT</footnote>
moves from the right edge to the left edge of the map. The ego vehicle is equipped
with sensors detecting the other actors present in its neighbourhood. This is rep-
resented as a *perception grid*, i.e., a 5x5 portion of the map having the ego vehicle
in its center. Each actor sends its move to the **ENVIRONMENT**, which updates the
map (encoded as a two-dimensional array of 10x10 cells) and broadcasts it to all
actors. These communication events yield transitions in the corresponding LTS:
in particular, **CAR_POSITION** indicates a move of the ego vehicle, and **LIDAR_MAP**
shows the current perception grid. To limit the size of the LTS and improve
the performance of verification, the model enforces a round-robin order for the
moves of the actors, each round corresponding to a (logical) time step, separated
by dedicated **TICK** events. This also enables the representation of simultaneous
moves in a way closer to the physical world simulated in CARLA [11].

As described in Section 3, the ego vehicle starts in all our scenarios at the
right edge and is free to move inside a “cone” towards the left edge of the map.
Hence, in each time step, the ego vehicle either stays at its position or moves
further to the left; in the restricted variants of the model, the ego vehicle may
stay at its position at most two times during the complete scenario.

The behaviour of a dynamic obstacle is defined by a list of moves (indicating
one of the eight possible moves to an adjacent cell in the map or a randomly
chosen one). Obstacles can always decide to stay at their current position and
(contrary to the ego vehicle) will never move to an already occupied cell (avoiding
collisions). When an obstacle moves outside the map, it disappears completely.

In all scenarios, four static obstacles (buildings) delimit a rectangular crossing of two roads. Scenarios S1.1, S2.2, S3.1, S3.3, S3.5, S4.5, S5.1, S6.3, and S8.1 feature also an additional static obstacle (parked bus) occluding a pedestrian.

# 5 Event Sequences and Probabilities

As a manner to compare scenarios quantitatively, we suggest using the probabil-
ities of particular event sequences to occur in the LTS of each scenario, converted
to a labeled DTMC (Discrete-Time Markov Chain). For simplicity, we consider
that all events are equiprobable (i.e., for each LTS state, all its outgoing transi-
tions have equal probabilities), leaving the experiments with specific event prob-
abilities for future work. Each event sequence considered can be characterized
using a generalized regular formula of MCL (Model Checking Language) [21],
and its probability can be computed using either exact, or approximate proba-
bilistic model checking, as explained in the subsections below.

## 5.1 Computing Probabilities of Event Sequences

Each event in a sequence (arrival, collision, perception, etc.) is described as
an MCL action predicate "{*E ?x:T !v*}", where *E* is the event name possibly
accompanied by data fields (exchanged during rendezvous in the original LNT
model). These data fields can be extracted and stored in variables (clause "*?x:T*"
stores a value of type *T* in variable *x*) or matched against given values (clause "*!v*"
matches against a value *v*). An action predicate may contain several extraction and/or matching clauses, as well as the wildcards "?any" (matching one field) and "..." (matching all remaining, zero or more, fields). Conditions can be added using the optional guard "where *C*", where *C* is a Boolean expression on the variables of extraction clauses. Events without data fields are denoted simply by their names, and the action predicate true denotes any event. Each event sequence is described as an MCL regular formula *R*, which is built on the alphabet of action predicates using extended regular expression operators: concatenation ("."), iteration 0 or more times ("*"), iteration *n* or more times ("{*n* ...}"), and iteration at most *n* times ("{0...*n*}").

We considered the following eight event sequences:

1. the ego vehicle arrives at its destination
   true* . ARRIVAL

2. the ego vehicle reaches the left edge without a collision, but not at its destination
   (not {COLLISION ...})* . {CAR_POSITION !0 ?any} and not ARRIVAL

3. the ego vehicle collides with an arbitrary obstacle
   true* . {COLLISION ...}

4. the ego vehicle collides with an obstacle (not the scenery)
   (not {COLLISION ...})* . {COLLISION ?o:string where o <> "SCENERY"}

5. the ego vehicle collides with an obstacle after at least *n* near-miss situations
   ((not ({COLLISION ...} or NEAR MISS))* . NEAR MISS) {n ...} .
   (not ({COLLISION ...} or NEAR MISS))* . {COLLISION ...}

6. the ego vehicle collides with an obstacle without having encountered a near-miss situation before the collision
   (not NEAR MISS)* . {COLLISION ...}

7. the ego vehicle perceives at least *n* obstacles simultaneously
   (not ARRIVAL)* . {LIDAR_MAP ?any ?any ?m:nat ?any where m >= n}

8. the ego vehicle arrives at destination before *n* time steps
   ((not (ARRIVAL or TICK))* . TICK) {0 ... n} .
   (not (ARRIVAL or TICK))* . ARRIVAL

When the LTS of a scenario can be completely generated, the probability of
each event sequence *R* above can be computed by evaluating the MCL proba-
bilistic temporal logic formula "{*R*}_{≥?0}" with the on-the-fly model checker [20]
of CADP.

## 5.2 Approximating Probabilities of Event Sequences

If the LTS becomes prohibitively large (because of too many obstacles in the sce-
nario), one can still *estimate* the probability of an event sequence using APMC
(Approximate Probabilistic Model Checking) [10], a particular case of statistical
model checking [16], which consists in generating execution traces and comput-
ing the percentage of traces matching the desired event sequence. The litera-
ture [1, 10, 15, 16] describes several formulas to compute a number of traces that
guarantee with a probability of $1 - \delta$ that the computed approximation is correct with an error of at most $\varepsilon$ (where the *confidence* $\delta$ and the *precision* $\varepsilon$ can be chosen between 0 and 1).

However, a correct approximation of the probabilities requires the traces to be of sufficient length: for example, the approximation of the probability for the ego vehicle to arrive at destination might be too low (possibly zero), if all traces are too short and too few traces contain an arrival. Concretely, for each event sequence, there must be a trace length $N$, such that for all traces of length at least $N$ it is possible to decide whether the trace matches the event sequence based only on the prefix of length $N$. Notice that, depending on the probabilistic formula $\varphi$ under verification, $N$ can be greater than the *radius* of the LTS, i.e., the maximal distance (length of the shortest sequence) from the initial state to every other state, because $\varphi$ may require to unroll loops several times. For instance, the unrestricted LTS of S1.1 has a radius of 87, but using APMC to approximate the probability that the ego vehicle does not move before the fifteenth time step<fnref n="11" /> requires traces of at least 114 events (the minimal length of a witness trace for this formula) to yield an estimation strictly greater than zero, and even longer traces to obtain a reasonable precision.

This suggests an intermediate approach between APMC and probabilistic model checking on the complete LTS. Consider a formula $\varphi$ requiring traces of at most length $N$. Thus, the probability that $\varphi$ holds on the complete LTS is the same as the probability that $\varphi$ holds on a *prefix*-LTS of depth $N$, which can be generated using a breadth-first traversal up to depth $N$. If $N$ is (significantly) smaller than the radius of the LTS, this intermediate approach combines the advantages of plain probabilistic model checking and APMC, namely precise results and reduced number of explored transitions.

In the case an interesting event sequence has no such upper bound on the traces, for example because it contains an unbounded repetition of events (as all event sequences in Section 5.1), APMC cannot be applied directly. A first idea would be to stepwise increase the length of the traces (or the prefix) and stop when the computed probabilities converge. However, there is the risk of detecting convergence too early: the approximation of the probability of the ego vehicle to arrive at destination is zero as long as the traces are too short, and starts increasing (and eventually converging) if there exists at least one trace of the current length containing an arrival.

Otherwise, one could either modify the event sequences (by replacing *-based repetitions with counter-based ones), or the model (by inhibiting unrestricted loops) to ensure the existence of an upper bound. We chose the latter approach, requiring all moves of the ego vehicle to change its position to the left and restricting the number of time steps with a “no-move” of the ego vehicle (i.e., the time steps when the ego vehicle does not change its position). This approach increases the LTS size (by a factor of about two due to the unfolding of the count of still allowed no-move steps, see Table 1) and also slightly changes the

<footnote n="11">¹¹ The corresponding event sequence can be described in MCL as follows:
"((not {CAR_POSITION ...})* . {CAR_POSITION ?n ?c: String where n =c}){15}"</footnote>
probabilities (because the traces with more no-move time steps are cut). Nevertheless, the approach does not add any new behaviour, the modified LTS being included in the original LTS (with respect to strong bisimulation).

We implemented the APMC approach as a Shell script (700 lines) on top of CADP, using a random simulator (with varying seeds) to extract execution traces, and the model checker to verify whether a trace matches an event sequence *R* by evaluating the MCL diamond modality “⟨*R*⟩ true” on the trace. The execution traces are computed only once and stored in text files, on which the MCL formulas are evaluated efficiently using the SEQ OPEN tool [8].

# 6 Scenario Assessment

We computed the probabilities for the event sequences given in Section 5 to compare all the scenarios derived from real traffic accident studies [14] listed in Table 1. Depending on the scenario, we either first generated the corresponding LTS and used probabilistic model checking, or (for the scenarios with LTS size marked *not available* in Table 1) we relied on APMC. In the latter case, to ensure a confidence $\delta$ of 5% and a precision $\varepsilon$ of 1%, we generated $\frac{\ln(2)-\ln(\delta)}{2\varepsilon^2} = 18,444$ traces [16, equation (2)]. We generated traces of 300 events, enough to force the ego vehicle either to reach the left edge of the map, or to collide with an obstacle.

For some examples, for which we could generate the LTS, we also compared the precise and approximate approaches. The approximate values had the expected precision, but there are notable differences in the efficiency. The question whether APMC is *faster* heavily depends on the scenario. Two aspects can be distinguished: the generation of the LTS or the set of traces and the computation of the probabilities. Notice that for each scenario, the LTS or the set of traces needs to be generated only once and can be reused to evaluate all probabilistic formulas. For all scenarios for which we could obtain the LTS, generating a single trace took less than one second; for the largest scenario S8.1, generating a single trace took about ten seconds. For all scenarios, each formula could be evaluated in less than one second on a trace. Thus, taken into account the time required for setting up the directories and accumulating the results, APMC takes about one second per trace or a bit more than five hours for one scenario-formula pair.

Hence, it is to be expected that APMC is slower (and less precise) if the LTS (not yet reduced for strong bisimulation) contains less transitions than the total number of transitions in all generated traces for APMC, i.e., the number of traces multiplied by their length and by the average branching factor of the LTS (because selecting one of the possible transitions takes roughly the same time as firing all of them). As shown on Figure 6, we indeed observed that for LTSs and prefix-LTSs with less than 18,444 * 300 * 2 = 11,066,400 transitions<fnref n="12" />, APMC was significantly slower for scenarios with at most three dynamic obstacles, but was faster for scenarios with at least four dynamic obstacles. Notice that to

<footnote n="12">¹² In our case, the average branching factor is less than two, with a maximal branching factor of four; the only exception is S1.6 with a maximal branching factor of five due to an obstacle moving randomly.</footnote>
reduce execution time, the generation of traces can be parallelized—but this is
also true for the generation of the (complete or prefix) LTS. We also observed
that minimizing the LTS before model checking reduces both its size and the
model checking time by a factor of two.

For most of our considered event sequences, there is no significant gain in
using a prefix-LTS for all event sequences leading to an **ARRIVAL** or **TRAVERSAL**,
because the prefix-LTS yielding probabilities close to those of the complete LTS
is only marginally smaller. A notable exception is the fourth event sequence
(collision, but not with the scenery): for this sequence and (unrestricted) scenario
S3.5, the difference between the probabilities computed for the complete LTS and
prefix-LTS of depth 100 is already smaller than 0.01, although the prefix-LTS
is not strongly bisimilar to (i.e., is strictly included in) the complete LTS for a
depth smaller than 163.

The following subsections present five figures based on the computed proba-
bilities for the restricted models and discuss how the insights obtained by their
analysis are beneficial for devising test scenarios. For readability of the figures,
we select series of scenarios.

## 6.1 Probabilities of Collision and Arrival

A first observation is that the probabilities of collision and arrival differ from one
scenario to another. Intuitively, increasing the number of obstacles increases the
probability of collision and decreases the probability for the ego vehicle to arrive
safely at destination. Consider the series of scenarios S0.1, S1.5, S2.1, S3.6, S4.3,
S5.2, S6.2, S7.1, S8.1, each adding one more obstacle to those already present.
Figure 7 shows the evolution of the probabilities for arrival, collision, collision
excluding the scenery, and traversal (i.e., reaching the left edge without collision
nor arrival). Notice that the probabilities of arrival, collision, and traversal sum
up to 1, because these are the three possible outcomes of an execution.

As expected, the highest (resp. lowest) probability of collision (resp. arrival)
is observed for the scenario with the most obstacles (S8.1) combining all critical
situations of Section 3. Interestingly, the probabilities of arrival and traversal do
not decrease linearly and the probability of collision (excluding scenery) does
not increase linearly either. Adding the third obstacle (white vehicle) has more
effect than the others: it adds the situation of a rear collision to the already
included front collision. However, adding *only* the white vehicle (S1.4, not shown
in Fig. 7) yields a *higher* probability of arrival than adding only the red vehicle
(S1.5). Adding the fifth obstacle (a second pedestrian moving in the opposite
direction to the ego vehicle) even *increases* the probability of arrival (the decrease
in the probability of collision is less significant): this might be explained by the
additional constraints that force the ego vehicle to stick to a straighter trajectory
(to avoid colliding with the pedestrian), favoring an arrival over a traversal.

Also, the probability of collision is for three and four obstacles already almost
at 50% (resp. 60%) and increases only slowly when adding further obstacles. This
suggests to limit the testing to four obstacles: more obstacles would increase the
cost without a significant gain in the probability of observing a collision.
<figure><img src="image_8.png" /><figcaption>Fig. 6: Overall validation times
(in hours)</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>Fig. 7: Probabilities of arrival, collision
(excluding scenery), and traversal</figcaption></figure>

## 6.2 Probability of Collision Preceded by a Near Miss

Figure 8 shows the probabilities of a collision preceded by near miss(es) for the same series of scenarios as in Section 6.1. In general, the more obstacles, the higher the probability of a collision preceded by a near miss. This confirms the intuition that more obstacles create more occasions for near misses. Similar to the findings of Section 6.1, adding the third obstacle has a significantly greater increase in the probabilities. Interestingly, the probability of at least three near misses decreases when adding the eighth obstacle: this might indicate that such a crowded environment leaves less room for the ego vehicle to successively avoid collisions so that a near miss situation more frequently leads to a collision.

## 6.3 Probability of Arrival Within a Given Time

Figure 9 shows the evolution of the probabilities for an arrival before *n* time steps (*n* ranging from nine to fifteen; the last data point corresponds to the probability of arrival without a time constraint) for the scenarios S1.3, S1.5, S2.2, S3.2, S3.4, S3.6, S4.2, S5.1, and S6.4. As expected, the probabilities of arrival before *n* time steps converge towards the probability of arrival. However, the speed of this convergence depends on the scenario. Roughly, the more obstacles, the faster the convergence: for instance, the scenarios S4.2 and S5.1 converge already for *n* = 11, whereas scenario S1.3 converges completely for *n* = 15 (but for all scenarios the probabilities are already very close for *n* = 12).

The figure also shows that more obstacles yield not necessarily a lower probability of arrival: for instance, the curve for scenario S3.4 (with three obstacles) is higher than those of scenarios S1.3 and S2.2, and the curve for scenario S6.4 is higher than the one for scenario S5.1.

## 6.4 Probability of Arrival Preceded by a Near Miss

Figure 10 compares the probabilities of arrival, preceded by none or at least *n* near-miss situations (*n* ranging from one to four) for the scenarios S0.1, S1.4, S2.2, S3.2, S4.1, S5.3, S6.3, S7.1, and S8.1. Only the number of obstacles in these
<figure><img src="image_10.png" /><figcaption>Fig. 8: Probabilities of a collision preceded by at least *n* near misses</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>Fig. 9: Probability of arrival before *n* time steps</figcaption></figure>

<figure><img src="image_12.png" /><figcaption>Fig. 10: Probability of an arrival preceded by *n* near misses</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>Fig. 11: Probability of arrival with simultaneous perception of *n* obstacles</figcaption></figure>

scenarios increases, but, contrary to the scenarios of Sect. 6.1, the actual set of obstacles changes between two scenarios: hence, the probability of arrival does not necessarily decrease when adding an obstacle. Notice that the probability of arrival is the sum of the probabilities for an arrival without and with at least one near-miss situation. For all scenarios, the probability for at least *n* ($> 0$) near-miss situations is higher than the probability of at least $n + 1$ near misses, because all execution traces of the latter are also traces of the former.

Unsurprisingly, for an increasing number of obstacles, the contribution to the probability of arrival shifts from an arrival without a near miss towards the probability for at least one near miss, because in a crowded environment, it is difficult for the ego vehicle to avoid near misses. Actually, the probability of an arrival without a preceding near-miss situation decreases with an increasing number of obstacles; it is almost zero already for the scenarios with three obstacles.

## 6.5 Probability of Arrival With Perception

Figure 11 shows, for the series of scenarios of Section 6.1, the probability of an arrival preceded by the simultaneous perception of at least *n* obstacles (expressed as a perception grid of the ego vehicle with at least *n* occupied cells). As to be expected, this probability increases with the number of obstacles in the scenario, but is bounded by the probability of arrival. Given that the static obstacles are
situated in the corners of the map and the perception of the ego vehicle is too
small to perceive more than one corner at a time, it might be surprising that
the probability to simultaneously perceive two or even three obstacles in scenario
S0.1 (without any dynamic obstacle) is greater than zero. However, this is due to
the size of the static obstacles (the one in the lower left corner occupies a total
of six cells). For some scenarios, the probabilities of arrival and simultaneous
perception of several obstacles are even identical: this indicates that in these
scenarios such a perception precedes inevitably every arrival.

The quantitative measures illustrated in this section for five different event
sequences allow one to sort the scenarios accordingly. Ultimately, it is up to the
test designer to choose the most appropriate event sequence to select tests.

7 Conclusion

The selection of test scenarios is crucial for ensuring the safety of autonomous vehicles. We proposed a generic approach for computing relevant measures to compare driving scenarios, based on formal modelling and probabilistic model checking. Using our publicly available formal model, we illustrated the approach to compare scenarios derived as variations from real traffic accident statistics. Taking advantage of approximation techniques, which avoid to completely explore the state space of a scenario, our approach scales to larger scenarios and enables comparison based on the probabilities of various event sequences expressed in temporal logic. Scalability can be further improved by exploiting the capabilities of recent multi-processor architectures, because parallelizing approximate probabilistic model checking is straightforward. The approach is useful for selecting the most relevant scenarios when devising a test suite for an autonomous vehicle, and also for creating interesting variations of scenarios present in datasets captured from real driving experiments. This can also help to contain testing costs by choosing the scenarios with similar characteristics but minimal number of obstacles.

The approach opens several perspectives. To go beyond the equiprobable
hypothesis of events, it would be interesting to experiment with specific proba-
bilities for particular events (inferred from real traffic datasets), using the label
renaming feature of the CADP model checker. It would be also interesting to
extend the formal model to support more evolved costs (e.g., acceleration/decel-
eration of the ego vehicle), or more complex trajectories including turns. Also,
the approach can be leveraged to establish a catalogue of generic, relevant tem-
poral logic formulas for comparing driving scenarios or even entire benchmarks.

***Acknowledgements.*** Part of this work has been supported by the Schlumberger Foundation and by the A-IQ Ready project, which receives funding within the Chips JU (the Public-Private Partnership for research, development and innovation under Horizon Europe) and National Authorities under grant agreement no. 101096658.
References

1. Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1) (Jan 2018), https://doi.org/10.1145/3158668

2. Caesar, H., Kabzan, J., Tan, K.S., Fong, W.K., Wolff, E., Lang, A., Fletcher, L., Beijbom, O., Omari, S.: NuPlan: A closed-loop ML-based planning benchmark for autonomous vehicles. In: CVPR ADP3 workshop (2021)

3. Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the LNT to LOTOS Translator (Version 7.3) (2024), https://cadp.inria.fr/publications/Champelovier-Clerc-Garavel-et-al-10.html, INRIA, France

4. Cheng, J., Chen, Y., Mei, X., Yang, B., Li, B., Liu, M.: Rethinking imitation-based planners for autonomous driving (2023)

5. Dosovitskiy, A., Ros, G., Codevilla, F., López, A.M., Koltun, V.: CARLA: an open urban driving simulator. In: CoRL. Proceedings of Machine Learning Research, vol. 78, pp. 1–16. PMLR (2017)

6. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. Journal on Software Tools for Technology Transfer 15(2), 89–107 (Apr 2013)

7. Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd – Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 10500, pp. 3–26. Springer (Oct 2017)

8. Garavel, H., Mateescu, R.: Seq.open: A tool for efficient trace-based verification. In: Graf, S., Mounier, L. (eds.) Proceedings of the 11th International SPIN Workshop on Model Checking of Software (SPIN’04), Barcelona, Spain. Lecture Notes in Computer Science, vol. 2989, pp. 150–155. Springer (Apr 2004)

9. Gruyer, D., Régnier, R., Ieng, S.S., El Zeenny, M., Andriantavison, K., Gasch, E., Habib, L., Renzaglia, A., Gava, C., Bernardin, F., Segonne, C., Mouchard, G.: WP2 state of the art: final report. Deliverable of PRISSMA Project L2.3, Plateforme de Recherche et d'Investissement pour la Sûreté et la Sécurité de la Mobilité Autonome, France (2024), https://prissma.univ-gustave-eiffel.fr/

10. Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2937, pp. 73–84. Springer (2004)

11. Horel, J.B., Laugier, C., Marsso, L., Mateescu, R., Muller, L., Paigwar, A., Renzaglia, A., Serwe, W.: Using Formal Conformance Testing to Generate Scenarios for Autonomous Vehicles. In: DATE/ASD 2022 - Design, Automation and Test in Europe - Autonomous Systems Design. pp. 532–537. IEEE, Antwerp, Belgium (Mar 2022). https://doi.org/10.23919/DATE54114.2022.9774581, https://inria.hal.science/hal-03516799

12. Horel, J.B., Ledent, P., Marsso, L., Muller, L., Laugier, C., Mateescu, R., Paigwar, A., Renzaglia, A., Serwe, W.: Verifying Collision Risk Estimation using Autonomous Driving Scenarios Derived from a Formal Model. Journal of Intelligent and Robotic Systems 107(4), 1–45 (Apr 2023). https://doi.org/10.1007/s10846-023-01808-3, https://inria.hal.science/hal-04138579

13. Junietz, P., Bonakdar, F., Klamann, B., Winner, H.: Criticality metric for the safety validation of automated driving using model predictive trajectory optimization. In: 2018 21st International Conference on Intelligent Transportation Systems (ITSC). pp. 60–65 (2018)
14. Ledoux, V., Krishnakumar, R., Herve, V.: Situations d'interactions accidentogènes : enjeux. Livrable L2.8, Projet Surca (2019), https://surca.univ-gustave-eiffel.fr/fileadmin/contributeurs/SURCA/WP2Livrable/SURCA_Livrable_L2_8-VF.pdf

15. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: An overview. In: Runtime Verification (2010), https://api.semanticscholar.org/CorpusID:8589228

16. Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical Model Checking, pp. 478–504. Springer International Publishing (2019). https://doi.org/10.1007/978-3-319-91908-9_23

17. Marsso, L., Mateescu, R., Muller, L., Serwe, W.: Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing. In: Mars 2022 - 5th Workshop on Models for Formal Analysis of Real Systems. EPTCS, vol. 355, pp. 60–117. Munich, Germany (Apr 2022). https://doi.org/10.4204/EPTCS.355.5, https://inria.hal.science/hal-03623521

18. Marsso, L., Mateescu, R., Serwe, W.: TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation. In: Beyer, D., Huisman, M. (eds.) Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18), Thessaloniki, Greece. Lecture Notes in Computer Science, vol. 10806, pp. 211–228. Springer (Apr 2018)

19. Marsso, L., Mateescu, R., Serwe, W.: Automated transition coverage in behavioural conformance testing. In: Casola, V., Benedictis, A.D., Rak, M. (eds.) Testing Software and Systems - 32nd IFIP WG 6.1 International Conference, ICTSS 2020, Naples, Italy, December 9-11, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12543, pp. 219–235. Springer (2020). https://doi.org/10.1007/978-3-030-64881-7_14

20. Mateescu, R., Requeno, J.I.: On-the-fly model checking for extended action-based probabilistic operators. Springer International Journal on Software Tools for Technology Transfer (STTT) 20(5), 563–587 (2018)

21. Mateescu, R., Thivolle, D.: A Model Checking Language for Concurrent Value-Passing Systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) Proc. of the 15th International Symposium on Formal Methods (FM’08). Lecture Notes in Computer Science, vol. 5014, pp. 148–164. Springer (May 2008)

22. Riedmaier, S., Ponn, T., Ludwig, D., Schick, B., Diermeyer, F.: Survey on scenario-based safety assessment of automated vehicles. IEEE Access 8, 87456–87477 (2020). https://doi.org/10.1109/ACCESS.2020.2993730

23. Wang, T., Kim, S., Ji, W., Xie, E., Ge, C., Chen, J., Li, Z., Ping, L.: Deepaccident: A motion and accident prediction benchmark for v2x autonomous driving. arXiv preprint arXiv:2304.01168 (2023)

24. Westhofen, L., Neurohr, C., Koopmann, T., Butz, M., Schütt, B., Utesch, F., Kramer, B., Gutenkunst, C., Böde, E.: Criticality metrics for automated driving: A review and suitability analysis of the state of the art. Archive Computational Methods Engineering 30, 1–35 (2023)