NeuralNetControlBarrier

Neural Networks (NNs) have been successfully employed to represent the state evolution of complex dynamical systems. Such models, referred to as NN dynamic models (NNDMs), use iterative noisy predictions of NN to estimate a distribution of system trajectories over time. Despite their accuracy, safety analysis of NNDMs is known to be a challenging problem and remains largely unexplored. To address this issue, in this paper, we introduce a method of providing safety guarantees for NNDMs. The paper (Neurips 2022), titled: "Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions", can be found on ArXiv.

Purpose of this code

This code generates stochastic barrier functions and controllers for NNDMs, in accordance with the paper.
Five case studies are included:

1. Pendulum 2D
2. Cartpole 4D
3. Husky 4D
4. Husky 5D
5. Acrobot 6D

Repeat Experiments

Linux	Mac OS X	Windows

Read the description below for repeatability of all the experiments.

Docker Image

The Dockerfile is provided in the main folder. Build this docker file to obtain all the required Julia and Mosek packages, as specified in the Project.toml. To build the docker image, navigate into the main folder and run the following command

docker build -t neurips_nn_barrier .

To start a container

docker run -it --name NNBarrierContainer neurips_nn_barrier

DO NOT BUILD THE DOCKERFILE BEFORE OBTAINING THE REQUIRED MOSEK LICENSE!

EXTERNAL: Mosek

Notice, to run the optimizations, a Mosek license is required! Visit https://www.mosek.com to download this license. After downloading, move mosek.lic from the mosek folder into the licenseFile folder.

Run through bash

Use the following commands to run the optimization case studies through bash.

runOptimization pendulum   # To run Pendulum
runOptimization cartpole   # To run Cartpole
runOptimization husky4d    # To run Husky 4D
runOptimization husky5d    # To run Husky 5D
runOptimization acrobot    # To run Acrobot

Run through Julia

Use the following commands to run the optimization case studies through Julia

Navigate to /NeuralNetControlBarrier.jl
In terminal call julia and run the following commands:

1.    using Pkg

2.    Pkg.activate(".") 

To run the Pendulum experiment for example, use the following command:

   include("Optimization/verification_pendulum")

The same command can be run for the Cartpole and Husky by changing the system's name accordingly after verification_

Change experiment setup for each case study

Navigate to the src folder inside NeuralNetControlBarrier.jl and open Systems.jl.
For each system, change the number of hypercubes by adjusting number_hypercubes. Table 1 in the paper includes the possible number of hypercubes for each system.

Contributing

All contributions welcome! All content in this repository is licensed under the MIT license.

Citing

If the package NeuralNetControlBarrier.jl is useful in your research, and you would like to acknowledge it, please cite this paper:

@article{mazouz2022nncbf,
  author  = {Rayan Mazouz, Karan Muvvala, Akash Ratheesh, Luca Laurenti and Morteza Lahijanian},
  title   = {Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions},
  year    = {2022},
  url     = {https://arxiv.org/abs/2206.07811}
}