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.
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