Compositional Verification and Optimization of Interactive Markov Chains

HERMANNS, Holger, Jan KRČÁL a Jan KŘETÍNSKÝ. Compositional Verification and Optimization of Interactive Markov Chains. In CONCUR 2013 - Concurrency Theory - 24th International Conference. Heidelberg Dordrecht London New York: Springer, 2013, s. 364-379. ISBN 978-3-642-40183-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-40184-8_26.

Základní údaje

Originální název

Compositional Verification and Optimization of Interactive Markov Chains

Autoři

HERMANNS, Holger (276 Německo), Jan KRČÁL (203 Česká republika, domácí) a Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí)

Vydání

Heidelberg Dordrecht London New York, CONCUR 2013 - Concurrency Theory - 24th International Conference, od s. 364-379, 16 s. 2013

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/13:00066202

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-40183-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-40184-8_26

Klíčová slova anglicky

interactive Markov chains; continuous-time stochstic systems; composition; verification; specification

Štítky

core_A, firank_A, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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.

---

Návaznosti

GBP202/12/G061, projekt VaV	Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI) Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky
MUNI/A/0739/2012, interní kód MU	Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU) Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0760/2012, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty