text:
Barcelona Smash Sports Wage Record as Average First Team Player Salary Soars Over £10m
Big-spending Barcelona have become the first sports club in history to pay an average first team wage of over £10m.
With the likes of Lionel Messi, Philippe Coutinho and Luis Suárez on the books, Barça have had to invest heavily in player wages. As transfer fees continue to spiral upwards with the thought of signing a top quality player for less than £50m becoming unthinkable, wages have also inflated considerably.
According to the Daily Mail, the Catalan giants are currently spending an average of £10.4m per player, which doesn't include additional fees that are paid for goals scored, clean sheets and appearances.
The research carried out by the Global Sports Salaries Survey put Barcelona top of list made up of 349 sports teams spread across 13 countries.
Real Madrid come second in the list, with Serie A giants Juventus tenth. The rest of the top ten is occupied by basketball teams from the NBA. This is the highest paying sports league in the world, followed by cricket's Indian Premier League. The Premier League tops the football chart, with an average of £2.9m paid in first team wages per player.
The English top tier sees Manchester United top the wage charts, followed by Manchester City, Chelsea, and Liverpool.
With Financial Fair Play looming over a number of sides, and having already landed Serie A side AC Milan in hot water, it remains to be seen whether football's mega spending can remain sustainable.
In other news, Barcelona manager Ernesto Valverde claimed that his side lacked 'offensive spark' in their dramatic 1-1 La Liga draw with Atlético Madrid.
The reigning champions left it late to salvage a draw against their fellow title challengers, with Ousmane Dembélé pulling his side level after a frustrating evening in the Spanish capital.


text:
MINEOLA, N.Y. – Nassau County District Attorney Madeline Singas announced that two men were arraigned on grand jury indictment charges for the murder of a 30-year old man in Hempstead on October 19, 2018.
Jamik Cannon, 26, of Hempstead, and Brian Marshall-Gibson, 23, of South Floral Park, were indicted on charges of:
Murder in the Second Degree (an A-I felony)
Attempted Murder in the Second Degree (a B violent felony)
Assault in the First Degree (a B violent felony)
Two counts each of Criminal Possession of a Weapon in the Second Degree (a C violent felony)
Cannon, who was arraigned on January 9, was remanded by Judge Robert Schwartz and is due back in court on January 28. Marshall-Gibson, who was arraigned on January 15, was remanded by Judge Schwartz and is due back in court on January 28. If convicted of the top count, the defendants face a maximum sentence of 25 years to life in prison.
"The victim and his friend were simply standing outside in broad daylight when the defendants allegedly approached with two guns and mercilessly shot them," DA Singas said. "The scourge of gun violence has impacted too many families in Nassau County and my office is committed to removing illegal guns from our streets."
DA Singas said that on October 19, 2018, at approximately 10:54 a.m., victim Demetrius Winfield, was with a friend, a local cab driver on break, in front of a home on Wellesley Street in Hempstead. Winfield and his friend were then allegedly shot by Cannon and Marshall-Gibson.
Winfield was shot in the face, chest and groin and was pronounced dead shortly afterwards at Winthrop Hospital. The second man was shot in the leg and is recovering.
Cannon and Winfield were known to each other and had gotten into a disagreement several days earlier at a gas station.
Cannon and Marshall-Gibson were arrested by members of the Nassau County Police Department on December 11.
Senior Assistant District Attorney Ania Pulaski of DA Singas' Major Offense Bureau is prosecuting this case. Cannon is represented by Dennis Lemke, Esq. and Marshall-Gibson is represented by Dana Grossblatt, Esq.
⇐Previous Uniondale Man Arrested for Starving Dog to Death and Feeding a Puppy in a Cruel and Dangerous MannerNext⇒ Three Suspected MS-13 Members Plead Guilty to Attempted Murder in Hempstead Lake State Park Attack

redpajama_set_name: RedPajamaCommonCrawl


text:
Stay at selected version (GB)
CD16/CD32 antibodies, mouse
Clone REA377 recognizes a shared epitope common to the human CD16 and CD32 antigens. CD16 and CD32 are also known as FcγIII and FcγII, respectively, and bind to epitopes located in the constant region domain of IgG. CD16 and CD32 are predominantly expressed on cells of hematopoietic lineages, including B cells, monocytes, NK cells, granulocytes, and dendritic cells. They are also found on hematopoietic progenitor cells, where they appear to play a role in T and B cell development.
Fc-gamma-RIIB, FCGR3, FcRIII, FcR-10, Fc-gamma RII, FcRII, Ly-17
Antigen: CD16/CD32
Alternative names of antigen: Fc-gamma-RIIB, FCGR3, FcRIII, FcR-10, Fc-gamma RII, FcRII, Ly-17
Entrez Gene ID: 14131, 14130
Molecular mass of antigen [kDa]: 26; 33
Distribution of antigen: B cells, monocytes, NK cells, granulocytes, dendritic cells
Available conjugates: PE
Splenocytes from C57BL/6 mice were stained with CD16/CD32 antibodies or with the corresponding REA Control antibodies (left images) and analyzed by flow cytometry using the MACSQuant
de Andrés, B. et al. (1997) Fc gammaRII (CD32) is linked to apoptotic pathways in murine granulocyte precursors and mature eosinophils. Blood 90(3): 1267-1274
de Andrés, B. et al. (1998) A regulatory role for Fcgamma receptors CD16 and CD32 in the development of murine B cells. Blood 92(8): 2823-2829
Zhang, D. et al. (2014) CD16 inhibition increases host survival in a murine model of severe sepsis. J. Surg. Res. 187(2): 605-609
CD16/CD32-PE, mouse
30 µg in 200 µL (1)
cells in a final volume of 100 µL.
150 µg in 1 mL (1)


text:
\section{Introduction}
Autonomous driving systems (ADS)
are expected to bring forth an efficient and safe road traffic.
With the great success of artificial intelligence (AI), such autonomous driving systems are designed and equipped with various  components, taking various sensor inputs and performing perception and prediction tasks. Thus, the safety guarantee of such AI enabled autonomous driving systems is a key challenge.

In order to test autonomous vehicles in real-world scenarios, tremendous resources are required to build scenes and simulate real traffics, so it is unacceptable to thoroughly test an ADS in the real world. The development of driving simulators such as CARLA~\cite{CARLA} and BeamNG~\cite{BeamNG} dramatically reduces the testing cost by introducing a virtual simulated environment. Based on the simulator, a variety of testing approaches have been developed to generating test cases and analysing different traffic scenes \cite{fremont2019scenic}.
However, even that many unsafe testing cases have been found by these approaches, such testing approaches provide almost no safety guarantee to the ADS.

Search-based testing approaches~\cite{AbdessalemNBS18, ArcainiZI21, calo2020generating, borg2021digital, gambi2019automatically, gambi2019asfault, tian2022mosat, haq2022efficient} try to find the parameters that make the ADS misbehave in the corresponding testing scenarios. These approaches often use a fitness function, e.g. time-to-collision~\cite{timetocollision}, to guide the search process.
In our work, we adopt this idea of  fitness functions to specify safety properties. At the same time, inspired by the previous work on linear model learning from a deep neural network~\cite{deeppac}, we propose an algorithm to learn a  fully connected neural network (FNN) model to approximating the fitness function.
Different from testing based approaches, the learned FNN can be proven to be probably approximately correct (PAC), which cannot be achieved by prior ADS testing methods.

In this paper, we focus on the formal verification for the safety properties of the ADS.
In contrast to testing, formal verification aims to give a mathematical proof to a given property of the system with the system formally modeled and the property formally specified.
An ADS can be modeled as a neural network controlled system (NNCS).
The safety verification of NNCS based on reachability analysis has been studied in previous works using activation function reduction~\cite{ivanov2019verisig}, abstract interpretation~\cite{tran2020nnv} and function approximation~\cite{ivanov2020verifying, ivanov2021verisig, huang2019reachnn, fan2020reachnn, huang2022polar}.
These white-box methods over-approximate the behaviour of neural networks using Tyler model arithmetic or abstract interpretation, and are too inefficient for large systems like ADS. Unlike the reachability analysis, our approach gives quantified certificate of safety properties instead, in a much more efficient way and a black-box manner that is more general.

In particular, in our work we verify the safety property of a given ADS, under various traffic scenarios, with a probabilistic guarantee. For example, with $99.9\%$ confidence, the ADS is collision-free with probability at least $99\%$ in the emergency braking scenario. A traffic scenario can comprise parameters such as vehicle velocity, weather, etc.
We are interested in whether the ADS can navigate safely in the traffic scenario with a wide range of parameters.

The idea behind our approach is to learn a surrogate model that approximates the fitness function of the original ADS with a measurable difference gap. If the surrogate model is proved to be safe in a traffic scenario, we can then derive a probabilistic guarantee on the safety property for the ADS in the same scenario.
If the surrogate model fails to meet the safety property, we further explore its parameter space, by dividing whole space into cells according to specified parameters and analysing the quantified level of safety in each of these cells. Therefore, our verification framework is quantitative in the formal specification of safety properties,  the learned surrogate model with its probabilistic guarantee, and the further analysis of safe/unsafe regions.

\commentout{
The surrogate model in our framework is a feed-foward neural network (FNN) that uses the parameters in a traffic scenario as input and approximates the decisions made by the ADS. The criterion quantification is a metric that indicates the level of safeness on a given criterion. To learn a good enough model, we design our step-wise learning procedure which train the model iteratively with both random samples and local extremes. The local extremes are parameters that can predict minimal or maximal quantification with the prior model. Here, we follow the intuition that the extremes are more likely to produce inaccurate predictions. We accumulate the training samples generated by all prior training steps and re-train the new model.

After we learn the surrogate model, we can estimate the absolute difference between the prediction of the surrogate model and the ground-truth quantification with a probabilistic guarantee. The estimation is achieved by calculating the maximal absolute difference considering only a finite subset of all possible parameters. The scenario optimization techniques allow us to give a probabilistic guarantee on such estimation. We then verify whether the quantification predicted by the surrogate model meets the safety criterion, taking into account the absolute difference estimated.
If the surrogate model can be verified, we can conclude a probabilistic guarantee on the safety of the ADS regarding to the traffic scenario.
If the surrogate model fails the safety criterion, we can also analyse it to give a insight on the dangerous parameter region. We first can divide the value of each parameter into two subsets. The safe set contains the parameter value where any quantification predicted meet the safe criterion regardless of other parameters, and the violating set contains the rest. It is clear that we can use such divisions to over-approximate the dangerous parameter region. Besides, the inner-approximations of the dangerous parameter region can be achieved by cover the unsafe neighbourhood around the unsafe parameters found in both learning phase and verification phase. Both the inner and the outer approximations can be used to help further development of the ADS.
}

In summary, the contributions in this paper are at least three fold.

\begin{itemize}
    \item We purpose a practical verification framework for the scenario specific safety of an autonomous driving system with probabilistic guarantee, based on surrogate model learning.
    \item
    When the verification fails, we can further conduct a quantitative analysis on the parameters of interest, and partition the parameter space into
    safe and potentially unsafe regions for the surrogate model. The analysis results are essential for improving the ADS
    \item We apply the developed verification approach and parameter space exploration method to the state-of-the-art ADS
    with five traffic scenarios in CARLA. The results confirm that the learning-based verification is a promising future direction for ADS.
\end{itemize}

\section{Background}
\label{sect:background}

