$\mathsf {SceneChecker}$: Boosting Scenario Verification Using Symmetry Abstractions

Abstract

We present $\mathsf {SceneChecker}$, a tool for verifying scenarios involving vehicles executing complex plans in large cluttered workspaces. $\mathsf {SceneChecker}$ converts the scenario verification problem to a standard hybrid system verification problem, and solves it effectively by exploiting structural properties in the plan and the vehicle dynamics. $\mathsf {SceneChecker}$ uses symmetry abstractions, a novel refinement algorithm, and importantly, is built to boost the performance of any existing reachability analysis tool as a plug-in subroutine. We evaluated $\mathsf {SceneChecker}$ on several scenarios involving ground and aerial vehicles with nonlinear dynamics and neural network controllers, employing different kinds of symmetries, using different reachability subroutines, and following plans with hundreds of waypoints in complex workspaces. Compared to two leading tools, DryVR and Flow*, $\mathsf {SceneChecker}$ shows 14$\times$ average speedup in verification time, even while using those very tools as reachability subroutines.

The authors are supported by a research grant from The Boeing Company and a research grant from NSF (FMITF: 1918531). We would like to thank John L. Olson, Aaron A. Mayne, and Michael R. Abraham from The Boeing Company for valuable technical discussions.

1 Introduction

Remarkable progress has been made in safety verification of hybrid and cyber-physical systems in the last decade [2,3,4,5,6,7,8,9]. The methods and tools developed have been applied to check safety of aerospace, medical, and autonomous vehicle control systems [4, 5, 10, 11]. The next barrier in making these techniques usable for more complex applications is to deal with what is colloquially called the scenario verification problem. A key part of the scenario verification problem is to check that a vehicle or an agent can execute a plan through a complex environment. A planning algorithm (e.g., probabilistic roadmaps [12] and rapidly-exploring random trees (RRTs) [13]) generates a set of possible paths avoiding obstacles, but only considering the geometry of the scenario, not the dynamics. The verification task has to ensure that the plan can indeed be safely executed by the vehicle with all the dynamic constraints and the state estimation uncertainties. Indeed, one can view a scenario as a hybrid automaton with the modes defined by the segments of the planner, but this leads to massive models. Encoding such automata in existing tools presents some practical hurdles. More importantly, analyzing such models is challenging as the over-approximation errors and the analysis times grow rapidly with the number of transitions. At the same time, such large hybrid verification problems also have lots of repetitions and symmetries, which suggest new opportunities.

We present $\mathsf {SceneChecker}$, a tool that implements a symmetry abstraction-refinement algorithm for efficient scenario verification. Symmetry abstractions significantly reduce the number of modes and edges of an automaton ${H}$ by grouping all modes that share symmetric continuous dynamics [14]. $\mathsf {SceneChecker}$ implements a novel refinement algorithm for symmetry abstractions and is able to use any existing reachability analysis tool as a subroutine. Our current implementation comes with plug-ins for using Flow$^{*}$ [4] and DryVR [6]. $\mathsf {SceneChecker}$’s verification algorithm is sound, i.e., if it returns $safe$, then the reachset of ${H}$ indeed does not intersect the unsafe set. The algorithm is lossless in the sense that if one can prove safety without using abstraction, then $\mathsf {SceneChecker}$ can also prove safety via abstraction-refinement, and typically a lot faster. $\mathsf {SceneChecker}$ can be found on figshare: https://figshare.com/articles/software/CAV2021_reduce_v6_ova/14504352 and its website: https://publish.illinois.edu/scenechecker/. An extended version of this paper is available online [1].

$\mathsf {SceneChecker}$ offers an easy interface to specify plans, agent dynamics, obstacles, initial uncertainty, and symmetry maps. $\mathsf {SceneChecker}$ checks if a fixed point has been reached after each call to the reachability subroutine, avoiding repeating computations. First, $\mathsf {SceneChecker}$ represents the input scenario as a hybrid automaton ${H}$ where modes are defined by the plan’s segments. It uses the symmetry maps provided by the user to construct an abstract automaton ${H}_v$. Automaton ${H}_v$ represents another scenario with fewer segments, each representing an equivalence class of symmetric segments in ${H}$. A side effect of the abstraction is that upon reaching waypoints in ${H}_v$, the agent’s state resets non-deterministically to a set of possible states. For example, in the case of rotation and translation invariance, the abstract scenario would have a single segment for any set of segments with a unique length in the original scenario. $\mathsf {SceneChecker}$ refines ${H}_v$ by splitting one of its modes to two modes. That corresponds to representing a set of symmetric segments with one more segment in the abstract scenario, capturing more accurately the original scenario¹.

