Stochastic reachability toolbox (SReachTools)

SReachTools is a MATLAB toolbox to tackle various problems in stochastic reachability. Currently, the toolbox can perform verification and (open-loop or affine disturbance-feedback) controller synthesis for linear (time-varying/time-invariant) systems with additive (Gaussian/non-Gaussian) disturbance. By verification, we are referring to the problem of stochastic reachability of a target tube. Our project website is at https://sreachtools.github.io.

This is an area of active research, and this toolbox will attempt to cater certain classes of problems.

We aim to support the following problems:

• Stochastic reachability of a target tube (guaranteeing safety for stochastic systems to lying in a collection of time-varying safe sets while satisfying input bounds):
  • This problem subsumes existing work on terminal hitting stochastic reach-avoid problems as well as stochastic viability problems. We implement a dynamic programming solution, limited to 3-dimensional LTI systems using SReachDynProg.
  • Open-loop controller synthesis using SReachPoint (admissible controller satisfying hard control bounds with maximum safety probability):
    • chance-open: Chance constraint formulation solved via linear programming
    • genzps-open: Fourier transforms-based compuation (Genz's algorithm + patternsearch)
    • particle-open: Particle control approach (mixed-integer linear program approach)
    • voronoi-open: Voronoi partition-based undersampled particle control approach (mixed-integer linear program approach)
  • Affine controller synthesis using SReachPoint (admissible controller with chance constrained input bounds with maximum safety probability):
    • chance-affine: Chance constraint formulation solved via difference-of-convex programming (risk allocation and controller synthesis performed simultaneously)
    • chance-affine-uni: Chance constraint formulation solved via bisection for uniform risk allocation and second order cone programs for controller synthesis (risk allocation and controller synthesis performed separately)
  • Stochastic reach set computation using SReachSet (set of initial states from which an admissible controller exists such that the probability of safety is above a given threshold):
    • chance-open: Chance constraint-based under-approximation
    • genzps-open: Fourier transforms-based under-approximation
    • lag-over/lag-under: Lagrangian methods-based over- and under-approximation
• Forward stochastic reachability using SReachFwd (characterizing the stochasticity of the state at a future time of interest):
  • state-stoch/concat-stoch: Stochasticity of the state or the concatenated state vector
  • state-prob/concat-prob: Probability of the state or the concatenated state vector lying in a target set or a tube respectively

Do check our project blog for updates!

Examples

For easy start, we have cataloged in our project webpage a number of relevant, easy-to-follow examples. These are also part of the repository (see examples/*.m).

Further, you can see SReachTools in action at Code Ocean. Check out https://codeocean.com/explore/capsules/?query=SReachTools.

Installation

We will denote MATLAB's command prompt by >>, while the system command prompt by $ .

Dependencies

External dependencies of SReachTools are:

1. MATLAB's Statistics and Machine Learning Toolbox
2. MPT3 (https://www.mpt3.org/)
3. CVX (http://cvxr.com/cvx/)
4. MATLAB's Global Optimization Toolbox (optional)
5. MATLAB's Optimization Toolbox (optional)
6. GeoCalcLib (https://github.com/sreachtools/GeoCalcLib) (optional)
7. GUROBI (optional)
8. MOSEK (optional)

Essential dependencies

These dependencies are platform-independent, and have been tested in Windows, MacOS, and Linux.

1. MATLAB (>2017a) with MATLAB's Statistics and Machine Learning Toolbox
2. MPT3 (https://www.mpt3.org/) --- for polytopic computational geometry
   1. Copy the MATLAB script install_mpt3.m provided by MPT3 from the browser to your local computer.
   2. Download and install MPT3 by running the following command in MATLAB's command prompt (after changing directory to the folder containing install_mpt3.m)

      >> install_mpt3
      

   3. Add cd <PATH-TO-TBXMANAGER>;tbxmanager restorepath to your MATLAB startup script for the MPT3 installation to persist across MATLAB runs.
3. CVX (http://cvxr.com/cvx/) --- for parsing convex and mixed-integer programs. Use the Standard bundles, including Gurobi and/or MOSEK, even if you do not plan to use Gurobi or MOSEK. CVX does not require any additional licenses to work with GUROBI or MOSEK in an academic setting.
   1. Download the zip file from http://cvxr.com/cvx/download/, and extract it to the cvx folder.
   2. Install CVX by running the following command in MATLAB's command prompt (after changing the current working directory to the cvx folder)

      >> cvx_setup
      

   3. Add cd <PATH-TO-CVX>;cvx_setup to your MATLAB startup script for the CVX installation to persist across MATLAB runs.
   4. Other notes:
      • Detailed installation instructions are given in http://cvxr.com/cvx/download/.
      • SDPT3 (the default backend solver of CVX) performs reasonably well with CVX, when compared to MOSEK, and significantly poorly when compared to GUROBI in the tested examples and CVX v2.1 version. See Step 5 for instructions in installing external solvers for SReachTools.

Optional dependencies

These dependencies will allow non-essential features of SReachTools or enable superior performance.

1. MATLAB's Global Optimization Toolbox and Optimization Toolbox
   • Affects genzps-open options in SReachPoint and SReachSet computation.
2. GeoCalcLib --- a MATLAB interface to Avis's LRS vertex-facet enumeration library. In empirical tests, we found LRS to be a superior alternative to MPT's preferred approach for vertex-facet enumeration, CDD.
   • Affects lag-over and lag-under options in SReachSet computation.
   • See https://github.com/sreachtools/GeoCalcLib for detailed installation instructions.
   • :warning: GeoCalcLib currently works only in Unix and MAC OS.
3. External solvers --- GUROBI and/or MOSEK.
   1. Why do we need to install external solvers?
      • Mixed-integer programming enabled by GUROBI or MOSEK is required for particle-based approaches in SReachPoint.
        • Affects voronoi-open and particle-open options in SReachPoint computation.
      • External solvers are typically more numerically robust and computationally faster than free solvers like SDPT3 that come with CVX.
        • Affects overall computation speed and solution quality.
   2. GUROBI (http://www.gurobi.com/): A backend solver for CVX that also enables mixed-integer programming associated with particle-based approaches, apart from convex programming. MPT3 + GUROBI also provides robust polyhedral computation. (:warning: Currently facing issues).
      1. GUROBI offers free academic license, which can be requested at http://www.gurobi.com/registration/download-reg.
      2. MPT3 + GUROBI: Requires the external installation.
         1. Obtain a copy of GUROBI Optimizer from http://www.gurobi.com/ (Requires signing up)
         2. Unzip the installation to desired folder.
         3. Generate the license file by running the following command in the Unix command prompt (after changing the current working directory to the <PATH-TO-GUROBI-HOME>/gurobi902/<OS>/bin/)

            $ grbgetkey OUTPUT_OF_GUROBI_LICENSE_REQUEST
            

         4. Setup GUROBI by running the following command in MATLAB's command prompt (after changing the current working directory to <PATH-TO-GUROBI-HOME>/gurobi902/<OS>/matlab/)

            >> gurobi_setup
            

         5. Add GRB_LICENSE_FILE environment variable that has the location of the gurobi.lic file for MPT3 to detect GUROBI. Alternatively, add the following command in startup.m

            >> setenv('GRB_LICENSE_FILE','/home/ubuntu/gurobi.lic')
            

         6. Update MPT3 with GUROBI by running the following command in MATLAB's command prompt

            >> mpt_init
            

      3. CVX + GUROBI: The current build of CVX v2.2 does not play well with GUROBI v9.0.2. (:warning: Currently f