HYMITATOR is a tool dedicated to the synthesis of parameters for hybrid automata (HA). It is a fork of IMITATOR, the tool for parameter synthesis in timed automata.
HYMITATOR implements extensions of the inverse method [ACEF09] and the behavioral cartography [AF10], initially defined for parametric timed automata, and adapted to hybrid automata [FK11]. In particular, it generalizes a concrete behavior of a HA, by synthesizing constraints on the parameters guaranteeing the same time-abstract behavior.
HYMITATOR is fully written in OCaml, and is available under the GNU General Public License.
HYMITATOR implements the following features:
The execution of HYMITATOR is fully automated, from the source file to the generation of the behavioral tiles and the corresponding trace sets under a graphical form.
HYMITATOR has been originally developed at LSV.