| Údaje o výsledku |
| Identifikační kód | RIV/00216224:14330/13:00072856 |
| Název v původním jazyce | Automatic Verification of Competitive Stochastic Systems |
| Druh | J - Článek v odborném periodiku |
| Jazyk | eng - angličtina |
| Obor | IN - Informatika |
| Rok uplatnění | 2013 |
| 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 | 1 |
| Ú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í | Jimp - Článek v impaktovaném časopise evidovaném ve Web of Science |
| Skupina oboru v hodnocení | 04 - Technické a informatické vědy |
| Konkrétní způsob(y) hodnocení výsledku | Článek v impaktovaném časopise evidovaném ve Web of Science |
| Bodové ohodnocení | 12,749 |
| Faktor korekce | 86,1 % |
| Body (upravené podle přílohy č. 8 Metodiky) | 10,980 |
| 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 % | 4,250 | 3,660 |
|
| Tvůrci výsledku |
| Počet tvůrců celkem | 5 |
| Počet domácích tvůrců | 1 |
| Tvůrce | Chen Taolue (státní příslušnost: CN - Čínská lidová republika) |
| 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 | Parker David (státní příslušnost: GB - Spojené království Velké Británie a Severního Irska) |
| Tvůrce | Simaitis Aistis (státní příslušnost: LT - Litevská republika) |
| Údaje blíže specifikující výsledek |
| Popis v původním jazyce | We present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular goal. We define a temporal logic called rPATL for expressing quantitative properties of stochastic multi-player games. This logic allows us to reason about the collective ability of a set of players to achieve a goal relating to the probability of an event's occurrence or the expected amount of cost/reward accumulated. We give an algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, as an extension of the PRISM tool. |
| Klíčová slova | Quantitative verification; Probabilistic model checking; Stochastic multi-player games; Probabilistic temporal logic |
| Kód UT ISI | 000321223500003 |
| Rozsah stran | 61-92 |
| Název periodka | Formal Methods in System Design |
| ISSN | 0925-9856 |
| Svazek periodika | 43 |
| Číslo periodika v rámci uvedeného svazku | 1 |
| Stát vydavatele periodika | US - Spojené státy americké |
| Počet stran výsledku | 32 |
| DOI výsledku | 10.1007/s10703-013-0183-7 |
| Ú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/13:00072856!RIV14-MSM-14330___ |
| Kontrolní kód | [10957ACD49B5] |
| Jiný výskyt tohoto výsledku se v RIV nenachází |
| Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl |
| Projekt | LG13010 - Zastoupení ČR v European Research Consortium for Informatics and Mathematics (2013-2015, MSM/LG) |
| I - Instit. podpora na rozvoj výzkumné organizace |