\subsection{Autonomous driving systems}
\label{subsect:criteria}
An autonomous driving system is designed to assist or even replace the human drivers in real traffic. By the degree of automation, ADS can be categorized into six levels, i.e. from L0 to L5\commentout{~\cite{SAEstandard}}. The desired L5 ADS can perform all actions required for all possible traffic scenarios without any help or human interactions.
A modern ADS receives the data from various sensors and generates the control signals using underlying models. A typical ADS we study has an architecture consisting sensors, perception module, prediction module, planning module and control module.

The autonomy of a vehicle must not compromise the on-road safety. In Table~\ref{tab:common_safe_criterion}, there are examples of requirements for guaranteeing that an ADS navigates safely under different traffic scenarios, in which we mainly focus on the collision free property in this paper.

\begin{table}[h]
\renewcommand{\arraystretch}{1.2}
\caption{Common Safety Properties for ADS}
\centering
\def\rule{0pt}{1.2\normalbaselineskip}{\rule{0pt}{1.2\normalbaselineskip}}
\begin{tabularx}{0.49\textwidth}{lX}
\hline
Safety Properties  & Description                                                                                \\ \hline \rule{0pt}{1.2\normalbaselineskip}
Collision Free   & The most critical requirement for ADS is not to collide with other vehicles, etc. This property evaluates the general safety of an ADS by judging whether a collision is occurred.                                                                               \\ \rule{0pt}{1.2\normalbaselineskip}
Route Completion & The functionality of an ADS can be measured with its ability to navigate and control the vehicle moving from one location to another. This property is designed to guarantee the percentage of the route completed by a vehicle with ADS.                        \\ \rule{0pt}{1.2\normalbaselineskip}
Traffic Lights   & Running the red light is one of the typical traffic misbehaviour. This property monitors whether the developed ADS can detect and follow the traffic lights correctly under diverse conditions.                                                                   \\ \rule{0pt}{1.2\normalbaselineskip}
Vehicle Speed    & There can be speed limits for different roads. This property requires the autonomous vehicle keep its speed in a reasonable range.                                                                                \\ \rule{0pt}{1.2\normalbaselineskip}
Lane Keeping     & To maintain the stability of an autonomous driving system, the car should always drive in traffic lanes as long as there is no overtaking or lane changing actions in progress. The ADS fails this property if the car ran over the lane where it should follow. \\ \hline
\end{tabularx}
\label{tab:common_safe_criterion}
\end{table}

\subsection{CARLA \& Scenairo Runner}
We use the high-fidelity simulator CARLA to generate the traffic scenarios. CARLA is based on Unreal Engine 4\commentout{~\cite{unrealengine}}, and it supports the real-time simulation of sensors, dynamic physics and traffic environments. It also provides an extensive library of traffic blueprints including pedestrians, vehicles and street signs, etc. Many modern autonomous driving systems, e.g. Transfuser~\cite{Transfuser} and LAV~\cite{LAV}
, are developed with the CARLA simulator.

In this paper, the Scenario Runner is used to build common traffic scenarios in the simulator.
 Scenario Runner is a tool provided by CARLA to build traffic scenarios. The logic of a scenario is encoded into a behaviour tree, which is composed of non-leaf control nodes (Select, Sequence and Parallel) and leaf nodes (behaviours). A scenario is then executed following the state of its behaviour tree.
\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=0.75\linewidth]{figures/ADSmodel.pdf}
    \caption{The simulator $\mathcal{E}$ iteratively generates the next state.}
    \label{fig:ADSmodel}
\end{figure}

\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=1\linewidth]{figures/scen1.pdf}
    \caption{In this scenario, the ego vehicle drives along the road while the leading NPC vehicle brakes. Parameters are NPC agent speed $\theta_1$, the deceleration $\theta_2$, and the distance $\theta_3$ between two vehicles.
    The behaviour model of the ego vehicle is its ADS, and the behaviour model $\psi_{\mathsf{NPC}_1}$ decelerates the NPC.  A function $\omega$ measures the distance between the ego vehicle and the leading NPC. The safety property is to guarantee the safe distance of $\tau = 0.1$(m) between two vehicles.

    }

    \label{fig:example}
\end{figure}

\section{Scenario driven safety verification}
\label{sec:verification}
In this section, we first formalize the autonomous driving scenario (Section \ref{subsec:ads}). Then, we introduce a model learning based verification approach in Section \ref{sec:model_learning}. When the verification cannot conclude the safety property, in Section \ref{sec:parameter_space}, techniques are also proposed to partition the parameter space into safe/unsafe regions.

\subsection{Formalism of the autonomous driving scenario}
\label{subsec:ads}
An autonomous driving scenario comprises an autonomous driving agent $\mathrm{ego}$ and other agents $\mathrm{NPC}_1,\mathrm{NPC}_2,\ldots$ in the (simulator) environment.
Denote by $\Theta=[0,1]^m$ the set of the parameter vector $\theta=(\theta_1,....,\theta_m)$, where each $\theta_i$ is a normalized parameter variable of the scenario.

We use $\mathcal{S}$ to denote the set of states. A state $s_t\in\mathcal{S}$ describes the  status of all agents in the virtual world at step $t$, including locations, speeds, accelerations, etc.
The behaviour of $\mathrm{ego}$ and $\mathrm{NPC}_i$ is modeled by the function $\psi_\mathrm{ego}(s_t)$ and $\psi_{\mathrm{NPC}_i}(s_t)$,
which generate the action $a_{\mathrm{ego},t}$ and $a_{\mathrm{NPC}_i,t}$ at step $t$, respectively.

The simulator $\mathcal{E}$
generates the next state $s_{t+1}$ according to the ego action $a_{\mathrm{ego}, t}$, the NPC actions $a_{\mathrm{NPC}_i,t}$, and the current state $s_t$ (see Figure~\ref{fig:ADSmodel}).
A simulation is a sequence of states $s_0, s_1, \ldots, s_{t_\bot}$ generated by simulator $\mathcal{E}$,
where $s_0$ is the initial state and $s_{t_\bot}$ is the final state satisfying some terminating conditions.
Note that the initial state $s_0$ and the behaviour functions $\psi_\mathrm{ego}$ and $\psi_{\mathrm{NPC}_i}$ are all instantiated and fixed by the parameter $\theta$.
Therefore, the state sequence $s_0,s_1,\ldots,s_{t_{\bot}}$ is uniquely determined by the parameter $\theta$. Namely, each state $s_t$ at step $t$ can be considered as a function $s_t(\theta)$.

\subsubsection*{Safety properties}
\label{subsec:properties}
We are interested in the safety requirement of critical scenarios. In traffic scenarios, many safety properties can be described as a physical quantity (such as velocity, distance, angle, etc) always satisfying a certain threshold during the entire driving process.
In autonomous driving scenarios, we define a function $\omega$ to
measure such physical quantity at a given state, and the safety properties can be defined as follows.
\begin{definition}[Safety Property]
For a given parameter $\theta\in\Theta$, a quantitative measure $\omega: \mathcal{S} \rightarrow \mathbb{R}$ and a threshold $\tau\in \mathbb{R}$,
the state sequence $s_0, s_1, \ldots, s_{t_\bot}$ is safe if:
\begin{equation}\label{eq:criteria_model}
    \forall t\in\{0,1,\ldots,t_\bot\} \; \omega(s_t(\theta)) \ge \tau.
\end{equation}
\end{definition}
For simplicity, we introduce a \emph{fitness function}
$\rho(\theta)=\min_{0\leq i \leq t_\bot}{\omega(s_i(\theta))}$,
and the property can be equivalently rewritten as
$\rho(\theta) \geq \tau$.
For instance, we can use the distance between two vehicles as the quantitative measure $\omega$, and the collision free property requires that the distance is no smaller than a safe threshold $\tau > 0$.

\commentout{Here, with the parameters $\theta=(\theta_i, \theta_{ego}, \theta_S)$ ranging in some parameter space $\Theta$, we can derive a simulation $(s_0, s_1, \ldots, s_t)$ using the behaviour model $\psi_i$, $\psi_{ego}$ and simulator $S$. We can then directly assess the criterion quantification of the simulation with the following criteria model
\begin{equation}
\label{eq:criteria_model}
    \rho(\theta) = \min_{0\leq i \leq t}{\omega(s_i)}
\end{equation}
For a simulation $(s_0, s_1, \ldots, s_t)$, we call it a counter-example if the value of the criteria model~\eqref{eq:criteria_model} is greater than zero regarding its parameter $\theta$, i.e., $\rho(\theta) < \tau$.
Now we formally introduce the AV scenario verification problem:
\begin{quote}
    Given the scenario $s_0$, the behaviour model $\psi(\cdot ;\theta)$, the stop condition $\phi$, the threshold $\tau$ and the simulator $S$, we determine whether the safety property given by the criterion quantification $\omega$ holds, i.e. $\rho(\theta) \geq \tau$ for all $\theta$ in the parameter space $\Theta$.
\end{quote}
}

\commentout{
\begin{example}
    We demonstrate the emergency braking scenario as an example pictured in Figure~\ref{fig:example}. In this scenario, the ego vehicle is driving along the road while the leading NPC vehicle is braking. The parameter $\theta_{ego}$ of the ego vehicle is its initial velocity $\theta_1$. For the NPC agent, the parameters contain the initial velocity $\theta_2$ and the deceleration $\theta_3$. The initial distance $\theta_4$ between two vehicles is the parameter for the simulator.
    The behaviour model $\psi_{ego}$ is the ADS equipped by the ego vehicle. The behaviour model $\psi_1$ of the NPC decelerates it until the vehicle fully stops. The stop condition $\phi$ here judges whether the ego vehicle fully stops or the simulation times out. The quantification function $\omega$ is actually the distance between the ego vehicle and the leading NPC. The criteria model $\rho$ actually calculates the minimal distance between two vehicles in this scenario. Here, the threshold $\tau$ is set to represents the minimal safe distance between vehicles, e.g. $0.2$. We can instantiate an verification problem that checks whether the ADS can keep a safe distance ($\geq 0.2$) in all possible scenarios generated with different parameters.
\end{example}
}

The example in Figure \ref{fig:example} maps these notations above to a driving scenario. The question then is how to verify that an ADS meets the safe requirement in Equation (\ref{eq:criteria_model}), as a scenario can be initialised with all possible parameter values.

\subsection{Surrogate model based verification}
\label{sec:model_learning}

\commentout{
\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=0.8\linewidth]{figures/framework2.eps}
    \caption{The xxxxxx}
    \label{fig:model_learning}
\end{figure}
}
In general, it is intractable to check the safety property since the fitness function $\rho(\theta)$ depends on the behaviour models and the simulator, which cannot be expressed by explicit functions. Moreover, the simulator and the ADS often act in a black-box manner, which will further complicate the analysis.
For verification purpose, we use a surrogate model $f$ (FNN with ReLU activate function in this paper) to approximate the original fitness function. An illustrative example is in Figure \ref{fig:examplemodel} for assisting the following discussion.

Solving the \emph{absolute distance} $\lambda$ between the surrogate model $f$ and the original fitness function $\rho$ can be encoded into an optimization problem:
\begin{equation}
    \label{eq:abs_dis_opt}
    \begin{split}
        & \min\limits_{\lambda \in \mathbb{R}}\lambda\\
        s.t.\;& \|f(\theta) - \rho(\theta)\| \leq \lambda,\;\forall \theta \in \Theta
    \end{split}
\end{equation}
Based on the scenario optimization technique~\cite{scenario_theorem},
we reduce the infinite parameter set $\Theta$ to a finite subset $\Theta_{\mathrm{sample}}$ containing $K$ samples.
\begin{equation}
    \label{eq:scenario_opt}
    \begin{split}
        & \min\limits_{\lambda \in \mathbb{R}}\lambda\\
        s.t.\;& \|f(\theta) - \rho(\theta)\| \leq \lambda,\;\forall \theta \in \Theta_{\mathrm{sample}}
    \end{split}
\end{equation}
As a result, the absolute distance given by Equation~\eqref{eq:scenario_opt} can be guaranteed with an error rate $\epsilon$ and a significance level $\eta$ according to the following lemma.
\begin{lemma}[see \cite{scenario_theorem}]\label{scenariotheorem}
    If \eqref{eq:scenario_opt} is feasible and has a unique optimal solution $\lambda^*$, and
    \begin{equation}
        \label{eq:scenariotheorem}
        \epsilon\geq \frac{2}{K}(\ln\frac{1}{\eta}+1),
    \end{equation}
    where $\epsilon$ and $\eta$ are the pre-defined error rate and the significance level, respectively, then with confidence at least $1-\eta$, the optimal $\lambda^*$ satisfies all the constraints in $\Omega$ but only at most a fraction of probability measure $\epsilon$, i.e., $\mathbb P (\|f(\theta) - \rho(\theta)\| > \lambda^*)\leq \epsilon$.
\end{lemma}

\paragraph{Neural network verification} After we have the absolute distance evaluation $\lambda^*$, one can use existing neural network verification tools like DeepPoly~\cite{deeppoly} and MILP~\cite{sherlock} to determine whether
\begin{equation}
    \label{eq:verify_on_learned_model}
    f(\theta) - \lambda^* \geq \tau, \forall \theta \in \Theta
\end{equation}
where $f(\theta) - \lambda^*$ serves as a probabilistic lower bound of the original model's fitness function $\rho$, and we remind that $\tau$ is the threshold for safety requirements.
Finally, when Equation~\eqref{eq:verify_on_learned_model} holds, the verification returns SAFE, and we can conclude that the autonomous driving system satisfies the safety property with error rate $\epsilon$ and significance level $\eta$:
\begin{equation*}
    \begin{split}
        \mathbb{P}(\rho(\theta)\geq \tau) &\geq \mathbb{P}(\rho(\theta)\geq f(\theta) - \lambda^*)\\
        &\geq \mathbb{P}(\|f(\theta) - \rho(\theta)\| \leq \lambda^*) \geq 1-\epsilon.
    \end{split}
\end{equation*}
In summary, by given enough samples $\Theta_{\mathrm{sample}}$, the verification results on a learned surrogate model $f$ can be transferred to the original fitness function $\rho$ with guarantee.

\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=0.8\linewidth]{figures/model_2.pdf}
    \caption{We plot the value of fitness function $\rho$ and the learned surrogate model $f$ with respect to the initial velocity $\theta_1$ of the NPC vehicle, while fixing other parameters.
    The fitness function $\rho$ is bounded by $f \pm \lambda^*$ with probabilistic guarantee. In this case, there exists initial velocity value that makes the distance lower bound from the surrogate model smaller than threshold $\tau$ (at bottom right corner), which violates Equation~\eqref{eq:verify_on_learned_model}. In other words, the ADS may break the collision free property.}
    \label{fig:examplemodel}
\end{figure}

\paragraph{Surrogate model learning} As mentioned above, we adopt model learning to approximate, with the guarantee in Lemma \ref{scenariotheorem}, the original fitness function.
Here, we present our learning procedure depicted in Algorithm~\ref{algo:model_learning}.
The major part of the algorithm is a while loop, in which the surrogate model is trained iteratively with the parameter set $\hat\Theta$ (and the corresponding simulation outcome).
After each iteration of training, the absolute distance evaluation $\lambda^*$ is calculated (in Line 5),
and the learning procedure terminates when $\lambda^*$ is small enough.
Otherwise, the model is not sufficiently trained,
and new parameters will be added into the parameter set (see Line 9--11) for the next training step.
In addition to the incrementally sampled parameters $\Theta_\mathrm{inc}$,
we further derive the extreme parameters (denoted by $\Theta_\mathrm{ex}$) that potentially deviate far from the fitness function at current step, where the surrogate model has minimum and maximum outputs.
These parameter samples can be generated by using the attack algorithms (such as PGD~\cite{PGD}) with maximization and minimization directions.
Finally, the surrogate model is obtained, as well as the distance $\lambda^*$ from the fitness function guaranteed with the error rate $\epsilon$ and the significance level $\eta$.

\begin{algorithm}[t]
  \caption{Surrogate Model Learning}
  \label{algo:model_learning}
  \begin{flushleft}
    \textbf{INPUT:}\,\, A driving scenario, error rate $\epsilon$, significance level $\eta$ \\
    \textbf{OUTPUT:}\,\, Surrogate model $f$, Absolute distance $\lambda^*$
  \end{flushleft}
  \begin{algorithmic}[1]
    \STATE initialise a surrogate model $f$
    \STATE sample a parameter set $\hat\Theta\subset \Theta$

    \WHILE {\emph{the time threshold is not met }}
        \STATE train $f$ with all $\theta\in\hat{\Theta}$ and  $\rho(\theta)$.

        \STATE $\lambda^* \leftarrow \mbox{the solution of the optimization problem~\eqref{eq:scenario_opt}}$
        \IF {$\lambda^*$ is small enough}
            \STATE \textbf{break}
        \ELSE
            \STATE incrementally sample the parameters $\Theta_\mathrm{inc}\subset\Theta$

            \STATE generate the extreme parameters $\Theta_\mathrm{ex}\subset\Theta$

            \STATE $\hat{\Theta}\leftarrow \hat{\Theta}\cup {\Theta}_{\mathrm{inc}} \cup {\Theta}_{\mathrm{ex}}$
        \ENDIF
    \ENDWHILE
    \RETURN $f$, $\lambda^*$
  \end{algorithmic}
\end{algorithm}

\commentout{
\subsection{Verification}
\label{subsect:verification}
Hereafter, we denote the vector of the parameters as $\theta = (\theta_1, \ldots, \theta_m) \in \Theta$.
Based on the surrogate model $f_n$ with $n$ steps of refinement, we try to verify the criteria on the it if we did not find any counter-examples in previous simulations. We first evaluate the absolute distance between the surrogate model $f_n$ and the criteria model $\rho$, which can be calculated with an optimization problem:
\begin{equation}
    \label{eq:abs_dis_opt}
    \begin{split}
        & \min\limits_{\lambda \in \mathbb{R}}\lambda\\
        s.t.\;& \|f(\theta) - \rho(\theta)\| \leq \lambda,\;\forall \theta \in \Theta
    \end{split}
\end{equation}
However, it is impossible to solve such optimization problem with infinite constraints. We then use the scenario optimization technique~\cite{} to reduce the optimization problem by only considering a subset of the parameters $\Theta_0$ containing $K$ samples according to a probability measure $\mathbb{P}$.
\begin{equation}
    \label{eq:scenario_opt}
    \begin{split}
        & \min\limits_{\lambda \in \mathbb{R}}\lambda\\
        s.t.\;& \|f(\theta) - \rho(\theta)\| \leq \lambda,\;\forall \theta \in \Theta_0
    \end{split}
\end{equation}
The absolute distance given by the scenario optimization can be guaranteed with an error rate $\epsilon$ and a significance level $\eta$ according to the following theorem.
\begin{lemma}[\cite{scenario_theorem}]\label{scenariotheorem}
    If \eqref{eq:scenario_opt} is feasible and has a unique optimal solution $\lambda^*$, and
    \begin{equation}
        \label{eq:scenariotheorem}
        \epsilon\geq \frac{2}{K}(\ln\frac{1}{\eta}+1),
    \end{equation}
    where $\epsilon$ and $\eta$ are the pre-defined error rate and the significance level, respectively, then with confidence at least $1-\eta$, the optimal $\lambda^*$ satisfies all the constraints in $\Omega$ but only at most a fraction of probability measure $\epsilon$, i.e., $\mathbb P (\|f(\theta) - \rho(\theta)\| > \lambda^*)\leq \epsilon$.
\end{lemma}
After we have the absolute distance evaluation $\lambda^*$, we will try to use verifiers like DeepPoly~\cite{} and MILP~\cite{} to determine whether
\begin{equation}
    \label{eq:verify_on_learned_model}
    f(\theta) - \lambda^* \geq \tau, \forall \theta \in \Theta
\end{equation}
Here, we actually evaluate the probabilistic upper bound $f(\theta) + \lambda^*$ of the criteria model $\rho$. We can then infer that the autonomous driving system satisfies the criteria under a PAC guarantee if the equation~\eqref{eq:verify_on_learned_model} holds.
\begin{equation*}
    \begin{split}
        \mathbb{P}(\rho(\theta)\geq \tau) &\geq \mathbb{P}(\rho(\theta)\geq f(\theta) - \lambda^*)\\
        &\geq \mathbb{P}(\|f(\theta) - \rho(\theta)\| \leq \lambda^*) \geq 1-\epsilon
    \end{split}
\end{equation*}
Here, we show that the verification results on a learned surrogate model $f$ can be transferred to the original criteria model $\rho$ under a PAC guarantee with enough samples $\Theta_0$
}

\commentout{
\begin{example}
    By fixing other parameters to some certain values, we plot the value of criteria model $\rho$ and the learned surrogate model $f$ with respect to the initial velocity $\theta_1$ of the ego vehicle in Figure~\ref{fig:examplemodel}. We bound the surrogate model using the estimated absolute distance $\lambda^*$ and draw the boundary with dashed lines. In this case, we can find some parameter value that makes the lower bound of the surrogate model smaller than threshold $\tau$, which violates equation~\ref{eq:verify_on_learned_model}. In other words, the ADS may break the safe distance criteria.
\end{example}
}

\subsection{Parameter space exploration}
\label{sec:parameter_space}
However, since autonomous driving systems are complex combinations of many components and algorithms, it is hard for them to stay safe in the whole parameter space.
When the verification does not return SAFE, it is meaningful to further analyse the relationship between the unsafe behaviour and the parameters, which will provide an important reference for improving the system.
Thus, based on the parameters we care about, which we called \emph{associated parameters}, we divide the parameter space into cells, and in a quantitative way, an indicator $\varrho\in[0,+\infty]$ can be computed to express how unsafe the model is within each cell.

Based on two associated parameters, saying $\theta_1$ and $\theta_2$, we can split the two-dimensional parameter space into a $l$-by-$l$ grid where each square has the same length $\delta=1/l$. Namely, the whole parameter space is divided into $l^2$ cells as $\Theta=\bigcup_{i,j=0,\ldots,l-1} \Theta_{i,j}$ where
\[
\Theta_{i,j}=[i\delta,(i+1)\delta]\times[j\delta,(j+1)\delta]\times[0,1]^{m-2}.
\]
Then, for the cell $\Theta_{i,j}$, we can define the quantitative unsafe indicator $\varrho_{i,j}$ as its minimal value satisfying
\[
\forall \theta \in \Theta_{i,j} \; f(\theta) \ge \tau-\varrho_{i,j}.
\]
Note that the quantified formula can be encoded by linear constraints, so we can compute $\varrho_{i,j}$ by MILP.
Intuitively, each $\tau-\varrho_{i,j}$ indicates the maximal threshold such that the surrogate model is safe with all $\theta\in\Theta_{i,j}$.
So, the region
\[
\Theta_{\mathrm{safe}}=\bigcup_{\varrho_{i,j}=0}\Theta_{i,j}
\]
is exactly an under-approximation of the parameter region that the surrogate is safe, and a larger $\varrho_{i,j}$ implies that the ADS is more prone to unsafe behaviour in such scenario within the corresponding parameter region.
In this work, we  focus on the analysis for two associated parameters since the results can be easily visualised by heat map, but it is straightforward to generalise this analysis to more associated parameters.

\begin{figure*}[!htb]
  \centering
  \subfloat{
    \includegraphics[width=1\linewidth]{figures/scen2.pdf}
  }
  \caption{(ii) \emph{Follow Pedestrian:} In this scenario, the ego car keeps a safe distance with the pedestrian in front.
  (iii) \emph{Through Redlight:} The ego car encounters a NPC car running the red light when crossing the junctions.

  (iv) \emph{Pedestrian Crossing:} A pedestrian crosses the road while the ego car enters the junction.
  (v) \emph{Cut-in with Obstacle:} In this scenario, a NPC car in front of a van tries to cut into the road where the ego car drives along.
  }
  \label{fig:scenarios}
\end{figure*}

\section{Experiments}
\label{sec:experiment}

In this section, we apply the proposed verification in Section \ref{sec:verification} together with the state-of-the-art autonomous driving system LAV \cite{LAV} \footnote{LAV is ranked the 3rd place in the CARLA Learderboard but the first two systems are not publicly available before submission.}. The safety requirement is to assure a safe road distance between the ego agent and the NPCs in various scenarios.

\paragraph*{Setup} Five traffic scenarios in Figure~\ref{fig:example} and Figure~\ref{fig:scenarios} are considered. There are two variants for each scenario at different locations, labelled with ``Case \#1'' and ``Case \#2''.
Besides similar parameters as detailed in Figure~\ref{fig:example}, there are also 8 weather parameters in each scenario, including cloudness, fog density, precipitation, precipitation deposits, sun altitude angle, sun azimuth angle, wetness and wind intensity.
Furthermore, an additional parameter is introduced to control the initial distance between the ego vehicle and the NPC vehicle.
The minimal safe distance between agents is $\tau = 0.1$ for all the scenarios.

The surrogate model is a 3-layer FNN with 100 neurons in each hidden layer.
The error rate $\epsilon$ and the significance level $\eta$ of the surrogate model are $0.01$ and $0.001$ respectively.
The number of the initial learning samples is $900$, and we train the surrogate model in $10$ iterations of refinement by increasing $40$ random samples and $10$ extreme samples after each iteration.
All the experiments are conducted on a server with AMD EYPC 7543 CPU, 128G RAM and 4 Nvidia RTX 3090.

\commentout{
\begin{itemize}
    \item{Emergency Braking:} In this scenario, the ego agent will follow a NPC agent on a straight road. The leading NPC car will perform emergency braking when the distance between it and the ego car is smaller than a threshold. There are 4 parameters in this scenario, the NPC velocity, initial distance between the NPC and the ego car, the threshold distance and the control parameter of the braking.
    \item{Follow Pedestrian:} In this scenario, a pedestrian is spawned in front of the ego car, and will walk along the road if its distance from the ego car is smaller than a threshold. The three parameters in this scenario are the NPC velocity, the initial distance and the threshold distance.
    \item{Through Redlight:} This scenario reproduce a classical scenario that the ego car encounters a NPC car running the red light when crossing the junctions. The NPC car will be spawned when the distance between the ego car and the junction is smaller than a threshold.
    There are three parameters in this scenario, the NPC velocity, the distance between the NPC car and the junction, and the threshold distance.
    \item{Pedestrian Crossing:} This scenario will spawn a pedestrian crossing the road when the ego car entering the junction. The pedestrian will be spawned when the distance between the ego car and the junction is smaller than a threshold. The two parameters in this scenario are the pedestrian velocity and the threshold distance.
    \item{Cut-in with Obstacle:} In this scenario, a NPC car in front of a van tries to cut into the road where the ego car drives along. The NPC performs the cut-in when the distance between it and the ego car is smaller than a threshold. The three parameters in this scenario are the NPC velocity, the initial distance between the ego car and the NPC car, and the threshold distance.
\end{itemize}
}

\subsection{Discovery of ADS glitch}
Before the verification, our framework can help discover functional glitches for the LAV autonomous driving system.
We find that sometimes the absolute distance evaluation $\lambda^*$ between the surrogate model $f$ and the fitness function $\rho$ is very large, for instance in the \emph{Follow Pedestrian} scenario and \emph{Through Redlight } scenario.
Such unusual $\lambda^*$ is an indication of an abnormal ADS behaviour.
By outlier detection and checking the corresponding simulation records, we identify $1$ and $26$ abnormal cases in $3\,000$ runs for the two scenarios, respectively.
These cases expose a functional glitch of the LAV system: \emph{the ego car can randomly halt in the middle of the road for no reason}, resulting in an extremely large distance.

To eliminate the influence of the glitch, we have to discard the abnormal cases. After the surrogate models are retrained, the absolute distance $\lambda^*$ is reduced sharply from $13.4436$ to $0.7087$ in the Follow Pedestrian scenario, and from $12.0283$ to $2.6678$ in the Through Redlight scenario.

\subsection{Safety verification}

We first verify whether the ADS can always keep  a safe distance in the studied scenarios. The results are reported in Table~\ref{tab:verification_results}.
The safe distance threshold $\tau$ is set to $0.1$ for all scenarios.
The verification concludes that one emergency braking scenario and two Follow Pedestrian scenarios (out of ten) are safe.

While the results in Table~\ref{tab:verification_results} indicate that certain scenarios (e.g., when NPCs are in front of the ego vehicle) are more safe than the others (e.g.,  when NPCs intrude from the sides), it is not surprising that there exist road hazards that result in safety violation in the verification, given the rich parameter conditions. This fact confirms the importance of the parameter space exploration phase.

\begin{table}[!htb]
\renewcommand{\arraystretch}{1.2}
\caption{Safety verification results of different scenarios: $\lambda^*$ is the resulting absolute difference. In the ``Counter-example.'' column, the checkmark (\checkmark) means the ADS is safe regarding to the scenario, otherwise an adversarial output of the surrogate model is given.}
\centering
\begin{tabular}{ccccc}
\hline
                       Scenario    & Case & $\lambda^*$ & Counter-example  \\ \hline
\multirow{2}{*}{Emergency Braking}    & \#1 & 6.8699      & 5.4876    \\
                                      & \#2 &                    5.4194      & \checkmark \\ \hline
\multirow{2}{*}{Follow Pedstrain}     & \#1 & 0.7087      & \checkmark \\
                                      & \#2 &                   4.2193      & \checkmark \\ \hline
\multirow{2}{*}{Through Redlight}     & \#1 & 4.6885      & -5.8308   \\
                                      & \#2 &                   2.9944      & -5.0789   \\ \hline
\multirow{2}{*}{Pedestrian Crossing}  & \#1 & 2.6678      & -0.5953    \\
                                      & \#2 &                    2.8866      & -1.7328   \\ \hline
\multirow{2}{*}{Cut-in with Obstacle} & \#1 & 0.4004      & -0.5991    \\
                                      & \#2 &                    0.8790      & 0.0772    \\   \hline
\end{tabular}
\label{tab:verification_results}
\end{table}

\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=0.99\linewidth]{figures/CutInWithObstacle.pdf}
    \caption{By heatmap, the results of parameter space exploration is illustrated for the cut-in scenario \#1. The grid marked with darker color implies the ADS is more likely to violate the safety property with the parameters in it.
    }
    \label{fig:Unsafe_Range_Cutin_With_Obstacle}
\end{figure}

\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=0.9\linewidth]{figures/PedestrianCrossing.pdf}
    \caption{Parameter space exploration is applied on the pedestrian crossing scenarios. The heatmaps show obviously different characteristics for Case~\#1 (with a cyclist) and Case~\#2 (with a walking pedestrian).}
    \label{fig:Unsafe_Range_Pedestrian_Crossing}
\end{figure}

\subsection{ADS behaviour analysis}

In our approach, parameter space exploration  is conducted (see Sect.~\ref{sec:parameter_space}) to analyse the behaviour of LAV, following driving hazards identified via the verification.
For two associated parameters, we divide the range $[0,1]$ evenly into $20$ intervals, and the quantitative indicator $\varrho_{i,j}$ for all parameter cells can be calculated.
Here, we analyse a) the cut-in scenario \#1 with three different parameters and b) the Pedestrian Crossing scenario in two different cases with the same parameters.

\emph{a) }
For the cut-in scenario \#1, we focus on three associated parameters---initial distance, trigger distance, and NPC velocity.
The analysis result is illustrated in Figure~\ref{fig:Unsafe_Range_Cutin_With_Obstacle}.
From the left most figure and the middle figure, it is clear that the ADS is more likely to keep the safe distance of the ego vehicle when the NPC velocity is high and the initial distance and trigger distance are large enough. This is reasonable as a faster NPC car and a longer distance leave more room for the ADS to overtake and make a braking response to avoid collision.

Interestingly, the unsafe indicator values are much larger in the right most figure, and it means that by the two distance parameters alone, the initial distance and the trigger distance, it is unable to reach a safe condition.
In other words, the proper NPC velocity parameter value is required for any safe traffic scenario.

\emph{b) }
Here, we report the quantitative unsafe indicator for two Pedestrian Crossing cases regards the NPC velocity and trigger distance in Figure~\ref{fig:Unsafe_Range_Pedestrian_Crossing}.
In the Pedestrian Crossing scenario \#1, we spawn a cyclist instead of a walking pedestrian, and the trigger distance is larger. It needs to be mentioned that the cyclist are faster (2-3 m/s) than the walking pedestrian (1-2 m/s).

From Figure~\ref{fig:Unsafe_Range_Pedestrian_Crossing}, we can conclude that larger NPC velocity and larger trigger distance make both scenarios safer for the ADS. Bedsides, the smaller unsafe indicator values also imply that the scenario \#1 are even safer than the scenario \#2. These meet the intuition that larger velocity and longer trigger distance can make the ADS more likely to sense the moving pedestrian. It is worth noting that the velocity parameter in first scenario (which is faster) seems less relative to the safety property than in the second scenario, and this captures the different behaviours of a cyclist and walking pedestrian.

\commentout{
\paragraph{End-to-end autonomous driving systems}
In this paper, we evaluate the safety properties of autonomous driving systems. The modern ADS can be classified into two categories, i.e. behaviour cloning~\cite{LAV, LBC, Transfuser} and reinforcement learning~\cite{ToromanoffWM20}. Our approach are compatible with almost all modern ADS since we treat the ADS as a black-box and analyse a surrogate model instead.

\paragraph{Testing methods for ADS}
Search-based testing approaches~\cite{AbdessalemNBS18, ArcainiZI21, calo2020generating, borg2021digital, gambi2019automatically, gambi2019asfault, tian2022mosat, haq2022efficient} tries to find the parameters that make the ADS misbehave in corresponding testing scenarios. These approaches often use a fitness function to guide the search process, e.g. time-to-collision~\cite{timetocollision}.
In our work, we also adopt the idea of the fitness function and learn a FNN model to approximate it.
One critical improvement of our work is the ability to give probabilistic guarantee on the safety criteria, which can not be achieved by prior ADS testing methods.

\paragraph{Reachability analysis of neural network controlled systems}
The safety verification of neural network controlled systems (NNCS) based on reachability analysis are studied in preivous works using activate function reduction~\cite{ivanov2019verisig}, abstract interpretation~\cite{tran2020nnv} and function approximation~\cite{ivanov2020verifying, ivanov2021verisig, huang2019reachnn, fan2020reachnn, huang2022polar}.
These white-box methods over-approximate the behaviour of neural networks using Tyler model arithmetic or abstract interpretation, and are too inefficient for large systems like ADS. Unlike the reachability analysis, our approach gives quantified certificate of safety properties instead, in a much more efficient way.
\cite{chen2021formal} Like Scenic
}

\section{Conclusion and future work}
In this paper, we propose a novel approach to verify the safety property of a given ADS with a probabilistic guarantee.
The safety property is quantified by a fitness function with scenario parameters.  A surrogate model is learned for approximating this fitness function under the traffic scenario, and the safety property verified in the surrogate model can be transferred to the original ADS with specified confidence and error rate.
When the verification fails, the parameter space is partitioned into safe and unsafe regions with quantitative indicators. This parameter space exploration further helps the testing and improvement of autonomous driving under different scenarios. The experiments validate the utility of our approach with promising results and vivid examples.

As for future work, we believe that the verification driven surrogate model learning will be an important direction for AI safety and security in general.
We are also interested in applying the parameter analysis in this work to the ``design space exploration'' of autonomous driving systems.

\bibliographystyle{IEEEtran}

\section{Introduction}
Autonomous driving systems (ADS)
are expected to bring forth an efficient and safe road traffic.
With the great success of artificial intelligence (AI), such autonomous driving systems are designed and equipped with various  components, taking various sensor inputs and performing perception and prediction tasks. Thus, the safety guarantee of such AI enabled autonomous driving systems is a key challenge.

In order to test autonomous vehicles in real-world scenarios, tremendous resources are required to build scenes and simulate real traffics, so it is unacceptable to thoroughly test an ADS in the real world. The development of driving simulators such as CARLA~\cite{CARLA} and BeamNG~\cite{BeamNG} dramatically reduces the testing cost by introducing a virtual simulated environment. Based on the simulator, a variety of testing approaches have been developed to generating test cases and analysing different traffic scenes \cite{fremont2019scenic}.
However, even that many unsafe testing cases have been found by these approaches, such testing approaches provide almost no safety guarantee to the ADS.

Search-based testing approaches~\cite{AbdessalemNBS18, ArcainiZI21, calo2020generating, borg2021digital, gambi2019automatically, gambi2019asfault, tian2022mosat, haq2022efficient} try to find the parameters that make the ADS misbehave in the corresponding testing scenarios. These approaches often use a fitness function, e.g. time-to-collision~\cite{timetocollision}, to guide the search process.
In our work, we adopt this idea of  fitness functions to specify safety properties. At the same time, inspired by the previous work on linear model learning from a deep neural network~\cite{deeppac}, we propose an algorithm to learn a  fully connected neural network (FNN) model to approximating the fitness function.
Different from testing based approaches, the learned FNN can be proven to be probably approximately correct (PAC), which cannot be achieved by prior ADS testing methods.

In this paper, we focus on the formal verification for the safety properties of the ADS.
In contrast to testing, formal verification aims to give a mathematical proof to a given property of the system with the system formally modeled and the property formally specified.
An ADS can be modeled as a neural network controlled system (NNCS).
The safety verification of NNCS based on reachability analysis has been studied in previous works using activation function reduction~\cite{ivanov2019verisig}, abstract interpretation~\cite{tran2020nnv} and function approximation~\cite{ivanov2020verifying, ivanov2021verisig, huang2019reachnn, fan2020reachnn, huang2022polar}.
These white-box methods over-approximate the behaviour of neural networks using Tyler model arithmetic or abstract interpretation, and are too inefficient for large systems like ADS. Unlike the reachability analysis, our approach gives quantified certificate of safety properties instead, in a much more efficient way and a black-box manner that is more general.

In particular, in our work we verify the safety property of a given ADS, under various traffic scenarios, with a probabilistic guarantee. For example, with $99.9\%$ confidence, the ADS is collision-free with probability at least $99\%$ in the emergency braking scenario. A traffic scenario can comprise parameters such as vehicle velocity, weather, etc.
We are interested in whether the ADS can navigate safely in the traffic scenario with a wide range of parameters.

The idea behind our approach is to learn a surrogate model that approximates the fitness function of the original ADS with a measurable difference gap. If the surrogate model is proved to be safe in a traffic scenario, we can then derive a probabilistic guarantee on the safety property for the ADS in the same scenario.
If the surrogate model fails to meet the safety property, we further explore its parameter space, by dividing whole space into cells according to specified parameters and analysing the quantified level of safety in each of these cells. Therefore, our verification framework is quantitative in the formal specification of safety properties,  the learned surrogate model with its probabilistic guarantee, and the further analysis of safe/unsafe regions.

\commentout{
The surrogate model in our framework is a feed-foward neural network (FNN) that uses the parameters in a traffic scenario as input and approximates the decisions made by the ADS. The criterion quantification is a metric that indicates the level of safeness on a given criterion. To learn a good enough model, we design our step-wise learning procedure which train the model iteratively with both random samples and local extremes. The local extremes are parameters that can predict minimal or maximal quantification with the prior model. Here, we follow the intuition that the extremes are more likely to produce inaccurate predictions. We accumulate the training samples generated by all prior training steps and re-train the new model.

After we learn the surrogate model, we can estimate the absolute difference between the prediction of the surrogate model and the ground-truth quantification with a probabilistic guarantee. The estimation is achieved by calculating the maximal absolute difference considering only a finite subset of all possible parameters. The scenario optimization techniques allow us to give a probabilistic guarantee on such estimation. We then verify whether the quantification predicted by the surrogate model meets the safety criterion, taking into account the absolute difference estimated.
If the surrogate model can be verified, we can conclude a probabilistic guarantee on the safety of the ADS regarding to the traffic scenario.
If the surrogate model fails the safety criterion, we can also analyse it to give a insight on the dangerous parameter region. We first can divide the value of each parameter into two subsets. The safe set contains the parameter value where any quantification predicted meet the safe criterion regardless of other parameters, and the violating set contains the rest. It is clear that we can use such divisions to over-approximate the dangerous parameter region. Besides, the inner-approximations of the dangerous parameter region can be achieved by cover the unsafe neighbourhood around the unsafe parameters found in both learning phase and verification phase. Both the inner and the outer approximations can be used to help further development of the ADS.
}

In summary, the contributions in this paper are at least three fold.

\begin{itemize}
    \item We purpose a practical verification framework for the scenario specific safety of an autonomous driving system with probabilistic guarantee, based on surrogate model learning.
    \item
    When the verification fails, we can further conduct a quantitative analysis on the parameters of interest, and partition the parameter space into
    safe and potentially unsafe regions for the surrogate model. The analysis results are essential for improving the ADS
    \item We apply the developed verification approach and parameter space exploration method to the state-of-the-art ADS
    with five traffic scenarios in CARLA. The results confirm that the learning-based verification is a promising future direction for ADS.
\end{itemize}

\section{Background}
\label{sect:background}

\subsection{Autonomous driving systems}
\label{subsect:criteria}
An autonomous driving system is designed to assist or even replace the human drivers in real traffic. By the degree of automation, ADS can be categorized into six levels, i.e. from L0 to L5\commentout{~\cite{SAEstandard}}. The desired L5 ADS can perform all actions required for all possible traffic scenarios without any help or human interactions.
A modern ADS receives the data from various sensors and generates the control signals using underlying models. A typical ADS we study has an architecture consisting sensors, perception module, prediction module, planning module and control module.

The autonomy of a vehicle must not compromise the on-road safety. In Table~\ref{tab:common_safe_criterion}, there are examples of requirements for guaranteeing that an ADS navigates safely under different traffic scenarios, in which we mainly focus on the collision free property in this paper.

\begin{table}[h]
\renewcommand{\arraystretch}{1.2}
\caption{Common Safety Properties for ADS}
\centering
\def\rule{0pt}{1.2\normalbaselineskip}{\rule{0pt}{1.2\normalbaselineskip}}
\begin{tabularx}{0.49\textwidth}{lX}
\hline
Safety Properties  & Description                                                                                \\ \hline \rule{0pt}{1.2\normalbaselineskip}
Collision Free   & The most critical requirement for ADS is not to collide with other vehicles, etc. This property evaluates the general safety of an ADS by judging whether a collision is occurred.                                                                               \\ \rule{0pt}{1.2\normalbaselineskip}
Route Completion & The functionality of an ADS can be measured with its ability to navigate and control the vehicle moving from one location to another. This property is designed to guarantee the percentage of the route completed by a vehicle with ADS.                        \\ \rule{0pt}{1.2\normalbaselineskip}
Traffic Lights   & Running the red light is one of the typical traffic misbehaviour. This property monitors whether the developed ADS can detect and follow the traffic lights correctly under diverse conditions.                                                                   \\ \rule{0pt}{1.2\normalbaselineskip}
Vehicle Speed    & There can be speed limits for different roads. This property requires the autonomous vehicle keep its speed in a reasonable range.                                                                                \\ \rule{0pt}{1.2\normalbaselineskip}
Lane Keeping     & To maintain the stability of an autonomous driving system, the car should always drive in traffic lanes as long as there is no overtaking or lane changing actions in progress. The ADS fails this property if the car ran over the lane where it should follow. \\ \hline
\end{tabularx}
\label{tab:common_safe_criterion}
\end{table}

\subsection{CARLA \& Scenairo Runner}
We use the high-fidelity simulator CARLA to generate the traffic scenarios. CARLA is based on Unreal Engine 4\commentout{~\cite{unrealengine}}, and it supports the real-time simulation of sensors, dynamic physics and traffic environments. It also provides an extensive library of traffic blueprints including pedestrians, vehicles and street signs, etc. Many modern autonomous driving systems, e.g. Transfuser~\cite{Transfuser} and LAV~\cite{LAV}
, are developed with the CARLA simulator.

In this paper, the Scenario Runner is used to build common traffic scenarios in the simulator.
 Scenario Runner is a tool provided by CARLA to build traffic scenarios. The logic of a scenario is encoded into a behaviour tree, which is composed of non-leaf control nodes (Select, Sequence and Parallel) and leaf nodes (behaviours). A scenario is then executed following the state of its behaviour tree.
\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=0.75\linewidth]{figures/ADSmodel.pdf}
    \caption{The simulator $\mathcal{E}$ iteratively generates the next state.}
    \label{fig:ADSmodel}
\end{figure}

\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=1\linewidth]{figures/scen1.pdf}
    \caption{In this scenario, the ego vehicle drives along the road while the leading NPC vehicle brakes. Parameters are NPC agent speed $\theta_1$, the deceleration $\theta_2$, and the distance $\theta_3$ between two vehicles.
    The behaviour model of the ego vehicle is its ADS, and the behaviour model $\psi_{\mathsf{NPC}_1}$ decelerates the NPC.  A function $\omega$ measures the distance between the ego vehicle and the leading NPC. The safety property is to guarantee the safe distance of $\tau = 0.1$(m) between two vehicles.

    }

    \label{fig:example}
\end{figure}

