Compositional Verification and Optimization of Interactive Markov Chains

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři

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

Rok publikování 2013
Druh Článek ve sborníku
Konference CONCUR 2013 - Concurrency Theory - 24th International Conference
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-642-40184-8_26
Obor Informatika
Klíčová slova interactive Markov chains; continuous-time stochstic systems; composition; verification; specification
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.