| Údaje o výsledku |
| Identifikační kód | RIV/00216224:14330/12:00064717 |
| Název v původním jazyce | Automatic Verification of Competitive Stochastic Systems |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor | IN - Informatika |
| Rok uplatnění | 2012 |
| 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í | D - Článek ve sborníku |
| Skupina oboru v hodnocení | 04 - Technické a informatické vědy |
| Konkrétní způsob(y) hodnocení výsledku | Výsledek hodnocený již v předchozím hodnocení, body se přebírají |
| Bodové ohodnocení | 44,376 |
| Faktor korekce | 77,6 % |
| Body (upravené podle přílohy č. 8 Metodiky) | 34,420 |
| 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 % | 14,792 | 11,473 |
|
| 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; G - garant výsledku; vedidk: 2477912) |
| Tvůrce | Kwiatkowska Marta (státní příslušnost: PL - Polská republika) |
| Tvůrce | Parker Dave (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 a model checking algorithm for verifying properties expressed in this logic and implement the techniques in a probabilistic model checker, based on the PRISM tool. |
| Klíčová slova | stochastic games; branching time logics; multi-agent systems |
| Název sborníku | Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference |
| Rozsah stran | 315-330 |
| Forma vydání | P - Tištěná verze „print“ |
| ISSN | 0302-9743 |
| ISBN | 9783642287558 |
| Počet stran výsledku | 15 |
| Název nakladatele | Springer-Verlag |
| Místo vydání | Berlin, Heidelberg |
| Místo konání akce | Tallinn |
| Rok konání akce | 2012 |
| Typ akce podle státní příslušnoti účastníků | WRD - Světová |
| Adresa www stránky s výsledkem | http://www.prismmodelchecker.org/papers/tacas12.pdf |
| DOI výsledku | 10.1007/978-3-642-28756-5_22 |
| Ú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 | 2013 |
| Systémové označení dodávky dat | RIV13-MSM-14330___/02:2 |
| Specifikace | RIV/00216224:14330/12:00064717!RIV13-MSM-14330___ |
| Kontrolní kód | [EDC5B4BEE4AC] |
| 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 | LA09016 - Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM) (2009-2012, MSM/LA) |
| I - Instit. podpora na rozvoj výzkumné organizace |