| Identifikační kód | RIV/00216224:14330/13:00066202 |
|---|
| Název v anglickém jazyce | Compositional Verification and Optimization of Interactive Markov Chains |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2013 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 2 |
|---|
| Počet tvůrců celkem | 3 |
|---|
| Počet domácích tvůrců | 2 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Holger Hermanns (státní příslušnost: DE - Spolková republika Německo)
Jan Krčál (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 9668780)
Jan Křetínský (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3503054) |
|---|
| Popis výsledku v anglickém jazyce | 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. |
|---|
| Klíčová slova oddělená středníkem | interactive Markov chains; continuous-time stochstic systems; composition; verification; specification |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-642-40184-8_26 |
|---|