TY - GEN
T1 - Compositional verification and optimization of interactive Markov chains
AU - Hermanns, Holger
AU - Krčál, Jan
AU - Křetínský, Jan
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84882781870&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-40184-8_26
DO - 10.1007/978-3-642-40184-8_26
M3 - Conference contribution
AN - SCOPUS:84882781870
SN - 9783642401831
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 364
EP - 379
BT - Concurrency Theory - 24th International Conference, CONCUR 2013, Proceedings
T2 - 24th International Conference on Concurrency Theory, CONCUR 2013
Y2 - 27 August 2013 through 30 August 2013
ER -