The HyReach Toolbox

HyReach is a MATLAB-based tool for the reachability analysis of linear hybrid systems. It represents reachable sets using support functions and is based on the principles presented in “Reachability Analysis of Hybrid Systems Using Support Functions” (Colas Le Guernic and Antoine Girard). In comparison to other available tools, HyReach integrates a variety of different algorithms and procedures for separate tasks performed by the reachability analyses. Hence, it allows the user to directly specify which algorithms will be used during the analysis. The provided GUI enables the user to easily choose between the provided algorithms and visualize the analysis results as graphical output. Moreover, the tool supports the concept of time- and fixpoint-triggered transitions within hybrid automata, which could be taken if a certain time has been reached or if a fixpoint has been found.

HyReach consists basically of two main components - the GUI and the computation core. The GUI component allows for the specification of user parameters such as the algorithms to be used, initial and input sets, settings related to the support function representation, general options and the input file defining the hybrid automaton. This information is passed to the computation core which performs the reachability analysis and returns its results to the GUI which can than be used to generate plots of different dimensions. The computation core itself consists of implementations of different algorithms for flowpipe construction, computation of guard intersections, overapproximations of the initial set and strategies to pick between multiple possible transitions. Some of these algorithms have been implemented within the HyReach tool, others were imported and require the availability of certain plug-ins, e.g. the MATLAB optimization toolbox, the CVX toolbox or the MPT toolbox.

A hybrid automaton can be provided in two different ways. The first option is to model the hybrid automaton graphically and provide that file. This can be done by creating a MATLAB/SIMULINK Statechart using a special syntax. A detailed description of this syntax with examples is shown in the “Help” document. The second option is to provide a hybrid automaton to the tool in a textual file defining the automaton. Those files are MATLAB .m functions which have to stick to a certain interface providing the data describing the automaton as output parameters. The big advantage of this format is that it allows the use of general MATLAB functions within the .m file. Thus, it is possible to specify hybrid automata construction-rules which might be based on a concrete parametrization or workspace values.

• Input formats: textual (M-Script based), graphical
• Different scenarios for flowpipe construction
• Different overapproximations for the initial set
• Different solvers for linear programming (used for support function representation of polytopes)
• Different algorithms for intersection computation
• Optional clustering of sets before computation of the intersection with guards
• Influence on the number of directions (constraints of the polytopes used for set representation)
• Specification of the initial set
• Specification of the input set
• Configuration of the timestep, time-horizon and max. number of considered discrete transitions
• Support for multi-threading
• Use of additional toolboxes for optimization (CVX, MPT)
• Choice of a strategy for transition picking
• Fixpoint detection
• Fixpoint triggered transitions
• Generation of visual output and export into different formats
• Textual output of the reached intervals for every dimension

• The backtracking for the transition picker setting “All” does not work at the moment

If you are interested in the project or accessing HyReach's Matlab code, please write a mail to: makhlouf[at]embedded[dot]rwth-aachen[dot]de or hansen[at]embedded[dot]rwth-aachen[dot]de

To gain access to the executable HyReach matlab files please contact us.
HyReach Example Input-Models
Help PDF