HooVer uses optimistic optimization to solve statistical model checking problems for MDPs. The tool is available at https://github.com/sundw2014/HooVer. For reviewers who want to reproduce the results in the paper, please see https://github.com/sundw2014/HooVer/blob/master/Reproduce.md.
Available Benchmark Scenarios
We have created several example models that capture scenarios involving autonomous vehicles and driving assist systems. More than 25% of all highway accidents are rear-end crashes, of which around 85% happen on single-lane highways. Automatic braking and collision warning systems are becoming standard features, however, testing their safety remains a challenge. We model these features in our scenarios which are illustrated in the following figure.
SLplatoon
SLplatoon models $m$ cars on a single lane. At every step, each car probabilistically decides to “speed up”, “cruise” or “brake” based on its current gap with the predecessor. The probabilistic parameters of the model are derived from data collected from overhead traffic enforcement cameras on roads. The uncertainty in the initial positions (and gaps) arises from perception inaccuracies, which are modeled as worst-case ranges. The initial state space of this model has $m$ dimensions corresponding to the initial positions of the cars. A state is unsafe if there are any two cars that get too close.
In our experiments, we set $m = 4$, and thus the initial state space $\Theta$ is $4$-dimensional. Curves above show the results of HooVer and PlasmaLab. Results are averaged over $10$ runs. Mean and standard deviation are reported. Source code of this model is available from https://github.com/sundw2014/HooVer/blob/master/models/Slplatoon.py
MLplatoon
MLplatoon models $m \times \ell$ cars on $\ell$ lanes. At every step, each car probabilistically chooses to either move forward like a vehicle in SLplatoon, or it changes to its left or right lane. These actions are chosen probabilistically, according to probability distributions that depend on their distances to the vehicles on its current lane, as well as left and right lanes. Then initial set (search space) is $(m \times \ell)$-dimensional. A state is unsafe if any two cars on the same lane get two close.
We have tried two different configurations for this scenario. In the first one, we set $m = 3,\ \ell = 3$, and thus the initial state space $\Theta$ is $9$-dimensional. In order to show the capability of HooVer to handle very large state spaces, we set $m = 9,\ \ell = 2$ ($18$-vehicles in total) in the second configuration, while some of the initial positions of the vehicles are fixed. The resulting $\Theta$ for this configuration is $8$-dimensional. The figure below shows the results of HooVer and PlasmaLab on these two configurations. Results are averaged over $10$ runs. Mean and standard deviation are reported. Source code of this model is available from https://github.com/sundw2014/HooVer/blob/master/models/Mlplatoon.py
DetectBrake
DetectBrake models a car running on a single-lane road and a pedestrian crossing the road in front of the car. The car is equipped with a lidar. Once detecting the pedestrian, the car starts braking. The probability of detecting the pedestrian is a function of the relative pose ($\theta$ and $d$) between the car and the pedestrian. In this benchmark, we model a broken lidar device that somehow cannot detect obstacles in a specific direction. The probability of detecting is given by $p(\theta, d) = \left(1 – \exp\left( \frac{-(\theta – \theta_b)^2}{s} \right)\right) \cdot \left(\max\{0, \frac{d_m – d}{d_m}\}\right)^2$, where $\theta_b$ is a constant angle along which the pedestrians cannot be detected, and $d_m$ is the maximum distance that the lidar can cover, and $s > 0$ is a parameter controlling how fast the probability decreases when approaching $\theta_b$. The detecting probability also declines as the distance increases. This model is almost always safe unless $\theta = \theta_b$ holds constantly for every step. This rarely happens when the velocities and initial positions of the car and the pedestrian satisfy some constraints. This is a more realistic model checking problem in the sense that the system is almost always safe unless it triggers some bugs. The goal of a model checker is to find such rare unsafe cases before deployment.
In our experiments, we set $s = 5 \times 10^{-6}$, and thus the resulting objective function is sharp around the maxima. The figure above shows the results of HooVer and PlasmaLab. Results are averaged over $10$ runs. Mean and standard deviation are reported. Source code of this model is available from https://github.com/sundw2014/HooVer/blob/master/models/DetectingPedestrian.py
Merging
Merging models a car on the ramp trying to merge to the left lane. There are $m$ cars on the left lane. At every step, each car on the left lane behaves exactly the same way as in SLplatoon, and the car on the ramp keeps accelerating with a constant acceleration, and if it is safe to merge, it may do so with a constant probability. The search space is $(m+1)$-dimensional and includes the initial position and the initial velocity of the car on the ramp. A state is unsafe if the car on the ramp runs beyond the end of the ramp or any two cars on the left lane get too close.
In our experiments, we set $m = 3$, and thus the resulting $\Theta$ is $4$-dimensional. The figure above shows the results of HooVer and PlasmaLab. Results are averaged over $10$ runs. Mean and standard deviation are reported. Source code is available from https://github.com/sundw2014/HooVer/blob/master/models/Merging.py