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/
- Supports also continuous-time systems, and not only linear but also nonlinear and hybrid ones.
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
Mainly some experimental code accompanying research papers.
In Julia
In Python
In Matlab
Breach toolbox for Matlab
Beware that Matlab’s toolboxes such as Requirements Toolbox and Simulink Design Verifier mention some temporal logic and temporal operators, but they do not adhere to the syntax of STL.