We evaluated $\mathsf {SceneChecker}$ on several scenarios where car and quadrotor agents with nonlinear dynamics follow plans to reach several destinations in 2D and 3D workspaces with hundreds of waypoints and polytopic obstacles. We considered different symmetries (translation and rotation invariance) and controllers (Proportional-Derivative (PD) and Neural Networks (NN)). We compared the verification time of $\mathsf {SceneChecker}$ with DryVR and Flow* as reachability subroutines against Flow* and DryVR as standalone tools. $\mathsf {SceneChecker}$ is faster than both tools in all scenarios considered, achieving an average of 14$\times$ speedup in verification time (Table 1). In certain scenarios where Flow* timed out (executing for more than 120 min), $\mathsf {SceneChecker}$ is able to complete verification in as fast as 12 min using Flow* as a subroutine. $\mathsf {SceneChecker}$ when using abstraction-refinement achieved 13$\times$ speedup in verification time over not using abstraction-refinement in scenarios with the NN-controlled quadrotor (Sect. 7).

Related Work. The idea of using symmetries to accelerate verification has been exploited in a number of contexts such as probabilistic models [15, 16], automata [17, 18], distributed architectures [19], and hardware [20, 21]. Some symmetry utilization algorithms are implemented in Mur$\phi$ [22] and Uppaal [23].

In our context of cyber-physical systems, Bak et al. [24] suggested using symmetry maps, called reachability reduction transformations, to transform reachsets to symmetric reachsets for continuous dynamical systems modeling non-interacting vehicles. Maidens et al. [25] proposed a symmetry-based dimensionality reduction method for backward reachable set computations for discrete dynamical systems. Majumdar et al. [26] proposed a safe motion planning algorithm that computes a family of reachsets offline and composes them online using symmetry. Bujorianu et al. [27] presented a symmetry-based theory to reduce stochastic hybrid systems for faster reachability analysis and discussed the challenges of designing symmetry reduction techniques across mode transitions.

In a more closely related research, we presented a modified version of DryVR that utilizes symmetry to cache reachsets aiming to accelerate simulation-based safety verification of continuous dynamical systems [28]. We developed the related tool $\mathsf {CacheReach}$ that implements a hybrid system verification algorithm that uses symmetry to accelerate reachability analysis [29]. $\mathsf {CacheReach}$ caches and shares computed reachsets between different modes of non-interacting agents using symmetry. $\mathsf {SceneChecker}$ is based on the theory of symmetry abstractions of hybrid automata we presented in [14]. We suggested computing the reachset of the abstract automaton instead of the concrete one then transform it to the concrete reachset using symmetry maps to accelerate verification. $\mathsf {SceneChecker}$ is built based on this line of work with significant algorithmic and engineering improvements. In addition to the abstraction of [14], $\mathsf {SceneChecker}$ 1) maps the unsafe set to an abstract unsafe set and verifies the abstract automaton instead of the concrete one and 2) decreases the over-approximation error of the abstraction through refinement. $\mathsf {SceneChecker}$ does not cache reachsets and thus saves cache-access and reachset-transformation times and does not incur over-approximation errors due to caching that $\mathsf {CacheReach}$ suffers from [29]. At the implementation level, $\mathsf {SceneChecker}$ accepts plans that are general directed graphs and polytopic unsafe sets while $\mathsf {CacheReach}$ accepts only single-path plans and hyperrectangle unsafe sets. We show more than $30\times$ speedup in verification time while having more accurate verification results when comparing $\mathsf {SceneChecker}$ against $\mathsf {CacheReach}$ (Table 1 in Sect. 7).

2 Specifying Scenarios in $\mathsf {SceneChecker}$

