@inproceedings{d9f9ed3d3b7047e5b391c0cc367aab17,
title = "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 labelled 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. Applications 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 modelling, state space generation and reduction, and model checking. The significance of the presented material and corresponding tools is highlighted through multiple case studies.",
keywords = "stochastic, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318003, EWI-25350, IR-93332, Interactive Markov chains, Abstraction, Model Checking, METIS-309682, logic",
author = "Florian Arnold and Daniel Gebler and Dennis Guck and Hassan Hatefi",
note = "Foreground = 25% ; Type of activity = publication in tutorial volume ; Main leader = UT ; Type of audience = Scientific community ; Size of audience = n.a. ; Countries addressed = international ;; Stochastic Model Checking ; Conference date: 22-10-2012 Through 26-10-2012",
year = "2014",
month = jun,
doi = "10.1007/978-3-662-45489-3_2",
language = "Undefined",
isbn = "978-3-662-45488-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "26--66",
editor = "A.K.I. Remke and Remke, {Anne Katharina Ingrid} and M.I.A. Stoelinga and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
booktitle = "Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems",
address = "Germany",
}