Unbounded Reachability
With the unbounded reachability, you can calculate the probability to reach a set of goal states from a set of initial states. It is possible to compute the maximum and minimum reachability probability.
- Home
- Time-Bounded Reachability
- Interval-Bounded Reachability
- Unbounded Reachability
- Expected Time
- Expected Steps
- Long-run Average
- Scheduler Synthesis
- Bisimulation
- Documentation
- Case Studies
- Download
- Contact
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.
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.