Compositional Verification and Optimization of Interactive Markov Chains

• 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
• 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

• Centrum excelence - Institut teoretické informatiky
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II.