| Údaje o výsledku |
| Identifikační kód | RIV/00216224:14330/13:00072717 |
| Název v původním jazyce | Local Model Checking of Weighted CTL with Upper-Bound Constraints |
| Druh | D - Článek ve sborníku |
| 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í | 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í | 46,181 |
| Faktor korekce | 50,1 % |
| Body (upravené podle přílohy č. 8 Metodiky) | 23,141 |
| 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 | 40,0 % | 18,472 | 9,256 |
|
| Tvůrci výsledku |
| Počet tvůrců celkem | 4 |
| Počet domácích tvůrců | 1 |
| Tvůrce | Jensen Jonas F. (státní příslušnost: DK - Dánské království) |
| Tvůrce | Larsen Kim G. (státní příslušnost: DK - Dánské království) |
| Tvůrce | Srba Jiří (státní příslušnost: CZ - Česká republika; A - domácí tvůrce; vedidk: 2753057) |
| Tvůrce | Oestergaard Lars K. (státní příslušnost: DK - Dánské království) |
| Údaje blíže specifikující výsledek |
| Popis v původním jazyce | We present a symbolic extension of dependency graphs by Liu and Smolka in order to model-check weighted Kripke structures against the logic CTL with upper-bound weight constraints. Our extension introduces a new type of edges into dependency graphs and lifts the computation of fixed-points from boolean domain to nonnegative integers in order to cope with the weights. We present both global and local algorithms for the fixed-point computation on symbolic dependency graphs and argue for the advantages of our approach compared to the direct encoding of the model checking problem into dependency graphs. We implement all algorithms in a publicly available tool prototype and evaluate them on several experiments. The principal conclusion is that our local algorithm is the most efficient one with an order of magnitude improvement for model checking problems with a high number of “witnesses”. |
| Klíčová slova | weigted CTL; model checking; Kripke structure; on-the-fly technique |
| Název sborníku | Proceedings of International SPIN Symposium on Model Checking of Software (SPIN'13) |
| Rozsah stran | 178-195 |
| Forma vydání | P - Tištěná verze „print“ |
| ISSN | 0302-9743 |
| ISBN | 9783642391750 |
| Počet stran výsledku | 18 |
| Název nakladatele | Springer-Verlag |
| Místo vydání | Netherlands |
| Místo konání akce | New York, USA |
| Rok konání akce | 2013 |
| Typ akce podle státní příslušnoti účastníků | WRD - Světová |
| DOI výsledku | 10.1007/978-3-642-39176-7_12 |
| Ú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:00072717!RIV14-MSM-14330___ |
| Kontrolní kód | [6BEEB2A06A7D] |
| 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 |