HyMITATOR − Parameter synthesis for hybrid systems

Behavioral cartography

Reachability analysis

Navigation benchmark


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.

The Team

HyMITATOR has been originally developed at LSV.

Main contributors:

This page makes use of valid HTML 5 and valid CSS.

Content and CSS can be reused and modified under the terms of license Creative Commons Attribution 3.0 Unported (CC BY 3.0).

Creative Commons Attribution 3.0 Unported