We apply SReachTools to perform the following analysis on various stochastic LTI and LTV systems:

  1. backward stochastic reachability (verification and controller synthesis)
  2. forward stochastic reachability (prediction of the stochasticity of the state in future)

Please feel free to add requests for more examples at https://github.com/sreachtools/SReachTools/issues. The code for XYZ.html is available in examples/XYZ.m. These html pages were created using MATLAB’s publish command (see examples/publish_examples.m).

Backward stochastic reachability

(Under)approximative verification and controller synthesis

Using convex optimization, Fourier transforms, mixed-integer linear programming, and computation geometry, we can perform backward stochastic reachability. Here, we define safety by requiring the state to stay within a pre-specified target tube (a collection of time-varying safe sets).

  • Verification problem: We can use SReachSet to compute the set of initial states and their associated admissible controllers such that the probability of safety of the system is above a user-specified threshold.
  • Controller synthesis problem: We can use SReachPoint to compute the optimal (open-loop or affine) controller that maximizes the safety probability, the likelihood of staying with the target tube.
  • See the table in the documentation page for how SReachTools can solve these problems and the available approximation guarantees.
  • In all of these examples, we will validate the optimal controllers using Monte-Carlo simulations.

We provide the following demonstration examples:

  1. Spacecraft rendezvous problem: In a satellite rendezvous problem, we wish to steer a spacecraft (deputy) towards another spacecraft on the same elliptical orbit (chief), while staying within the line-of-sight cone and respecting actuation limits. The relative dynamics of the deputy with respect to the chief spacecraft is a LTI system (Clohessy-Wiltshire-Hill dynamics) with additive Gaussian disturbance.
  2. Dubin’s vehicle with a known turn rate: Given a Dubin’s car with a known turning rate and additive disturbance in position, we wish to ascertain the set of initial states and its associated controllers from which the car can be steered to lie within a target tube.
  3. Automated anesthesia delivery system: Given the dynamics for the sedation levels of a patient, we wish to design an automated anesthesia delivery system that maintains the probability of the depth of hypnosis to stay within pre-specified bounds, above 0.99. Open in Code Ocean
  4. Lagrangian approximations for the stochastic double integrator: For a stochastic double integrator, we compute the over- and under-approximations for the stochastic viability problem, and compare it with the dynamic programming.
  5. Building Automation System: For assuring probabilistic safety in a multi-room building automation system. Open in Code Ocean

Dynamic programming

Stochastic double integrator: For a stochastic double integrator, we compute a grid-based dynamic programming solution to the stochastic reachability of different target tubes listed below.

  • Stochastic viability problem
  • Stochastic reach-avoid problem (terminal hitting time)
  • Stochastic reachability of a target tube (a collection of time-varying safe sets)

The application of SReachDyn is given in [dIntSReachDyn.html].

Forward stochastic reachability

  1. Spacecraft rendezvous problem: Computes the probability of the state of the spacecraft lying in a set at future time of interest with/without safety requirements. We also demonstrate how SReachTools can handle a deterministic and a stochastic initial state. The dynamics of the spacecraft is assumed to be a LTI system (Clohessy-Wiltshire-Hill dynamics) with additive Gaussian disturbance, and the controller is given by a LQR controller.