A scenario verification problem is specified by a set of fixed obstacles, a plan, and an agent that is supposed to execute the plan without running into the obstacles (e.g., see Fig. 1B). For ground and air vehicles, for example, the agent moves in a subset of the 2D or the 3D Euclidean space called the workspace. A plan is a directed graph ${G}= \langle V, S\rangle$ with vertices $V$ in the workspace called waypoints and edges $S$ called segments². A general graph allows for nondeterministic and contingency planning.

An agent is a control system that can follow waypoints. Let the state space of the agent be $X$ and $\varTheta \subseteq X$ be the uncertain initial set. Let $s_{ init }$ be the initial segment in ${G}$ that the agent has to follow. From any state $x\in X$, the agent follows a segment $s\in S$ by moving along a trajectory. A trajectory is a function $\xi :X\times S \times {\mathbb {R}^{\ge 0}}\rightarrow X$ that meets certain dynamical constraints of the vehicle. Dynamics are either specified by ordinary differential equations (ODE) or by a black-box simulator. For ODE models, $\xi$ is a solution of an equation of the form: $\frac{d \xi }{dt}(x, s, t) = f(\xi (x, s, t),s)$, for any $t \in {\mathbb {R}^{\ge 0}}$ and $\xi (x, s, 0) = x$, where $f: X\times S\rightarrow X$ is Lipschitz continuous in the first argument. Note that the trajectories only depend on the segment the agent is following (and not on the full plan ${G}$). We denote by $\xi . fstate$, $\xi . lstate$, and $\xi .{ dom }$ the initial and last states and the time domain of the time bounded trajectory $\xi$, respectively.

We can view the obstacles near each segment as sets of unsafe states, ${ O }: S\rightarrow 2^X$. The map $tbound : S\rightarrow {\mathbb {R}^{\ge 0}}$ determines the maximum time the agent should spend in following any segment. For any pair of consecutive segments $(s,s')$, i.e. sharing a common waypoint in ${G}$, $guard ((s,s'))$ defines the set of states (a hyperrectangle around a waypoint) at which the agent is allowed to transition from following $s$ to following $s'$.

3 Transforming Scenarios to Hybrid Automata

The input scenario is first represented as a hybrid automaton by a $\mathsf{Hybrid}$ $\mathsf{constructor}$. This constructor is a Python function that parses the $\mathsf{Scenario}$ $\mathsf{file}$ and constructs the data structures to store the scenario’s hybrid automaton components. In what follows, we describe the constructed automaton informally. In our current implementation, sets are represented either as hyper-rectangles or as polytopes using the Tulip Polytope Library³.

Scenario as a Hybrid Automaton. A hybrid automaton has a set of modes (or discrete states) and a set of continuous states. The evolution of the continuous states in each mode is specified by a set of trajectories and the transition across the modes are specified by $guard$ and $reset$ maps. The agent following a plan in a workspace can be naturally modeled as a hybrid automaton ${H}$, where $s_ init$ and $\varTheta$ are its initial mode and set of states.

Each segment $s\in S$ of the plan ${G}$ defines a mode of ${H}$ (e.g. see Fig. 1A). The set of edges $E\subseteq S\times S$ of ${H}$ is defined as pairs of consecutive segments in ${G}$. For an edge $e\in E$, $guard (e)$ is the same as that of ${G}$. The $reset$ map of ${H}$ is the identity map. We will see in Sect. 5 that abstract automata will have nontrivial reset maps.

Verification Problem. An execution of length k is a sequence $\sigma := (\xi _0, s_0), \ldots , (\xi _k,s_k)$. It models the behavior of the agent following a particular path in the plan G. An execution $\sigma$ must satisfy: 1) $\xi _0. fstate \in \varTheta$ and $s_0 =s_ init$, for each $i\in \{0,\ldots , k-1\}$, 2) $(s_i,s_{i+1}) \in E$, 3) $\xi _i. lstate \in guard ((s_i, s_{i+1}))$, and 4) $\xi _i. lstate = \xi _{i+1}. fstate$, and 5) for each $i\in \{0,\ldots , k\}$, $\xi _i.{ dom } \le tbound (s_i).$ The set of reachable states is $Reach _{H}:= \{ \sigma . lstate \ |\ \sigma$ is an execution$\}$. The restriction of $Reach _{H}$ to states with mode $s\in S$ (i.e., agent following segment $s$) is denoted by $Reach _{H}(s)$. Thus, the hybrid system verification problem requires us to check whether $\forall s\in S$, $Reach _{H}(s) \cap { O }(s) = \emptyset$.

