Verification of open interactive Markov chains

Tomáš Brázdil, Holger Hermanns, Jan Krčál, Jan Křetínský, Vojtěch Řehák

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

13 Scopus citations

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.

Original languageEnglish
Title of host publication32nd International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012
Pages474-485
Number of pages12
DOIs
StatePublished - 2012
Event32nd International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012 - Hyderabad, India
Duration: 15 Dec 201217 Dec 2012

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume18
ISSN (Print)1868-8969

Conference

Conference32nd International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012
Country/TerritoryIndia
CityHyderabad
Period15/12/1217/12/12

Keywords

  • Compositional verification
  • Discretization
  • IMC
  • Synthesis
  • Time bounded reachability

Fingerprint

Dive into the research topics of 'Verification of open interactive Markov chains'. Together they form a unique fingerprint.

Cite this