\section{Scenario driven safety verification}
\label{sec:verification}
In this section, we first formalize the autonomous driving scenario (Section \ref{subsec:ads}). Then, we introduce a model learning based verification approach in Section \ref{sec:model_learning}. When the verification cannot conclude the safety property, in Section \ref{sec:parameter_space}, techniques are also proposed to partition the parameter space into safe/unsafe regions.

\subsection{Formalism of the autonomous driving scenario}
\label{subsec:ads}
An autonomous driving scenario comprises an autonomous driving agent $\mathrm{ego}$ and other agents $\mathrm{NPC}_1,\mathrm{NPC}_2,\ldots$ in the (simulator) environment.
Denote by $\Theta=[0,1]^m$ the set of the parameter vector $\theta=(\theta_1,....,\theta_m)$, where each $\theta_i$ is a normalized parameter variable of the scenario.

We use $\mathcal{S}$ to denote the set of states. A state $s_t\in\mathcal{S}$ describes the  status of all agents in the virtual world at step $t$, including locations, speeds, accelerations, etc.
The behaviour of $\mathrm{ego}$ and $\mathrm{NPC}_i$ is modeled by the function $\psi_\mathrm{ego}(s_t)$ and $\psi_{\mathrm{NPC}_i}(s_t)$,
which generate the action $a_{\mathrm{ego},t}$ and $a_{\mathrm{NPC}_i,t}$ at step $t$, respectively.

The simulator $\mathcal{E}$
generates the next state $s_{t+1}$ according to the ego action $a_{\mathrm{ego}, t}$, the NPC actions $a_{\mathrm{NPC}_i,t}$, and the current state $s_t$ (see Figure~\ref{fig:ADSmodel}).
A simulation is a sequence of states $s_0, s_1, \ldots, s_{t_\bot}$ generated by simulator $\mathcal{E}$,
where $s_0$ is the initial state and $s_{t_\bot}$ is the final state satisfying some terminating conditions.
Note that the initial state $s_0$ and the behaviour functions $\psi_\mathrm{ego}$ and $\psi_{\mathrm{NPC}_i}$ are all instantiated and fixed by the parameter $\theta$.
Therefore, the state sequence $s_0,s_1,\ldots,s_{t_{\bot}}$ is uniquely determined by the parameter $\theta$. Namely, each state $s_t$ at step $t$ can be considered as a function $s_t(\theta)$.

\subsubsection*{Safety properties}
\label{subsec:properties}
We are interested in the safety requirement of critical scenarios. In traffic scenarios, many safety properties can be described as a physical quantity (such as velocity, distance, angle, etc) always satisfying a certain threshold during the entire driving process.
In autonomous driving scenarios, we define a function $\omega$ to
measure such physical quantity at a given state, and the safety properties can be defined as follows.
\begin{definition}[Safety Property]
For a given parameter $\theta\in\Theta$, a quantitative measure $\omega: \mathcal{S} \rightarrow \mathbb{R}$ and a threshold $\tau\in \mathbb{R}$,
the state sequence $s_0, s_1, \ldots, s_{t_\bot}$ is safe if:
\begin{equation}\label{eq:criteria_model}
    \forall t\in\{0,1,\ldots,t_\bot\} \; \omega(s_t(\theta)) \ge \tau.
\end{equation}
\end{definition}
For simplicity, we introduce a \emph{fitness function}
$\rho(\theta)=\min_{0\leq i \leq t_\bot}{\omega(s_i(\theta))}$,
and the property can be equivalently rewritten as
$\rho(\theta) \geq \tau$.
For instance, we can use the distance between two vehicles as the quantitative measure $\omega$, and the collision free property requires that the distance is no smaller than a safe threshold $\tau > 0$.

\commentout{Here, with the parameters $\theta=(\theta_i, \theta_{ego}, \theta_S)$ ranging in some parameter space $\Theta$, we can derive a simulation $(s_0, s_1, \ldots, s_t)$ using the behaviour model $\psi_i$, $\psi_{ego}$ and simulator $S$. We can then directly assess the criterion quantification of the simulation with the following criteria model
\begin{equation}
\label{eq:criteria_model}
    \rho(\theta) = \min_{0\leq i \leq t}{\omega(s_i)}
\end{equation}
For a simulation $(s_0, s_1, \ldots, s_t)$, we call it a counter-example if the value of the criteria model~\eqref{eq:criteria_model} is greater than zero regarding its parameter $\theta$, i.e., $\rho(\theta) < \tau$.
Now we formally introduce the AV scenario verification problem:
\begin{quote}
    Given the scenario $s_0$, the behaviour model $\psi(\cdot ;\theta)$, the stop condition $\phi$, the threshold $\tau$ and the simulator $S$, we determine whether the safety property given by the criterion quantification $\omega$ holds, i.e. $\rho(\theta) \geq \tau$ for all $\theta$ in the parameter space $\Theta$.
\end{quote}
}

\commentout{
\begin{example}
    We demonstrate the emergency braking scenario as an example pictured in Figure~\ref{fig:example}. In this scenario, the ego vehicle is driving along the road while the leading NPC vehicle is braking. The parameter $\theta_{ego}$ of the ego vehicle is its initial velocity $\theta_1$. For the NPC agent, the parameters contain the initial velocity $\theta_2$ and the deceleration $\theta_3$. The initial distance $\theta_4$ between two vehicles is the parameter for the simulator.
    The behaviour model $\psi_{ego}$ is the ADS equipped by the ego vehicle. The behaviour model $\psi_1$ of the NPC decelerates it until the vehicle fully stops. The stop condition $\phi$ here judges whether the ego vehicle fully stops or the simulation times out. The quantification function $\omega$ is actually the distance between the ego vehicle and the leading NPC. The criteria model $\rho$ actually calculates the minimal distance between two vehicles in this scenario. Here, the threshold $\tau$ is set to represents the minimal safe distance between vehicles, e.g. $0.2$. We can instantiate an verification problem that checks whether the ADS can keep a safe distance ($\geq 0.2$) in all possible scenarios generated with different parameters.
\end{example}
}

The example in Figure \ref{fig:example} maps these notations above to a driving scenario. The question then is how to verify that an ADS meets the safe requirement in Equation (\ref{eq:criteria_model}), as a scenario can be initialised with all possible parameter values.

\subsection{Surrogate model based verification}
\label{sec:model_learning}

\commentout{
\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=0.8\linewidth]{figures/framework2.eps}
    \caption{The xxxxxx}
    \label{fig:model_learning}
\end{figure}
}
In general, it is intractable to check the safety property since the fitness function $\rho(\theta)$ depends on the behaviour models and the simulator, which cannot be expressed by explicit functions. Moreover, the simulator and the ADS often act in a black-box manner, which will further complicate the analysis.
For verification purpose, we use a surrogate model $f$ (FNN with ReLU activate function in this paper) to approximate the original fitness function. An illustrative example is in Figure \ref{fig:examplemodel} for assisting the following discussion.

Solving the \emph{absolute distance} $\lambda$ between the surrogate model $f$ and the original fitness function $\rho$ can be encoded into an optimization problem:
\begin{equation}
    \label{eq:abs_dis_opt}
    \begin{split}
        & \min\limits_{\lambda \in \mathbb{R}}\lambda\\
        s.t.\;& \|f(\theta) - \rho(\theta)\| \leq \lambda,\;\forall \theta \in \Theta
    \end{split}
\end{equation}
Based on the scenario optimization technique~\cite{scenario_theorem},
we reduce the infinite parameter set $\Theta$ to a finite subset $\Theta_{\mathrm{sample}}$ containing $K$ samples.
\begin{equation}
    \label{eq:scenario_opt}
    \begin{split}
        & \min\limits_{\lambda \in \mathbb{R}}\lambda\\
        s.t.\;& \|f(\theta) - \rho(\theta)\| \leq \lambda,\;\forall \theta \in \Theta_{\mathrm{sample}}
    \end{split}
\end{equation}
As a result, the absolute distance given by Equation~\eqref{eq:scenario_opt} can be guaranteed with an error rate $\epsilon$ and a significance level $\eta$ according to the following lemma.
\begin{lemma}[see \cite{scenario_theorem}]\label{scenariotheorem}
    If \eqref{eq:scenario_opt} is feasible and has a unique optimal solution $\lambda^*$, and
    \begin{equation}
        \label{eq:scenariotheorem}
        \epsilon\geq \frac{2}{K}(\ln\frac{1}{\eta}+1),
    \end{equation}
    where $\epsilon$ and $\eta$ are the pre-defined error rate and the significance level, respectively, then with confidence at least $1-\eta$, the optimal $\lambda^*$ satisfies all the constraints in $\Omega$ but only at most a fraction of probability measure $\epsilon$, i.e., $\mathbb P (\|f(\theta) - \rho(\theta)\| > \lambda^*)\leq \epsilon$.
\end{lemma}

\paragraph{Neural network verification} After we have the absolute distance evaluation $\lambda^*$, one can use existing neural network verification tools like DeepPoly~\cite{deeppoly} and MILP~\cite{sherlock} to determine whether
\begin{equation}
    \label{eq:verify_on_learned_model}
    f(\theta) - \lambda^* \geq \tau, \forall \theta \in \Theta
\end{equation}
where $f(\theta) - \lambda^*$ serves as a probabilistic lower bound of the original model's fitness function $\rho$, and we remind that $\tau$ is the threshold for safety requirements.
Finally, when Equation~\eqref{eq:verify_on_learned_model} holds, the verification returns SAFE, and we can conclude that the autonomous driving system satisfies the safety property with error rate $\epsilon$ and significance level $\eta$:
\begin{equation*}
    \begin{split}
        \mathbb{P}(\rho(\theta)\geq \tau) &\geq \mathbb{P}(\rho(\theta)\geq f(\theta) - \lambda^*)\\
        &\geq \mathbb{P}(\|f(\theta) - \rho(\theta)\| \leq \lambda^*) \geq 1-\epsilon.
    \end{split}
\end{equation*}
In summary, by given enough samples $\Theta_{\mathrm{sample}}$, the verification results on a learned surrogate model $f$ can be transferred to the original fitness function $\rho$ with guarantee.

\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=0.8\linewidth]{figures/model_2.pdf}
    \caption{We plot the value of fitness function $\rho$ and the learned surrogate model $f$ with respect to the initial velocity $\theta_1$ of the NPC vehicle, while fixing other parameters.
    The fitness function $\rho$ is bounded by $f \pm \lambda^*$ with probabilistic guarantee. In this case, there exists initial velocity value that makes the distance lower bound from the surrogate model smaller than threshold $\tau$ (at bottom right corner), which violates Equation~\eqref{eq:verify_on_learned_model}. In other words, the ADS may break the collision free property.}
    \label{fig:examplemodel}
\end{figure}

\paragraph{Surrogate model learning} As mentioned above, we adopt model learning to approximate, with the guarantee in Lemma \ref{scenariotheorem}, the original fitness function.
Here, we present our learning procedure depicted in Algorithm~\ref{algo:model_learning}.
The major part of the algorithm is a while loop, in which the surrogate model is trained iteratively with the parameter set $\hat\Theta$ (and the corresponding simulation outcome).
After each iteration of training, the absolute distance evaluation $\lambda^*$ is calculated (in Line 5),
and the learning procedure terminates when $\lambda^*$ is small enough.
Otherwise, the model is not sufficiently trained,
and new parameters will be added into the parameter set (see Line 9--11) for the next training step.
In addition to the incrementally sampled parameters $\Theta_\mathrm{inc}$,
we further derive the extreme parameters (denoted by $\Theta_\mathrm{ex}$) that potentially deviate far from the fitness function at current step, where the surrogate model has minimum and maximum outputs.
These parameter samples can be generated by using the attack algorithms (such as PGD~\cite{PGD}) with maximization and minimization directions.
Finally, the surrogate model is obtained, as well as the distance $\lambda^*$ from the fitness function guaranteed with the error rate $\epsilon$ and the significance level $\eta$.

\begin{algorithm}[t]
  \caption{Surrogate Model Learning}
  \label{algo:model_learning}
  \begin{flushleft}
    \textbf{INPUT:}\,\, A driving scenario, error rate $\epsilon$, significance level $\eta$ \\
    \textbf{OUTPUT:}\,\, Surrogate model $f$, Absolute distance $\lambda^*$
  \end{flushleft}
  \begin{algorithmic}[1]
    \STATE initialise a surrogate model $f$
    \STATE sample a parameter set $\hat\Theta\subset \Theta$

    \WHILE {\emph{the time threshold is not met }}
        \STATE train $f$ with all $\theta\in\hat{\Theta}$ and  $\rho(\theta)$.

        \STATE $\lambda^* \leftarrow \mbox{the solution of the optimization problem~\eqref{eq:scenario_opt}}$
        \IF {$\lambda^*$ is small enough}
            \STATE \textbf{break}
        \ELSE
            \STATE incrementally sample the parameters $\Theta_\mathrm{inc}\subset\Theta$

            \STATE generate the extreme parameters $\Theta_\mathrm{ex}\subset\Theta$

            \STATE $\hat{\Theta}\leftarrow \hat{\Theta}\cup {\Theta}_{\mathrm{inc}} \cup {\Theta}_{\mathrm{ex}}$
        \ENDIF
    \ENDWHILE
    \RETURN $f$, $\lambda^*$
  \end{algorithmic}
\end{algorithm}

\commentout{
\subsection{Verification}
\label{subsect:verification}
Hereafter, we denote the vector of the parameters as $\theta = (\theta_1, \ldots, \theta_m) \in \Theta$.
Based on the surrogate model $f_n$ with $n$ steps of refinement, we try to verify the criteria on the it if we did not find any counter-examples in previous simulations. We first evaluate the absolute distance between the surrogate model $f_n$ and the criteria model $\rho$, which can be calculated with an optimization problem:
\begin{equation}
    \label{eq:abs_dis_opt}
    \begin{split}
        & \min\limits_{\lambda \in \mathbb{R}}\lambda\\
        s.t.\;& \|f(\theta) - \rho(\theta)\| \leq \lambda,\;\forall \theta \in \Theta
    \end{split}
\end{equation}
However, it is impossible to solve such optimization problem with infinite constraints. We then use the scenario optimization technique~\cite{} to reduce the optimization problem by only considering a subset of the parameters $\Theta_0$ containing $K$ samples according to a probability measure $\mathbb{P}$.
\begin{equation}
    \label{eq:scenario_opt}
    \begin{split}
        & \min\limits_{\lambda \in \mathbb{R}}\lambda\\
        s.t.\;& \|f(\theta) - \rho(\theta)\| \leq \lambda,\;\forall \theta \in \Theta_0
    \end{split}
\end{equation}
The absolute distance given by the scenario optimization can be guaranteed with an error rate $\epsilon$ and a significance level $\eta$ according to the following theorem.
\begin{lemma}[\cite{scenario_theorem}]\label{scenariotheorem}
    If \eqref{eq:scenario_opt} is feasible and has a unique optimal solution $\lambda^*$, and
    \begin{equation}
        \label{eq:scenariotheorem}
        \epsilon\geq \frac{2}{K}(\ln\frac{1}{\eta}+1),
    \end{equation}
    where $\epsilon$ and $\eta$ are the pre-defined error rate and the significance level, respectively, then with confidence at least $1-\eta$, the optimal $\lambda^*$ satisfies all the constraints in $\Omega$ but only at most a fraction of probability measure $\epsilon$, i.e., $\mathbb P (\|f(\theta) - \rho(\theta)\| > \lambda^*)\leq \epsilon$.
\end{lemma}
After we have the absolute distance evaluation $\lambda^*$, we will try to use verifiers like DeepPoly~\cite{} and MILP~\cite{} to determine whether
\begin{equation}
    \label{eq:verify_on_learned_model}
    f(\theta) - \lambda^* \geq \tau, \forall \theta \in \Theta
\end{equation}
Here, we actually evaluate the probabilistic upper bound $f(\theta) + \lambda^*$ of the criteria model $\rho$. We can then infer that the autonomous driving system satisfies the criteria under a PAC guarantee if the equation~\eqref{eq:verify_on_learned_model} holds.
\begin{equation*}
    \begin{split}
        \mathbb{P}(\rho(\theta)\geq \tau) &\geq \mathbb{P}(\rho(\theta)\geq f(\theta) - \lambda^*)\\
        &\geq \mathbb{P}(\|f(\theta) - \rho(\theta)\| \leq \lambda^*) \geq 1-\epsilon
    \end{split}
\end{equation*}
Here, we show that the verification results on a learned surrogate model $f$ can be transferred to the original criteria model $\rho$ under a PAC guarantee with enough samples $\Theta_0$
}

\commentout{
\begin{example}
    By fixing other parameters to some certain values, we plot the value of criteria model $\rho$ and the learned surrogate model $f$ with respect to the initial velocity $\theta_1$ of the ego vehicle in Figure~\ref{fig:examplemodel}. We bound the surrogate model using the estimated absolute distance $\lambda^*$ and draw the boundary with dashed lines. In this case, we can find some parameter value that makes the lower bound of the surrogate model smaller than threshold $\tau$, which violates equation~\ref{eq:verify_on_learned_model}. In other words, the ADS may break the safe distance criteria.
\end{example}
}

\subsection{Parameter space exploration}
\label{sec:parameter_space}
However, since autonomous driving systems are complex combinations of many components and algorithms, it is hard for them to stay safe in the whole parameter space.
When the verification does not return SAFE, it is meaningful to further analyse the relationship between the unsafe behaviour and the parameters, which will provide an important reference for improving the system.
Thus, based on the parameters we care about, which we called \emph{associated parameters}, we divide the parameter space into cells, and in a quantitative way, an indicator $\varrho\in[0,+\infty]$ can be computed to express how unsafe the model is within each cell.

Based on two associated parameters, saying $\theta_1$ and $\theta_2$, we can split the two-dimensional parameter space into a $l$-by-$l$ grid where each square has the same length $\delta=1/l$. Namely, the whole parameter space is divided into $l^2$ cells as $\Theta=\bigcup_{i,j=0,\ldots,l-1} \Theta_{i,j}$ where
\[
\Theta_{i,j}=[i\delta,(i+1)\delta]\times[j\delta,(j+1)\delta]\times[0,1]^{m-2}.
\]
Then, for the cell $\Theta_{i,j}$, we can define the quantitative unsafe indicator $\varrho_{i,j}$ as its minimal value satisfying
\[
\forall \theta \in \Theta_{i,j} \; f(\theta) \ge \tau-\varrho_{i,j}.
\]
Note that the quantified formula can be encoded by linear constraints, so we can compute $\varrho_{i,j}$ by MILP.
Intuitively, each $\tau-\varrho_{i,j}$ indicates the maximal threshold such that the surrogate model is safe with all $\theta\in\Theta_{i,j}$.
So, the region
\[
\Theta_{\mathrm{safe}}=\bigcup_{\varrho_{i,j}=0}\Theta_{i,j}
\]
is exactly an under-approximation of the parameter region that the surrogate is safe, and a larger $\varrho_{i,j}$ implies that the ADS is more prone to unsafe behaviour in such scenario within the corresponding parameter region.
In this work, we  focus on the analysis for two associated parameters since the results can be easily visualised by heat map, but it is straightforward to generalise this analysis to more associated parameters.

\begin{figure*}[!htb]
  \centering
  \subfloat{
    \includegraphics[width=1\linewidth]{figures/scen2.pdf}
  }
  \caption{(ii) \emph{Follow Pedestrian:} In this scenario, the ego car keeps a safe distance with the pedestrian in front.
  (iii) \emph{Through Redlight:} The ego car encounters a NPC car running the red light when crossing the junctions.

  (iv) \emph{Pedestrian Crossing:} A pedestrian crosses the road while the ego car enters the junction.
  (v) \emph{Cut-in with Obstacle:} In this scenario, a NPC car in front of a van tries to cut into the road where the ego car drives along.
  }
  \label{fig:scenarios}
\end{figure*}

\section{Experiments}
\label{sec:experiment}

In this section, we apply the proposed verification in Section \ref{sec:verification} together with the state-of-the-art autonomous driving system LAV \cite{LAV} \footnote{LAV is ranked the 3rd place in the CARLA Learderboard but the first two systems are not publicly available before submission.}. The safety requirement is to assure a safe road distance between the ego agent and the NPCs in various scenarios.

\paragraph*{Setup} Five traffic scenarios in Figure~\ref{fig:example} and Figure~\ref{fig:scenarios} are considered. There are two variants for each scenario at different locations, labelled with ``Case \#1'' and ``Case \#2''.
Besides similar parameters as detailed in Figure~\ref{fig:example}, there are also 8 weather parameters in each scenario, including cloudness, fog density, precipitation, precipitation deposits, sun altitude angle, sun azimuth angle, wetness and wind intensity.
Furthermore, an additional parameter is introduced to control the initial distance between the ego vehicle and the NPC vehicle.
The minimal safe distance between agents is $\tau = 0.1$ for all the scenarios.

The surrogate model is a 3-layer FNN with 100 neurons in each hidden layer.
The error rate $\epsilon$ and the significance level $\eta$ of the surrogate model are $0.01$ and $0.001$ respectively.
The number of the initial learning samples is $900$, and we train the surrogate model in $10$ iterations of refinement by increasing $40$ random samples and $10$ extreme samples after each iteration.
All the experiments are conducted on a server with AMD EYPC 7543 CPU, 128G RAM and 4 Nvidia RTX 3090.

\commentout{
\begin{itemize}
    \item{Emergency Braking:} In this scenario, the ego agent will follow a NPC agent on a straight road. The leading NPC car will perform emergency braking when the distance between it and the ego car is smaller than a threshold. There are 4 parameters in this scenario, the NPC velocity, initial distance between the NPC and the ego car, the threshold distance and the control parameter of the braking.
    \item{Follow Pedestrian:} In this scenario, a pedestrian is spawned in front of the ego car, and will walk along the road if its distance from the ego car is smaller than a threshold. The three parameters in this scenario are the NPC velocity, the initial distance and the threshold distance.
    \item{Through Redlight:} This scenario reproduce a classical scenario that the ego car encounters a NPC car running the red light when crossing the junctions. The NPC car will be spawned when the distance between the ego car and the junction is smaller than a threshold.
    There are three parameters in this scenario, the NPC velocity, the distance between the NPC car and the junction, and the threshold distance.
    \item{Pedestrian Crossing:} This scenario will spawn a pedestrian crossing the road when the ego car entering the junction. The pedestrian will be spawned when the distance between the ego car and the junction is smaller than a threshold. The two parameters in this scenario are the pedestrian velocity and the threshold distance.
    \item{Cut-in with Obstacle:} In this scenario, a NPC car in front of a van tries to cut into the road where the ego car drives along. The NPC performs the cut-in when the distance between it and the ego car is smaller than a threshold. The three parameters in this scenario are the NPC velocity, the initial distance between the ego car and the NPC car, and the threshold distance.
\end{itemize}
}

