Verification of Open Interactive Markov Chains

Authors Tomas Brazdil, Holger Hermanns, Jan Krcal, Jan Kretinsky, Vojtech Rehak

Thumbnail PDF


  • Filesize: 0.53 MB
  • 12 pages

Document Identifiers

Author Details

Tomas Brazdil
Holger Hermanns
Jan Krcal
Jan Kretinsky
Vojtech Rehak

Cite AsGet BibTex

Tomas Brazdil, Holger Hermanns, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Verification of Open Interactive Markov Chains. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 474-485, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Interactive Markov chains (IMC) are compositional behavioral models extending both labeled transition systems and continuous-time Markov chains. IMC pair modeling convenience - owed to compositionality properties - with effective verification algorithms and tools - owed to Markov properties. Thus far however, IMC verification did not consider compositionality properties, but considered closed systems. This paper discusses the evaluation of IMC in an open and thus compositional interpretation. For this we embed the IMC into a game that is played with the environment. We devise algorithms that enable us to derive bounds on reachability probabilities that are assured to hold in any composition context.
  • IMC
  • compositional verification
  • synthesis
  • time bounded reachability
  • discretization


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail