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.


What is an Interactive Markov Chain?

An Interactive Markov Chain (IMC) is equal to an Continuous Time Markov Decision Process (CTMDP), where the Markovian and interactive transitions are separated.

What is IMCA for?

The Interactive Markov Chain Analyzer supports:

How to use IMCA?

IMCA is a tool written in C++. It is available for

platforms. More infos how to run IMCA can be found in the documentation.

A small Presentation for the GUI Version (1.2)

Für den Inhalt dieser Seite ist eine neuere Version von Adobe Flash Player erforderlich.

Adobe Flash Player herunterladen



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.