PV3 IMITATOR: Inverse Method for Inferring Time Abstract behaviorcan perform a number of actions on a network of automata and a set of desired properties

Tool for automated parameter synthesis for concurrent timed systems

Application domain/field

Type of tool

Model checker?

Expected input


Own syntax/input language (.imi file) Property should be in a separate file (.imiprop file)

Expected output

? (depends on what analysis is done with the tool)


IMITATOR implements the following algorithms: Uses Parma Polyhedra Library (PPL)


License: GPL v3
Automaton Synthesis


Related papers

Last publication date

15 July 2021

Related tools

HyMITATOR, extension of IMITATOR for parameter synthesis on hybrid systems.

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.