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:
- 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
- Mac OSX
- Windows with cygwin
platforms. More infos how to run IMCA can be found in the documentation.