Compositional Verification and Optimization of Interactive Markov Chains

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

HERMANNS Holger KRČÁL Jan KŘETÍNSKÝ Jan

Year of publication 2013
Type Article in Proceedings
Conference CONCUR 2013 - Concurrency Theory - 24th International Conference
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-642-40184-8_26
Field Informatics
Keywords interactive Markov chains; continuous-time stochstic systems; composition; verification; specification
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.