4 Specifying Symmetry Maps in $\mathsf {SceneChecker}$

The hybrid automaton representing a scenario, as constructed by the $\mathsf{Hybrid}$ $\mathsf{constructor}$, is transformed into an abstract automaton. $\mathsf {SceneChecker}$ uses symmetry abstractions [14]. The abstraction is constructed by the $\mathsf{abstract}$ function (line 1 of Algorithm 1) which uses a collection of pairs of maps $\varPhi = \{(\gamma _{s}: X\rightarrow X,\rho _{s}: S\rightarrow S)\}_{s\in S}$ that is provided by the user. We describe below how these maps are specified by the user in the $\mathsf{Dynamics}$ $\mathsf{file}$. These maps should satisfy:

$$\begin{aligned} \forall \ t\ge 0, x_0 \in X, s\in S, \gamma _s(\xi (x_0, s,t)) = \xi (\gamma _s(x_0), \rho _s(s), t). \end{aligned}$$

(1)

where $\forall s\in S$, the map $\gamma _s$ is differentiable and invertible. Such maps are called symmetries for the agent’s dynamics. They transform the agent’s trajectories to other symmetric ones of its trajectories starting from symmetric initial states and following symmetric modes (or segments in our scenario verification setting). It is worth noting that (1) does not depend on whether the trajectories $\xi$ are defined by ODEs or black-box simulators. Currently, condition (1) is not checked by $\mathsf {SceneChecker}$ for the maps specified by the user. However, in the following discussion, we present some ways for the user to check (1) on their own. For ODE models, a sufficient condition for (1) to be satisfied is if: $\forall \ x\in X,s\in S,\ \frac{\partial \gamma _s}{\partial x} f(x, s) = f(\gamma _s(x), \rho _s(s))$, where f is the right-hand-side of the ODE [30]. For black-box models, (1) can be checked using sampling methods. In realistic settings, dynamics might not be exactly symmetric due to unmodeled uncertainties. In the future, we plan to account for such uncertainties as part of the reachability analysis.

In scenario verification, a given workspace would have a coordinate system according to which the plan (waypoints) and the agent’s state (position, velocity, heading angle, etc.) are represented. In a 2D workspace, for any segment $s\in S$, an example symmetry $\rho _s$ would transform the two waypoints of s to a new coordinate system where the second waypoint is the origin and $s$ is aligned with the negative side of the horizontal axis (see Fig. 1D). The corresponding $\gamma _s$ would transform the agent’s state to this new coordinate system (e.g. by rotating its position and velocity vectors and shifting the heading angle). For such a pair $(\gamma _s,\rho _s)$ to satisfy (1), the agent’s dynamics have to be invariant to such a coordinate transformation and (1) merely formalizes this requirement. Such an invariance property is expected from vehicles’ dynamics–rotating or translating the lane should not change how an autonomous car behaves.

5 Symmetry Abstraction of the Scenario’s Automaton

In this section, we describe how the $\mathsf{abstract}$ function in Algorithm 1 uses the functions in the $\mathsf{Dynamics}$ $\mathsf{file}$ to construct an abstraction of the scenario’s hybrid automaton provided by the $\mathsf{Hybrid}$ $\mathsf{constructor}$. Given the symmetry maps of $\varPhi$, the symmetry abstraction of ${H}$ is another hybrid automaton ${H}_v$ that aggregates many symmetric modes (segments) of ${H}$ into a single mode of ${H}_v$.

