Info

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.

Publications

Here you will find some publications about IMC's and MA's.

Publications about IMC's and MA's

Guck, D. and Han, T. and Katoen, J.P. and Neuhäußer, M.R. (2012) Quantitative Timed Analysis of Interactive Markov Chains. In NASA Formal Methods Symposium (NFM). pages 8–23. Volume 7226 of Lecture Notes in Computer Science. Springer-Verlag.
Martin R. Neuhäußer. Model Checking Nondeterministic and Randomly Timed Systems. PhD Thesis, RWTH Aachen University and University of Twente, 2010.
Lijun Zhang, and Martin R. Neuhäußer. Model Checking Interactive Markov Chains. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pages 53–68. Volume 6015 of Lecture Notes in Computer Science. Springer, 2010.
Holger Hermanns, and Joost-Pieter Katoen. The How and Why of Interactive Markov Chains. In Formal Methods for Components and Objects (FMCO). pages 311–337. Volume 6286 of LNCS. Springer-Verlag, 2010.
Holger Hermanns. Interactive Markov chains: and the quest for quantified quality. Springer-Verlag, 2002.


Here you will find some external publications.

External Publications

J. Bruno, P. Downey, and G. N. Frederickson. Sequencing Tasks with Exponential Service Times to Minimize the Expected Flow Time or Makespan. Journal of the ACM, Volume 28 Issue 1, Jan. 1981.
P.C. Kanellakis and S.A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. PODC '83 Proceedings of the second annual ACM symposium on Principles of distributed computing.

News

10.07.2014

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

More recent versions available at github!

08.03.2013

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

14.02.2013

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

08.11.2012

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

29.03.2012

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.

05.01.2012

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

20.01.2011

Update of the IMCA tool to version 1.1.

10.10.2010

First release of the IMCA tool.