\subsection{Discovery of ADS glitch}
Before the verification, our framework can help discover functional glitches for the LAV autonomous driving system.
We find that sometimes the absolute distance evaluation $\lambda^*$ between the surrogate model $f$ and the fitness function $\rho$ is very large, for instance in the \emph{Follow Pedestrian} scenario and \emph{Through Redlight } scenario.
Such unusual $\lambda^*$ is an indication of an abnormal ADS behaviour.
By outlier detection and checking the corresponding simulation records, we identify $1$ and $26$ abnormal cases in $3\,000$ runs for the two scenarios, respectively.
These cases expose a functional glitch of the LAV system: \emph{the ego car can randomly halt in the middle of the road for no reason}, resulting in an extremely large distance.

To eliminate the influence of the glitch, we have to discard the abnormal cases. After the surrogate models are retrained, the absolute distance $\lambda^*$ is reduced sharply from $13.4436$ to $0.7087$ in the Follow Pedestrian scenario, and from $12.0283$ to $2.6678$ in the Through Redlight scenario.

\subsection{Safety verification}

We first verify whether the ADS can always keep  a safe distance in the studied scenarios. The results are reported in Table~\ref{tab:verification_results}.
The safe distance threshold $\tau$ is set to $0.1$ for all scenarios.
The verification concludes that one emergency braking scenario and two Follow Pedestrian scenarios (out of ten) are safe.

While the results in Table~\ref{tab:verification_results} indicate that certain scenarios (e.g., when NPCs are in front of the ego vehicle) are more safe than the others (e.g.,  when NPCs intrude from the sides), it is not surprising that there exist road hazards that result in safety violation in the verification, given the rich parameter conditions. This fact confirms the importance of the parameter space exploration phase.

\begin{table}[!htb]
\renewcommand{\arraystretch}{1.2}
\caption{Safety verification results of different scenarios: $\lambda^*$ is the resulting absolute difference. In the ``Counter-example.'' column, the checkmark (\checkmark) means the ADS is safe regarding to the scenario, otherwise an adversarial output of the surrogate model is given.}
\centering
\begin{tabular}{ccccc}
\hline
                       Scenario    & Case & $\lambda^*$ & Counter-example  \\ \hline
\multirow{2}{*}{Emergency Braking}    & \#1 & 6.8699      & 5.4876    \\
                                      & \#2 &                    5.4194      & \checkmark \\ \hline
\multirow{2}{*}{Follow Pedstrain}     & \#1 & 0.7087      & \checkmark \\
                                      & \#2 &                   4.2193      & \checkmark \\ \hline
\multirow{2}{*}{Through Redlight}     & \#1 & 4.6885      & -5.8308   \\
                                      & \#2 &                   2.9944      & -5.0789   \\ \hline
\multirow{2}{*}{Pedestrian Crossing}  & \#1 & 2.6678      & -0.5953    \\
                                      & \#2 &                    2.8866      & -1.7328   \\ \hline
\multirow{2}{*}{Cut-in with Obstacle} & \#1 & 0.4004      & -0.5991    \\
                                      & \#2 &                    0.8790      & 0.0772    \\   \hline
\end{tabular}
\label{tab:verification_results}
\end{table}

\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=0.99\linewidth]{figures/CutInWithObstacle.pdf}
    \caption{By heatmap, the results of parameter space exploration is illustrated for the cut-in scenario \#1. The grid marked with darker color implies the ADS is more likely to violate the safety property with the parameters in it.
    }
    \label{fig:Unsafe_Range_Cutin_With_Obstacle}
\end{figure}

\begin{figure}[t]
    \centering
        \centering
        \includegraphics[width=0.9\linewidth]{figures/PedestrianCrossing.pdf}
    \caption{Parameter space exploration is applied on the pedestrian crossing scenarios. The heatmaps show obviously different characteristics for Case~\#1 (with a cyclist) and Case~\#2 (with a walking pedestrian).}
    \label{fig:Unsafe_Range_Pedestrian_Crossing}
\end{figure}

\subsection{ADS behaviour analysis}

In our approach, parameter space exploration  is conducted (see Sect.~\ref{sec:parameter_space}) to analyse the behaviour of LAV, following driving hazards identified via the verification.
For two associated parameters, we divide the range $[0,1]$ evenly into $20$ intervals, and the quantitative indicator $\varrho_{i,j}$ for all parameter cells can be calculated.
Here, we analyse a) the cut-in scenario \#1 with three different parameters and b) the Pedestrian Crossing scenario in two different cases with the same parameters.

\emph{a) }
For the cut-in scenario \#1, we focus on three associated parameters---initial distance, trigger distance, and NPC velocity.
The analysis result is illustrated in Figure~\ref{fig:Unsafe_Range_Cutin_With_Obstacle}.
From the left most figure and the middle figure, it is clear that the ADS is more likely to keep the safe distance of the ego vehicle when the NPC velocity is high and the initial distance and trigger distance are large enough. This is reasonable as a faster NPC car and a longer distance leave more room for the ADS to overtake and make a braking response to avoid collision.

Interestingly, the unsafe indicator values are much larger in the right most figure, and it means that by the two distance parameters alone, the initial distance and the trigger distance, it is unable to reach a safe condition.
In other words, the proper NPC velocity parameter value is required for any safe traffic scenario.

\emph{b) }
Here, we report the quantitative unsafe indicator for two Pedestrian Crossing cases regards the NPC velocity and trigger distance in Figure~\ref{fig:Unsafe_Range_Pedestrian_Crossing}.
In the Pedestrian Crossing scenario \#1, we spawn a cyclist instead of a walking pedestrian, and the trigger distance is larger. It needs to be mentioned that the cyclist are faster (2-3 m/s) than the walking pedestrian (1-2 m/s).

From Figure~\ref{fig:Unsafe_Range_Pedestrian_Crossing}, we can conclude that larger NPC velocity and larger trigger distance make both scenarios safer for the ADS. Bedsides, the smaller unsafe indicator values also imply that the scenario \#1 are even safer than the scenario \#2. These meet the intuition that larger velocity and longer trigger distance can make the ADS more likely to sense the moving pedestrian. It is worth noting that the velocity parameter in first scenario (which is faster) seems less relative to the safety property than in the second scenario, and this captures the different behaviours of a cyclist and walking pedestrian.

\commentout{
\paragraph{End-to-end autonomous driving systems}
In this paper, we evaluate the safety properties of autonomous driving systems. The modern ADS can be classified into two categories, i.e. behaviour cloning~\cite{LAV, LBC, Transfuser} and reinforcement learning~\cite{ToromanoffWM20}. Our approach are compatible with almost all modern ADS since we treat the ADS as a black-box and analyse a surrogate model instead.

\paragraph{Testing methods for ADS}
Search-based testing approaches~\cite{AbdessalemNBS18, ArcainiZI21, calo2020generating, borg2021digital, gambi2019automatically, gambi2019asfault, tian2022mosat, haq2022efficient} tries to find the parameters that make the ADS misbehave in corresponding testing scenarios. These approaches often use a fitness function to guide the search process, e.g. time-to-collision~\cite{timetocollision}.
In our work, we also adopt the idea of the fitness function and learn a FNN model to approximate it.
One critical improvement of our work is the ability to give probabilistic guarantee on the safety criteria, which can not be achieved by prior ADS testing methods.

\paragraph{Reachability analysis of neural network controlled systems}
The safety verification of neural network controlled systems (NNCS) based on reachability analysis are studied in preivous works using activate function reduction~\cite{ivanov2019verisig}, abstract interpretation~\cite{tran2020nnv} and function approximation~\cite{ivanov2020verifying, ivanov2021verisig, huang2019reachnn, fan2020reachnn, huang2022polar}.
These white-box methods over-approximate the behaviour of neural networks using Tyler model arithmetic or abstract interpretation, and are too inefficient for large systems like ADS. Unlike the reachability analysis, our approach gives quantified certificate of safety properties instead, in a much more efficient way.
\cite{chen2021formal} Like Scenic
}

\section{Conclusion and future work}
In this paper, we propose a novel approach to verify the safety property of a given ADS with a probabilistic guarantee.
The safety property is quantified by a fitness function with scenario parameters.  A surrogate model is learned for approximating this fitness function under the traffic scenario, and the safety property verified in the surrogate model can be transferred to the original ADS with specified confidence and error rate.
When the verification fails, the parameter space is partitioned into safe and unsafe regions with quantitative indicators. This parameter space exploration further helps the testing and improvement of autonomous driving under different scenarios. The experiments validate the utility of our approach with promising results and vivid examples.

As for future work, we believe that the verification driven surrogate model learning will be an important direction for AI safety and security in general.
We are also interested in applying the parameter analysis in this work to the ``design space exploration'' of autonomous driving systems.

\bibliographystyle{IEEEtran}

redpajama_set_name: RedPajamaArXiv


text:
Article entitled "The Imperative of Considering the Concept of Highest and Best Use in Healthcare Valuation," by HCC CEO Robert James Cimasi and HCC President Todd A. Zigrang, was published in NACVA Online Journal
Part 1 of 2 of an article entitled, "The Imperative of Considering the Concept of Highest and Best Use in Healthcare Valuation", by HCC CEO Robert James Cimasi, MHA, ASA, FRICS, MCBA, CVA, CM&AA, and HCC President Todd A. Zigrang, was published on March 26, 2015 in NACVA and the Consultants' Training Institute's QuickRead Newsletter.
The article describes that while traditional valuation methodologies have relied upon the analysis of historical accounting and other data as predictive of future performance and value, this may not hold true with every economy, industry, or even every enterprise within an industry, over time. For example, the turbulent status of the healthcare industry over the last five decades, since the passage of Medicare in the 1960s, has introduced intervening events and circumstances that have had a dramatic effect on the revenue, expense, and subsequent net economic benefit stream of enterprises operating in the healthcare marketplace. Accordingly, the "road map of historical performance" of healthcare related enterprises becomes less predictive of future performance. In this first article, of a two-part series, the authors focus on the various standards of value applicable to healthcare engagement and conclude discussing the highest and best use standard.


A community connecting businesses, financial institutions, and processors!
As part of your ePayResources membership, we have started a new community connecting financial institutions, businesses, and processors.
This networking and informational forum lead by industry experts will provide payments industry updates and a platform to discuss matters affecting your payments business.
Click the link below to read the full press release.
Access to the Payments Forum group within our Connections Member Community to register for each webinar, access resources, and join in discussions!
Nonmembers - Download the member application + forum enrollment packet linked below. To learn more about benefits of membership, click here.
Members - Download the Forum enrollment packet linked below.
Complete the enrollment packet, sign, and send to OpsAdmin@ePayResources.org or fax 214-438-4515.
Wait for the email confirming that you have been added to the Payments Forum group within the Connections Member Community within 2 business days of receipt of your completed packet.
Login to the Connections Member Community and access the Forum group by navigating to Communities - My Communities - Payments Forum.
Register for the Forum Meetings you plan to participate on under the Events section. Reminder, registration for each meeting is required and space is limited.
Click the FAQ document linked below that may help answer many of your questions.
If you have additional questions about the Forum contact Debbie Arai, AAP, Vice President, Third-Party Services, ePayAdvisors, at 1-800-475-0585 ext. 1601, or darai@epayadvisors.com.
If you have membership-related questions, contact our Member & Industry Relations team at 1-800-475-0585, Option 4, or email membership@epayresources.org.