Compositional verification and optimization of interactive Markov chains

Holger Hermanns, Jan Krčál, Jan Křetínský

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

7 Scopus citations

Abstract

Interactive Markov chains (IMC) are compositional behavioural models extending labelled transition systems and continuous-time Markov chains. We provide a framework and algorithms for compositional verification and optimization of IMC with respect to time-bounded properties. Firstly, we give a specification formalism for IMC. Secondly, given a time-bounded property, an IMC component and the assumption that its unknown environment satisfies a given specification, we synthesize a scheduler for the component optimizing the probability that the property is satisfied in any such environment.

Original languageEnglish
Title of host publicationConcurrency Theory - 24th International Conference, CONCUR 2013, Proceedings
Pages364-379
Number of pages16
DOIs
StatePublished - 2013
Event24th International Conference on Concurrency Theory, CONCUR 2013 - Buenos Aires, Argentina
Duration: 27 Aug 201330 Aug 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8052 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference24th International Conference on Concurrency Theory, CONCUR 2013
Country/TerritoryArgentina
CityBuenos Aires
Period27/08/1330/08/13

Fingerprint

Dive into the research topics of 'Compositional verification and optimization of interactive Markov chains'. Together they form a unique fingerprint.

Cite this