IMITATOR (standing for Inverse Method for Inferring Time AbstracT behaviOR) is a tool for efficient synthesis for Timed Automata. It is originally based on the inverse method [ACEF09] and the behavioral cartography [AF10] for Parametric Timed Automata (PTAs). In particular, it generalizes a concrete behavior of a PTA, by synthesizing constraints on the parameters.
IMITATOR is fully written in OCaml, and is available under the GNU General Public License.
Its recent extension (in IMITATOR 2.5) to stopwatches with arbitrary resets allow its use in the framework of parametric scheduling analysis.
IMITATOR implements the following features:
The execution of IMITATOR is fully automated, from the source file to the generation of the behavioral tiles and the corresponding trace sets under a graphical form.
IMITATOR has been originally developed at LSV.
Main contributors:
IMITATOR got support from the following institutions and projects.
This page makes use of valid HTML 5 and valid CSS.