Modes and Transitions. Any segment $s\in S$ of ${H}$ is mapped to the segment $\rho _s(s)$ in ${H}_v$ using $\mathsf{modeVir}$. The set of modes $S_v$ of ${H}_v$ is the set of segments $\{\rho _s(s)\}_{s\in S}$. For any $s_v$, $tbound _v(s_v) = \max _{s\in S, s_v = \rho _s(s)} tbound (s)$. In the example of Sect. 4 (Fig. 1D), the segments in ${H}_v$ are aligned with the horizontal axis and ending at the origin. The number of segments in ${H}_v$ would be the number of segments in ${G}$ with unique lengths. The agent would always be moving towards the origin of the workspace in the abstract scenario. Any edge $e= (s, s') \in E$ of ${H}$ is mapped to the edge $e_v = (\rho _s(s), \rho _{s'}(s'))$ in ${H}_v$. The $guard (e)$ is mapped to $\gamma _s( guard (e))$ using $\mathsf{polyVir}$ which becomes part of $guard _v(e_v)$ in ${H}_v$. For any $x\in X$, $reset (x, e)$, which is equal to $x$, is mapped to $\gamma _{s'} (\gamma _s^{-1}(x))$ and becomes part of $reset _v(x, e_v)$ in ${H}_v$. In our example in Sect. 4, the $\gamma _s^{-1}(x)$ would represent $x$ in the absolute coordinate system assuming it was represented in the coordinate system defined by segment $s$. The $\gamma _{s'}(\gamma _s^{-1}(x))$ would represent $\gamma _s^{-1}(x)$ in the new coordinate system defined by segment $s'$. The $guard _v(e_v)$ would be the union of rotated hyperrectangles centered at the origin that result from translating and rotating the guards of the edges represented by $e_v$. The initial set $\varTheta$ of ${H}$ is mapped to $\varTheta _v = \gamma _{s_{ init }}(\varTheta )$, the initial set of ${H}_v$. A formal definition of symmetry abstractions can be found in [1] (or [14]).

The unsafe map ${ O }$ is mapped to ${ O }_v$, where $\forall s_v \in S_v, { O }_v(s_v) = \cup _{s\in S, \rho _s(s) = s_v} \gamma _s({ O }(s))$. That means that the obstacles near any segment $s\in S$ in the environment will be mapped to be near its representative segment $\rho _s(s)$ in ${H}_v$.

A forward simulation relation between ${H}$ and ${H}_v$ can show that if ${H}_v$ is safe with respect to ${ O }_v$, then ${H}$ is safe with respect to ${ O }$. More formally, if $\forall s_v \in S_v, Reach _{{H}_v}(s_v) \cap { O }_v(s_v) = \emptyset$, then $\forall s\in S, Reach _{H}(s) \cap { O }(s) = \emptyset$ [14].

6 $\mathsf {SceneChecker}$ Algorithm Overview

A sketch of the core abstraction-refinement algorithm is shown in Algorithm 1. It constructs a symmetry abstraction ${H}_v$ of the concrete automaton ${H}$ resulting from the $\mathsf{Hybrid}$ $\mathsf{constructor}$. $\mathsf {SceneChecker}$ attempts to verify the safety of ${H}_v$ using traditional reachability analysis. $\mathsf {SceneChecker}$ uses a $cache$ to store per-mode initial sets from which reachsets have been computed and thus avoids repeating computations. An example run is shown in Fig. 1.

Fig. 1.

A simple scenario with a car following a plan with six segments is shown in B. Set of initial positions (green square), unsafe set (grey), and the segments (black lines). The automaton (A) has one mode per segment. Translation and rotation symmetries are used to abstract A to the automaton C. The abstraction translates and rotates each segment of the original scenario to a segment aligned with the x-axis and ends at the origin resulting in the segments (i.e. modes) $s_v^0$ and $s_v^1$. The unsafe set is transformed accordingly for each mode as shown in D. SceneChecker computes the reachset of C which turns out to be unsafe; to illustrate the process this abstract reachset transformed to the original scenario is shown in E. The colors refer to a different abstract modes. The algorithm refines C to F by adding $s_v^2$ (same segment as $s_v^1$ but different guard). The reachset of F is safe and the algorithm terminates (H). (The colored figure is available in the online version of this paper)

The core algorithm $\mathsf{verify}$ (Algorithm 2) is called iteratively. If $\mathsf{verify}$ returns $( safe , \bot )$ or $( unknown ,\bot )$, $\mathsf {SceneChecker}$ returns the same result. If $\mathsf{verify}$ instead results in $( refine , s_v^*)$, $\mathsf{splitMode}$ (check the extended version of this paper [1] for the formal definition) is called to refine ${H}_v$ by splitting $s_v^*$ into two modes $s_v^1$ and $s_v^2$. Each of the two modes would represent part of the set of the segments of $S$ that were originally mapped to $s_v$ in $rv$. Then the edges, guards, resets, and the unsafe sets related to $s_v$ are split according to their definitions.

The function $\mathsf{verify}$ executes a depth first search (DFS) over the mode graph of ${H}_v$. For any mode $s_v$ being visited, $\mathsf{computeReachset}$ computes $R_v$, an over-approximation of the agent’s reachset starting from $initset$ following segment $s_v$ for time $tbound _v(s_v)$. If $R_v \cap { O }_v(s_v) = \emptyset$, $\mathsf{verify}$ recursively calls $s_v$’s children continuing the DFS in line 6. Before calling each child, its initial set is computed and the part for which a reachset has already been computed and stored in $cache$ is subtracted. If all calls return $safe$, then $initset$ is added to the other initial sets in $cache [s_v]$ (line 12) and $\mathsf{verify}$ returns $safe$. Most importantly, if $\mathsf{verify}$ returns $( refine ,s_v^*)$ for any of $s_v$’s children, it directly returns $( refine ,s_v^*)$ for $s_v$ as well (line 7). If any child returns $unknown$ or $R_v$ intersects ${ O }_v(s_v)$, $\mathsf{verify}$ will need to split $s_v$. In that case, it checks if $rv ^{-1}[s_v]$ is not a singleton set and thus amenable to splitting (line 10). If $s_v$ can be split, $\mathsf{verify}$ returns $( refine , s_v)$. Otherwise, $\mathsf{verify}$ returns $( unknown , \bot )$ implicitly asking one of $s_v$’s ancestors to be split instead.

Correctness. $\mathsf {SceneChecker}$ ensures that all the refined automata ${H}_v$’s are abstractions of the original hybrid automaton ${H}$ (a proof is given in the extended version of this paper [1]). For any mode with a reachset intersecting the unsafe set, $\mathsf {SceneChecker}$ keeps refining that mode and its ancestors until safety can be proven or ${H}_v$ becomes ${H}$.

Theorem 1

(Soundness). If $\mathsf {SceneChecker}$ returns $safe$, then ${H}$ is $safe$.

If $\mathsf{verify}$ is provided with the concrete automaton ${H}$ and unsafe set ${ O }$, it will be the traditional safety verification algorithm having no over-approximation error due to abstraction. If such a call to $\mathsf{verify}$ returns $safe$, then $\mathsf {SceneChecker}$ is guaranteed to return $safe$. That means that the refinement ensures that the over-approximation error of the reachset caused by the abstraction is reduced to not alter the verification result.

Counter-examples. $\mathsf {SceneChecker}$ currently does not find counter-examples to show that the scenario is $unsafe$. There are several sources of over-approximation errors, namely, $\mathsf{computeReachset}$ and guard intersections. Even after all the over-approximation errors from symmetry abstractions are eliminated, as refinement does, it still cannot infer unsafe executions or counter-examples because of the other errors. We plan to address this in the future by combining the current algorithm with systematic simulations.

7 Experimental Evaluation

Agents and Controllers. In our experiments, we consider two types of nonlinear agent models: a standard 3-dimensional car (C) with bicycle dynamics and 2 inputs, and a 6-dimensional quadrotor (Q) with 3 inputs. For each of these agents, we developed a PD controller and a NN controller for tracking segments. The NN controller for the quadrotor is from Verisig’s paper [9] but modified to be rotation symmetric (check the extended version of this paper [1] for more details). Similarly, the NN controller for the car is made rotation symmetric. Both NN controllers are translation symmetric as they take as input the difference between the agent’s state and the segment being followed. The PD controllers are translation and rotation symmetric by design.

Symmetries. We experimented with two different collections of symmetry maps $\varPhi$s: 1) translation symmetry (T), where for any segment $s$ in ${G}$, $\gamma _s$ maps the states so that the coordinate system is translated by a vector that makes its origin at the end waypoint of $s$, and 2) rotation and translation symmetry (TR), where instead of just translating the origin, $\varPhi$ rotates the xy-plane so that $s$ is aligned with the x-axis, which we described in Sect. 4. For each agent and one of its controllers, we manually verified that condition (1) is satisfied for each of the two $\varPhi$s using the sufficient condition for ODEs in Sect. 4.

