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. © 2013 Springer-Verlag.
CITATION STYLE
Hermanns, H., Krčál, J., & Křetínský, J. (2013). Compositional verification and optimization of interactive Markov chains. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8052 LNCS, pp. 364–379). https://doi.org/10.1007/978-3-642-40184-8_26
Mendeley helps you to discover research relevant for your work.