Examples and Performance Evaluation¶

Getting started: Simple Automatic Emergency Braking¶

scenario graph — An illustration of Automatic Emergency Braking System¶

Consider the example an AEB as shown above: Cars 1 and 2 are cruising down the highway with zero relative velocity and certain initial relative separation; Car 1 suddenly switches to a braking mode and starts slowing down according, certain amount of time elapses, before Car 2 switches to a braking mode. We are interested to analyze the severity (relative velocity) of any possible collisions.

Safety Verification of the AEB System¶

The black-box of the vehicle dynamics is described in The Autonomous Vehicle Benchmark, and the transition graph of the above AEB is shown in Transition Graph. The unsafe region is that the relative distance between the two cars are too close ( $|sy_1-sy_2|<3$ ). The input files describing the hybrid system is shown in Input Format.

Verification Result of the AEB System¶

Run DryVR’s verification algorithm for the AEB system:

python main.py input/daginput/input_brake.json

The system is checked to be safe. We can also plot the reachtubes for different variables. For example, the reachtubes for the position of Car1 and Car2 along the road the direction are shown below. From the reachtube we can also clearly see that the relative distance between the two cars are never too small.

The Autonomous Vehicle Benchmark¶

The hybrid system for a scenario is constructed by putting together several individual vehicles. The higher-level decisions (paths) followed by the vehicles are captured by the transition graphs discussed in Transition Graph.

Each vehicle has the following modes

Const: move forward at constant speed,
Acc1: constant acceleration,
Brk or Dec: constant (slow) deceleration,
TurnLeft and TurnRight: the acceleration and steering are controlled in such a manner that the vehicle switches to its left (resp. right) lane in a certain amount of time.

The mode for the entire system consists of n vehicles are the mode of each vehicle separated by semicolon. For example, Const;Brk means the first car is in the const speed mode, while the second car is in the brake mode. For each vehicle, we mainly analyze four variables: absolute position ( $sx$ ) and velocity ( $vx$ ) orthogonal to the road direction ( $x$ -axis), and absolute position ( $sy$ ) and velocity ( $vy$ ) along the road direction ( $y$ -axis). The throttle and steering is captured using the four variables.

Verification Examples¶

DryVR now comes with more than two dozen interesting examples, including

6 mixed-signal circuit models with hundreds of nonlinear terms in the dynamics and both time and state dependent transitions
6 high dimensional linear system models (up to 384 dimensions)derived from fields such as civil engineering and robotics
an 8-dimensional hybrid vehicle lane switch model modeling a vehicle switches its lane on highway if it get too close to another vehicle in front of it
a set of standard 2-7 dimensional benchmarks

The simulators for these models are also available in the folder “examples” under the root directory, and the input files are in the folder “input/daginput” and “input/nondaginput”.

Verification Peformance Evaluation¶

We have measured performance for examples come with DryVR 2.0. Peformance is measured using computer with i7 6600u, 16gb ram, Ubuntu 16.04 OS.

Model	Dimension	Time for 1 simulation	Total Time	Flow* time
Biological model I	7	0.01s	0.04s	66.4s
Biological model II	7	0.01s	0.04s	223.4s
Coupled Vanderpol	4	0.03s	0.14s	1038.3s
Spring pendulum	4	0.05s	0.16s	1377.5s
Roessler	3	0.02s	0.36s	17.1s
Lorentz system	3	0.34s	1.07s	316.7s
Lac operon	2	0.47s	171.35s	44.2s
Lotka-Volterra	2	0.02s	0.10s	3.9s
Buckling column	2	0.04s	0.43s	26.4s
Jet engine	2	0.07s	12.1s	6.8s
Brusselator	2	0.10s	3.02s	5.2s
Vanderpol	2	0.05s	2.92s	6.4s
Vehicle platoon 3	9	0.32s	4.28s	21.08s
Uniform nor sigmoid	3	120.91s	1314.22s	Exception
Uniform inverter loop	2	10.94s	278.56s	Exception
Uniform inverter sigmoid	2	24.87s	246.76s	Exception
Uniform nor ramp	3	173.77s	1765.55s	Exception
Uniform or ramp	4	176.70s	1778.87s	Exception
Uniform or sigmoid	4	168.75s	2186.00s	Exception
Clamped beam	348	540.80s	5717.63s	Time out
Building model	48	3.28s	20.24s	Time out
Partial differential equation	20	12.05s	41.21s	Time out
FOM	20	12.18s	40.9s	Time out
Motor control system	8	5.22s	17.89s	Time out
International space station	25	79.99s	243.60s	Time out
Lane switch	8	0.29s	563.52s	N/A

Synthesis Examples¶

We provide 6 controller synthesis benchmarks examples, including:

A vehicle collision avoidance model where a car driving on the highway is asked to avoid an obstacle in front of it.
Robot find a path in a maze.
Motion planning from synthesis tool Pessoa with specification similar to Example 2.
DC motor where the velocity of a DC motor needs to be regulated.
Room heating where the task is to control the temperature of 3 rooms and keep them around 21.
Inverted pendulum as a classical reach-avoid problem.

Synthesis Performance Evaluation¶

Peformance is measured using computer with i7 6600u, 16gb ram, Ubuntu 16.04 OS. Note the running time for graph search can be very different since the alogirthm is randomly search for the graph. It may also return nothing as well. Try to run algorithm multiple times if it does not return the graph.

Example	Dimension	Time horizon	Min staying time	Running Time
vehicle collision avoidance	4	50.0s	2.0s	1896.26s
robot in maze	4	10.0s	1.0s	98.93s
motion plan	3	6.0s	1.0s	4.55s
DC motor	2	1.0s	0.1s	0.35s
room heating	3	25.0s	2.0s	2.66s
inverted pendulum	2	2.0s	0.2s	6.06s