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.

Erlang(30,10) model

Introduction

This case studie will show the different options the tool offers. We use the IMC depicted below, where Erl(30,10) denotes a transition with an Erlang (k,n) distributed delay. This corresponds to k=30 consecutive Markovian transitions, each with rate n = 10. Thus, the time to move from s2 to goal state s3 is K/n = 3 with variance k/n^2 = 3/10.

The source of the IMC model can be found here: erlang3010.imc


Model


Time-Bounded Reachability

We have computed the minimum and maximum time-bounded reachability probability for time-bound z=7 with scheduler synthesis for maximum time-bounded reachability.

minimum maximum
time interval: [0,7] [0,7]
error-bound: 0.0001 0.0001
probability: 0.491991 0.982829
computing time: 3.62014 sec 3.78784 sec

Expected-Time and Expected-Steps

We have computed the minimum and maximum expected-time and expected-steps to reach the goal state s4 from initial state s0.

expected-time expected-steps
minimum: 2 2
maximum: 4 31

For all computations the computing time was between 11 and 12 seconds.

News

03.08.2014

IMCA 1.6 beta Bugfix.

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.