| Údaje o výsledku |
| Identifikační kód | RIV/00216224:14330/11:00067394 |
| Název v původním jazyce | Quantitative Multi-Objective Verification for Probabilistic Systems |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor | IN - Informatika |
| Rok uplatnění | 2011 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů |
| Počet výskytů výsledku | 2 |
| Údaje z Hodnocení výsledků výzkumných organizací 2014 |
| Výsledek byl hodnocen v Pilíři I |
| Rozsah vyřazení výsledku | Tento výskyt výsledku není vyřazen |
| Zařazení výsledku v hodnocení | D - Článek ve sborníku |
| Skupina oboru v hodnocení | 04 - Technické a informatické vědy |
| Konkrétní způsob(y) hodnocení výsledku | Článek ve sborníku evidovaném v databázi Scopus bodovaný podle SJR zdroje typu Book Series nebo Conference Proceedings |
| Bodové ohodnocení | 53,461 |
| Faktor korekce | 100,9 % |
| Body (upravené podle přílohy č. 8 Metodiky) | 53,957 |
| Rozdělení výsledku mezi předkladatele |
| Organizace | Výzkumná organizace? | Podíl | Body | Body (upravené podle přílohy č. 8 Metodiky) |
|---|
| Masarykova univerzita / Fakulta informatiky | ano | 33,3 % | 17,820 | 17,986 |
|
| Tvůrci výsledku |
| Počet tvůrců celkem | 5 |
| Počet domácích tvůrců | 1 |
| Tvůrce | Forejt Vojtěch (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 2477912) |
| Tvůrce | Kwiatkowska Marta (státní příslušnost: GB - Spojené království Velké Británie a Severního Irska) |
| Tvůrce | Norman Gethin (státní příslušnost: GB - Spojené království Velké Británie a Severního Irska) |
| Tvůrce | Parker David (státní příslušnost: GB - Spojené království Velké Británie a Severního Irska) |
| Tvůrce | Qu Hongyang (státní příslušnost: CN - Čínská lidová republika) |
| Údaje blíže specifikující výsledek |
| Popis v původním jazyce | We present a verification framework for analysing multiple quantitative objectives of systems that exhibit both nondeterministic and stochastic behaviour. These systems are modelled as probabilistic automata, enriched with cost or reward structures that capture, for example, energy usage or performance metrics. Quantitative properties of these models are expressed in a specification language that incorporates probabilistic safety and liveness properties, expected total cost or reward, and supports multiple objectives of these types. We propose and implement an efficient verification framework for such properties and then present two distinct applications of it: firstly, controller synthesis subject to multiple quantitative objectives; and, secondly, quantitative compositional verification. The practical applicability of both approaches is illustrated with experimental results from several large case studies. |
| Klíčová slova | stochastic systems; verification; multi-objective optimisation |
| Kód UT ISI | 000301820100011 |
| Název sborníku | Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11) |
| Rozsah stran | 112-127 |
| Forma vydání | P - Tištěná verze „print“ |
| ISSN | 0302-9743 |
| Počet stran výsledku | 16 |
| ISBN | 9783642198342 |
| Název nakladatele | Springer-Verlag |
| Místo vydání | Německo |
| Místo konání akce | Saarbrücken, Germany |
| Rok konání akce | 2011 |
| Typ akce podle státní příslušnoti účastníků | WRD - Světová |
| DOI výsledku | 10.1007/978-3-642-19835-9_11 |
| Údaje o tomto záznamu o výsledku |
| Předkladatel | Masarykova univerzita / Fakulta informatiky |
| Dodavatel | MSM - Ministerstvo školství, mládeže a tělovýchovy (MŠMT) |
| Rok sběru | 2014 |
| Systémové označení dodávky dat | RIV14-MSM-14330___/01:1 |
| Specifikace | RIV/00216224:14330/11:00067394!RIV14-MSM-14330___ |
| Kontrolní kód | [AF15D93E5CDF] |
| Další výskyty tohoto výsledku od stejného předkladatele |
| Dodáno MŠMT v roce 2012 | Záznam s identifikačním kódem RIV/00216224:14330/11:00056901 v dodávce dat RIV12-MSM-14330___/01:1 |
| Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl |
| Projekt | 1M0545 - Institut Teoretické Informatiky (2005-2011, MSM/1M) |