A Tutorial on Interactive Markov Chains

Abstract. Interactive Markov chains (IMCs) constitute a powerful sto-chastic model that extends both continuous-time Markov chains and la-belled transition systems. IMCs enable a wide range of modelling and analysis techniques and serve as a semantic model for many industrial and scientific formalisms, such as AADL, GSPNs and many more. Appli-cations cover various engineering contexts ranging from industrial system-on-chip manufacturing to satellite designs. We present a survey of the state-of-the-art in modelling and analysis of IMCs. We cover a set of techniques that can be utilised for compositional mod-elling, state space generation and reduction, and model checking. The significance of the presented material and corresponding tools is high-lighted through multiple case studies.