TIRA: Toolbox for Interval Reachability Analysis

Library of methods to compute an interval over-approximation of the finite-time reachable set for both continous- and discrete-time systems

TIRA: Toolbox for Interval Reachability Analysis

TIRA is a Matlab library gathering several methods to compute an interval over-approximation of the reachable set of a dynamical system. This means that each method creates a box containing the set of all the positions that can be reached by a given system subject to uncertainties on both its initial position and external disturbances. This type of over-approximation approaches is particularly important in the field of safety verification: since the exact reachable set is too complicated to be computed exactly, we compute an over-approximating set with the much simpler shape of a box, which ensures that if the box never includes a known unsafe set (such as an obstacle that we want to avoid with our robotic system), then we are guaranteed that all real system trajectories also avoid this unsafe set since they are all contained in the box.

As of version 2 (2021-12-03), TIRA contains 7 different methods (several having also numerous sub-methods) solving such reachability analysis problem. Creating a library of several methods solving the same problem is relevant because each method has its own strengths, weaknesses and limitations that makes it interesting for or applicable to only some cases. The choice of a toolbox architecture as a library of several methods also presents two big advantages. Firstly, if the user does not ask for a specific method to be used on their system, the toolbox will then automatically check the requirements of each available method until it finds one that can be called successfully. Secondly, the library architecture makes it very easy (either for the toolbox authors or for external users) to define and include new reachability methods into the unified framework of TIRA.

Documentation

A more in-depth description of TIRA and the implemented methods can be found in the Documentation folder. It contains:

• TIRA_user_manual.pdf: the user manual of the toolbox detailing the installation instructions, toolbox architecture, an overview of the implemented reachability methods and their requirements, as well as guidelines for three types of use of the toolbox (testing it on pre-defined examples; calling implemented reachability methods on your own system; adding new reachability methods to the toolbox).
• HSCC2019_paper.pdf: tool-paper at HSCC19 describing the toolbox architecture and the theory of the 5 main over-approximation methods implemented in version 1 of TIRA (2019-02-19).
• Springer2021_partial_preprint.pdf: partial preprint of the book Interval Reachability Analysis: Bounding Trajectories of Uncertain Systems with Boxes for Control and Verification containing a thourough tutorial-like presentation of all 7 reachability methods implemented in version 2 of TIRA (2021-12-03). The uploaded partial preprint contains the preface, table of content, and Appendix B related to TIRA). If you are interested in this book, feel free to contact the authors directly.

Changelog

Version 2 - 2021-12-03

• 2 new reachability methods: Quasi-Monte Carlo and Monte Carlo
• 1 new submethod for Sampled-data mixed-monotonicity, using second-order sensitivity
• Reworked logger for cleaner console outputs (error, warning, info, runtime)
• Folder Test_suite calling all methods and submethods to check that future changes of the toolbox do not break anything
• Tighter method for over-approximation of interval matrix exponential using Horner formulation and Scaling and squaring
• Option to pick or define the ODE solver used in continuous-time methods that need one
• Improved and more thourough user manual in folder Documentation

Version 1 - 2019-02-19

• Unified framework for interval reachability analysis of continuous-time and discrete-time systems
• 5 main reachability methods: Continuous-time monotonicity, Growth-bound and contraction analysis of continuous-time systems, Continuous-time mixed-monotonicity, Sampled-data mixed-monotonicity (with 2 submethods: Interval arithmetics, Sampling and falsification), Discrete-time mixed-monotonicity
• Folder Examples containing 12 pre-defined example systems

References

Citing TIRA

HSCC-2019 tool paper: TIRA: Toolbox for Interval Reachability Analysis

@inproceedings{meyer2019hscc,
  title={{TIRA}: Toolbox for Interval Reachability Analysis},
  author={Meyer, Pierre-Jean and Devonport, Alex and Arcak, Murat},
  booktitle={$22^{nd}$ ACM International Conference on Hybrid Systems: Computation and Control},
  pages={224-229},
  year={2019}
}

Reference book

The 2021 book Interval Reachability Analysis: Bounding Trajectories of Uncertain Systems with Boxes for Control and Verification provides a tutorial-like description of all interval reachability analysis methods implemented in version 2 of TIRA (2021-12-03)

@book{meyer2021springer,
  title={Interval Reachability Analysis: Bounding Trajectories of Uncertain Systems with Boxes for Control and Verification},
  author={Meyer, Pierre-Jean and Devonport, Alex and Arcak, Murat},
  year={2021},
  publisher={Springer}
}

Contributors

• Pierre-Jean Meyer, COSYS-ESTAS, Univ Gustave Eiffel, Lille. Email @univ-eiffel.fr : pierre-jean.meyer
• Alex Devonport, EECS, UC Berkeley. Email @berkeley.edu : alex_devonport
• Neelay Junnarkar, EECS, UC Berkeley
• Murat Arcak, EECS, UC Berkeley. Email @berkeley.edu : arcak

License

Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License (CC BY-NC-SA 4.0)