The IMCA tool is written in C++. It compiles on Linux systems, if all needed libraries are available. It was also testetd succesfully under Mac OSX and Windows with cygwin.

Informations about IMCA (1.4)

Here you will find informations about how to compile IMCA and how to use it.

Compilation of IMCA

IMCA needs the following additional libraries:

If all libraries are installed, you have to adjust the path to the SoPlex library in the Makefile. After running make you obtain an executable file imca in the bin folder. Note that IMCA is distributed under the GNU GENERAL PUBLIC LICENSE.

Informations about IMCA (1.2)

Here you will find informations about how to compile IMCA and how to use it.

Compilation of IMCA

IMCA needs the following libraries:

If all libraries are installed, just run the in the main folder. This will automatically start the compile routine and will create an executable file named imca in this folder. If this don't work, or you will compile it by yourself, you need to go into /bin/imcgui/ and run qmake and after that make. The program will compile if all libraries are installed correctly.


In the following manual, you will find a short description about the used input files and the functionalities of IMCA.


In the folder examples are some example IMC's, that can be used to test the IMCA tool.

The number of states and transitions of the model and the error-bound will have influence on the computing time. Below are some example computations for a workstation cluster model: workstation_cluster_N8.imc.

original closed and
states 2771 2771 135
transitions 10708 3637 407

Computing time for time-bounded reachability:

time-bound error-bound closed and
1 10^-4 797.59 sec 4.33504 sec
1 10^-6 2393.87 sec 415.544 sec
10 10^-4 800.478 sec 5.08759 sec
10 10^-6 2393.8 sec 480.023 sec
100 10^-4 803.598 sec 5.24707 sec
100 10^-6 2644.56 sec 480.424 sec



IMCA 1.6 beta Bugfix.


IMCA 1.6 beta available. Includes full support of Markov automata with rewards.

More recent versions available at github!


IMCA 1.5 beta update available. Includes bcg2imca translator and an interval step output for time-bounded reachability.


IMCA 1.5 beta available. Changes in MEC decomposition for long-run average computation, small bugfixes and new examples.


IMCA 1.4 beta available. Bugfixes and extension with time- and step-bounded reachability for Markov automata.


IMCA 1.3 beta available as command-line tool. Usage of the SoPlex library and Markov Automata support. Functionality reduction to unbounded reachability, expected-time and long-run average. Full functionality will follow.


IMCA 1.2 beta available, including LP Solve library and LRA computation.


Update of the IMCA tool to version 1.1.


First release of the IMCA tool.