IMCA
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.
![](imc_low_res.png)
What is IMCA for?
The Interactive Markov Chain Analyzer supports:
- Time-Bounded Reachability
- Interval-Bounded Reachability
- Unbounded Reachability
- Expected Time
- Expected Steps (Version 1.1 and 1.2)
- Long-run Average
- Scheduler Synthesis (Version 1.1 and 1.2)
- Bisimulation (Version 1.1 and 1.2)
How to use IMCA?
IMCA is a tool written in C++. It is available for
- Linux
- Mac OSX
- Windows with cygwin
platforms. More infos how to run IMCA can be found in the documentation.