Scenarios. We created four scenarios with 2D workspaces (S1-4) and one scenario with a 3D workspace (S5) with corresponding plans. We generated the plans using an RRT planner [31] after specifying a number of goal sets that should be reached. We modified S4 to have more obstacles but still have the same plan and named the new version S4.b and the original one S4.a. When the quadrotor was considered, the waypoints of the 2D scenarios (S1-4) were converted to 3D representation by setting the altitude for each waypoint to 0. Scenario S5 is the same as S2 but S5’s waypoints have varying altitudes. The scenarios have different complexities ranging from few segments and obstacles to hundreds of them. All scenarios are safe when traversed by any of the two agents.

We verify these scenarios using $\mathsf {SceneChecker}$ and $\mathsf {CacheReach}$, each with two instances, one with DryVR and the other with Flow*, implementing $\mathsf{computeReachset}$. We also use DryVR and Flow* as independent tools to verify the same scenarios. The results of experiments with tools that involve DryVR (i.e., $\mathsf {SceneChecker}$+DryVR, $\mathsf {CacheReach}$+DryVR, and DryVR) are stochastic and change between runs. The reason is that each time DryVR is called, it randomly samples traces of the system from which it computes the requested reachset. We fix the random seed for repeatable results in this section. We show close averaging-based results on $\mathsf {SceneChecker}$’s website.

