Software

Reachability analysis

Reachability analysis based on set propagation

In Matlab

• Multiparametric Toolbox (MPT): https://www.mpt3.org
  • Some functionality (invariant set computation) purely for discrete-time systems
• CORA: https://tumcps.github.io/CORA/
  • Continuous-time and hybrid systems.

Quite a few other tools can be found on the web but mostly unmaintained.

In Julia

• ReachabilityAnalysis.jl: https://juliareach.github.io/ReachabilityAnalysis.jl/

In Python

• Sorry, I am not aware of anything, but I will gladly add whatever you suggest. Just keep in mind that the tool should be actively maintained to be useful at least for study purposes.

Barrier certificates

No specialized software. At the moment just the same computational tools as for Lyapunov stability analysis – nonnegative (sum-of-squares) polynomial optimization, etc.

Temporal logics

Beware that Matlab’s toolboxes such as Requirements Toolbox and Simulink Design Verifier mention some temporal logic and temporal operators, they certainly do not implement the full breadth sketched in our lecture.