Publication details

Compositional Verification and Optimization of Interactive Markov Chains



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

Faculty of Informatics

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.

More info