PRoTECT is an open-source software tool, for the parallelized construction of safety barrier certificates (BCs) for nonlinear polynomial systems. This tool aims to verify safety properties for four classes of dynamical systems: (i) discrete-time stochastic systems (dt-SS), (ii) discrete-time deterministic systems (dt-DS), (iii) continuous-time stochastic systems (ct-SS), and (iv) continuous-time deterministic systems (ct-DS). PRoTECT is implemented in Python as an application programming interface (API), offering users the flexibility to interact either through its user-friendly graphic user interface (GUI) or via function calls from other Python programs. PRoTECT leverages parallelism across different barrier degrees to efficiently search for a feasible BC. Additionally, PRoTECT employs sum-of-squares (SOS) optimization programs to systematically search for polynomial-type BCs.
We have provided Youtube tutorial videos to help understand how to use PRoTECT here.
- Artifact Evaluation
- Installation
- Examples
- Related Paper
- Reporting Bugs
- License
- Youtube Videos about PRoTECT
If you are a reviewer for the AE committee, the instructions for how to install and reproduce the results of our paper can be found here. As the tool uses a GUI, we recommend running it on the Virtual Machine provided by the AE Committee that can be found here on Zenodo, the instructions are partially tailored for this VM. Assuming PRoTECT is installed in the home directory then by navigating to the bash-scripts folder you can simply run:
./install_ubuntu22_PRoTECT_and_FOSSIL.sh
to install all necessary dependencies and update the PYTHONPATH, etc. apropriately.
If you choose to use Mosek you will also need a license that can be acquired here (free for academics).
If using Ubuntu, we have provided an installation script that automatically installs all prerequisites and sets up the PYTHONPATH assuming the repository is cloned into the home directory:
cd ~/PRoTECT/bash-scripts
./install_ubuntu22_PRoTECT.sh
It is also easy to install the tool manually. We assume the user has python3 and pip installed on their machine. To install necessary dependencies, run from the directory containing the repository: pip install -r requirements.txt
To use PRoTECT via its GUI, simply navigate a terminal to the current folder and then run python3 main.py. You can import pre-configured examples into the GUI from the folder GUI_config_files by clicking the button Import Config. You can also run the examples for the deterministic and stochastic systems from the respective folders with python3 <example-name>.py (You may also need to temporarily add PRoTECT to your PATH using export PYTHONPATH=/<path-to-PRoTECT>/PRoTECT:$PYTHONPATH before running the examples this way, or permanently add it to your PATH by appending export PYTHONPATH=$PYTHONPATH:/<path-to-PRoTECT>/PRoTECT to the end of the file ~/.profile, or equivalent, and restarting your computer). Helpful information about which files to adjust for your specific machine to edit the PYTHONPATH can be found here.
We have provided some tutorial videos which cover the basics of installation and using PRoTECT which can be found here.
We have also included a Dockerfile which can run the API scripts for PRoTECT with a default solver of CVXOPT, but cannot support the GUI. To build and run this Dockerfile, use the following commands:
docker build -t protect .
docker run --rm -it --name protect protect
You can add the Mosek license into the Docker image by adapting the following command:
docker cp <license-file-on-host-machine> protect:<location-for-license-on-Docker-image>
We present some selected examples graphically to demonstrate some use cases of PRoTECT. All the examples can be found in the folder ex where the deterministic case studies also include the code to run them on the tool FOSSIL for comparison (the models in models.py should be copied into the equivalent FOSSIL file models.py).
In addition configuration files for all of the examples can be imported in the GUI for analysis if desired, these can be found in the folder GUI_config_files.
A continuous-time deterministic system of a 2D jet engine is verified over an infinite-time horizon with the goal of never reaching the red avoid region, see ex2_jet_engine_ct_DS.py.
A continuous-time deterministic system of a 2D Van der Pol oscillator is verified over a finite-time horizon with the goal of not reaching the red avoid region with some confidence, see ex2_van_der_pol_oscillator_dt_SS_uniform.py.
A discrete-time deterministic system of a two-room temperature system that is verified over an infinite time horizon with the goal of never the red avoid region, see ex2_TwoRoomTemp_dt_DS.py.
Two 2D continuous-time deterministic systems with Linear (left) and Nonlinear (right) dynamics are verified over a finite-time horizon with the goal of not reaching the red avoid region with some confidence, see ex2_A1linear_ct_SS.py and ex2_nonlinear_ct_SS.py.
The arXiv version of the paper is located here.
@misc{wooding2024protect,
title={PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems},
author={Ben Wooding and Viacheslav Horbanov and Abolfazl Lavaei},
year={2024},
eprint={2404.14804},
archivePrefix={arXiv},
primaryClass={eess.SY}
}
If you encounter any issues or have feedback, please open an issue in the repository. We appreciate your input and will address it as soon as possible.
This work is licensed under a Creative Commons Attribution 4.0 International License.
