| Údaje o výsledku |
| Identifikační kód | RIV/00216224:14330/13:00067580 |
| Název v původním jazyce | Verification of Liveness Properties on Closed Timed-Arc Petri Nets |
| 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 | 33,3 % | 15,394 | 7,714 |
|
| Tvůrci výsledku |
| Počet tvůrců celkem | 5 |
| Počet domácích tvůrců | 1 |
| Tvůrce | Andersen Mathias (státní příslušnost: DK - Dánské království) |
| Tvůrce | Larsen Heine 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 | Soerensen Mathias G. (státní příslušnost: DK - Dánské království) |
| Tvůrce | Taankvist Jakob H. (státní příslušnost: DK - Dánské království) |
| Údaje blíže specifikující výsledek |
| Popis v původním jazyce | Verification of closed timed models by explicit state-space exploration methods is an alternative to the wide-spread symbolic techniques based on difference bound matrices (DBMs). A few experiments found in the literature confirm that for the reachability analysis of timed automata explicit techniques can compete with DBM-based algorithms, at least for situations where the constants used in the models are relatively small. To the best of our knowledge, the explicit methods have not yet been employed in the verification of liveness properties in Petri net models extended with time. We present an algorithm for liveness analysis of closed Timed-Arc Petri Nets (TAPN) extended with weights, transport arcs, inhibitor arcs and age invariants and prove its correctness. The algorithm computes optimized maximum constants for each place in the net that bound the size of the reachable state-space. |
| Klíčová slova | timed-arc Petri nets; verification; liveness; discretization |
| Název sborníku | Proceedings of Mathematical and Engineering Methods in Computer Science (MEMICS'12) |
| Rozsah stran | 69-81 |
| Forma vydání | P - Tištěná verze „print“ |
| ISSN | 0302-9743 |
| Počet stran výsledku | 13 |
| ISBN | 9783642360442 |
| Název nakladatele | Springer-Verlag |
| Místo vydání | Netherlands |
| Místo konání akce | Znojmo |
| Rok konání akce | 2012 |
| Typ akce podle státní příslušnoti účastníků | EUR - Evropská |
| DOI výsledku | 10.1007/978-3-642-36046-6_8 |
| Ú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:00067580!RIV14-MSM-14330___ |
| Kontrolní kód | [27FF59262B9A] |
| 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 |