$\mathsf {SceneChecker}$ is able to verify all scenarios with PD controllers. The results are shown in Table 1⁴ and plotted for C-S1 using $\mathsf {SceneChecker}$+Flow* in Fig. 1.

Observation 1: $\mathsf {SceneChecker}$ offers fast scenario verification and boosts existing reachability tools Looking at the two total time (Tt) columns for the two instances of $\mathsf {SceneChecker}$ with the corresponding columns for Flow* and DryVR, it becomes clear that symmetry abstractions can boost the verification performance of reachability engines. For example, in C-S4.a, $\mathsf {SceneChecker}$+DR was around $20\times$ faster than DryVR. In C-S3, $\mathsf {SceneChecker}$ with Flow* was around $16\times$ faster than Flow*. In scenario Q-S5, $\mathsf {SceneChecker}$ timed out at least in part because a $\mathsf{computeReachset}$ call to Flow* timed out. Even when many refinements are required and thus causing several repetitions of the verification process in Algorithm 1, $\mathsf {SceneChecker}$ is still faster than DryVR and Flow* (C-S4.b). All three tools resulted in $safe$ for all scenarios when completed executions.

Table 1. Comparison between $\mathsf {SceneChecker}$, DryVR (DR), Flow* (F*), and $\mathsf {CacheReach}$ ($\mathsf{CacheR}$). Both $\mathsf {SceneChecker}$ and $\mathsf {CacheReach}$ use reachability tools as subroutines. The subroutines used are specified after the ‘+’ sign. $\varPhi$ is TR. The table shows the number of mode-splits performed (Nrefs), the total number of calls to $\mathsf{computeReachset}$ (Rc), the total time spent in reachset computations (Rt), and the total computation time in minutes (Tt). In scenarios where a tool ran over 120 min, we marked the Tt column as ‘Timed out’ (TO) and the other ones as ‘Not Available’ (NA).

Observation 2: $\mathsf {SceneChecker}$ is faster and more accurate than $\mathsf {CacheReach}$ Since $\mathsf {CacheReach}$ only handles single-path plans, we only verify the longest path in the plans of the scenarios in its experiments. $\mathsf {CacheReach}$’s instance with Flow* resulted in unsafe reachsets in C-S1 and C-S4.b scenarios likely because of the caching over-approximation error. In all scenarios where $\mathsf {CacheReach}$ completed verification besides C-S4.b, it has more Rc and longer Tt (more than $30\times$ in C-S2) while verifying simpler plans than $\mathsf {SceneChecker}$ using the same reachability subroutine. In all Q scenarios, both instances of $\mathsf {CacheReach}$, with Flow* and DryVR, timed out.

