Document Open Access Logo

Verification of Open Interactive Markov Chains

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2012.474.pdf
  • Filesize: 0.53 MB
  • 12 pages

Document Identifiers

Subject Classification

Keywords
  • IMC
  • compositional verification
  • synthesis
  • time bounded reachability
  • discretization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get 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) https://doi.org/10.4230/LIPIcs.FSTTCS.2012.474

Author Details

Tomas Brazdil
Holger Hermanns
Jan Krcal
Jan Kretinsky
Vojtech Rehak
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact