@inproceedings{,
 title = {Model Checking Interactive Markov Chains },
 year = {2010},
 author = {Lijun Zhang and Martin R. Neuh{\"a}u{\"s}er},
 series = {LNCS},
 booktitle = {Sixteenth International Conference on tools and
algorithms for the construction and analysis of systems (TACAS)},
 publisher = {Springer},
  subproject = {S3},
  access={restricted},
  bibtex={zhang.tacas10.bib},
  pdf={zhang.tacas10.pdf},
  abstract={Hermanns has introduced interactive Markov chains (IMCs) which arise as an
orthogonal extension of labelled transition systems and continuous-time
Markov chains (CTMCs). IMCs enjoy nice compositional aggregation properties
which help to minimize the state space incrementally.
However, the model checking problem for IMCs remains unsolved apart
from those instances, where the IMC can be converted into a CTMC.
This paper tackles this problem: We interpret the continuous stochastic
logic (CSL) over IMCs and define the semantics of probabilistic CSL formulas
with respect to the class of fully time and history dependent schedulers.
Our main contribution is an efficient model checking algorithm for
verifying CSL formulas on IMCs. Moreover, we show the applicability of our
approach and provide some experimental results.},
}