Observation 3: More symmetric dynamics result in faster verification time $\mathsf {SceneChecker}$ usually runs slower in 3D scenarios compared to 2D ones (Q-S2 vs. Q-S5) in part because there is no rotational symmetry in the z-dimension to exploit. That leads to larger abstract automata. Therefore, many more calls to $\mathsf{computeReachset}$ are required.

We only used $\mathsf {SceneChecker}$’s instance with DryVR for agents with NN-controllers⁵. We tried different $\varPhi$s. The results are shown in Table 2. When not using abstraction-refinement, $\mathsf {SceneChecker}$ took 10.5, 130.95, and 74.15 min for the QNN-S2, QNN-S3, and QNN-S4 scenarios, while DryVR took 5.22, 52.56, and 61.31 min for the same scenarios, respectively. Comparing these results with those in Table 2 shows that the speedup in verification time of $\mathsf {SceneChecker}$ is caused by the abstraction-refinement algorithm, achieving more than 13$\times$ in certain scenarios (QNN-S4 using $\varPhi =$ T). $\mathsf {SceneChecker}$+DR was more than 10$\times$ faster than DryVR in the same scenario.

Table 2. Comparison between $\varPhi$s. In addition to the statisitics of Table 1, this table reports the number of modes and edges in the initial and final (after refinement) abstractions ($|S_v|^i$, $|E_v|^i$; $|S_v|^f$, and $|E_v|^f$, respectively)

Observation 4: Choice of $\varPhi$ is a trade-off between over-approximation error and number of refinements The choice of $\varPhi$ affects the number of refinements performed and the total running times (e.g. QNN-S2, QNN-S3, and QNN-S4). Using TR leads to a more succinct ${H}_v$ but larger over-approximation error causing more mode splits. On the other hand, using T leads to a larger ${H}_v$ but less over-approximation error and thus fewer refinements. This trade-off can be seen in Table 2. For example, QNN-S4 with $\varPhi =$ T resulted in zero mode splits leading to $|S_v|^i = |S_v|^f = 7$, while $\varPhi =$ TR resulted in 4 mode splits, starting with $|S_v|^i = 1$ modes and ending with $|S_v|^f = 5$, and longer verification time because of refinements. On the other hand, in QNN-S3, $\varPhi =$ TR resulted in Nref$=5$, $|S_v|^f = 6$, and Tt$=12.7$ min while $\varPhi =$T resulted in Nref$=4$, $|S_v|^f = 11$, and Tt$=16.88$ min. Observation 5: Complicated dynamics require more verification time Different vehicle dynamics affect the number of refinements performed and consequently the verification time (e.g. QNN-S2, QNN-S4, CNN-S2, and CNN-S4). The car appears to be less stable than the quadrotor leading to longer verification time for the same scenarios. This can also be seen by comparing the results of Tables 1 and 2. The PD controllers lead to more stable dynamics than the NN controllers requiring less total computation time for both agents. More stable dynamics lead to tighter reachsets and fewer refinements.

8 Limitations and Discussions

$\mathsf {SceneChecker}$ allows the choice of modes to be changed from segments to waypoints or sequences of segments as well. The waypoint-defined modes eliminate the need for segments of ${G}$ to have few unique lengths, but only allow $\varPhi =$ T. $\mathsf {SceneChecker}$ splits only one mode per refinement and then repeats the computation from scratch. It has to refine many times in unsafe scenarios until reaching the result $unknown$. We plan to investigate other strategies for eliminating spurious counter-examples and returning valid ones in unsafe cases. In the future, it will be important to address other sources of uncertainty in scene verification such as moving obstacles, interactive agents, and other types of symmetries such as permutation and time scaling. Finally, it will be useful to connect a translator to generate scene files from common road simulation frameworks such as CARLA [32], commonroad [33], and Scenic [34].