Verification of Liveness Properties on Closed Timed-Arc Petri Nets (2013)výskyt výsledku
| Identifikační kód | RIV/00216224:14330/13:00067580 |
|---|---|
| Název v anglickém jazyce | Verification of Liveness Properties on Closed Timed-Arc Petri Nets |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor - skupina | I - Informatika |
| Obor | IN - Informatika |
| Rok uplatnění | 2013 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku | 1 |
| Počet tvůrců celkem | 5 |
| Počet domácích tvůrců | 1 |
| Výčet všech uvedených jednotlivých tvůrců | Mathias Andersen (státní příslušnost: DK - Dánské království) Heine G. Larsen (státní příslušnost: DK - Dánské království) Jiří Srba (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2753057) Mathias G. Soerensen (státní příslušnost: DK - Dánské království) Jakob H. Taankvist (státní příslušnost: DK - Dánské království) |
| Popis výsledku v anglické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 inthe 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 oddělená středníkem | timed-arc Petri nets; verification; liveness; discretization |
| Stránka www, na které se nachází výsledek | - |
| DOI výsledku | 10.1007/978-3-642-36046-6_8 |
Údaje o výsledku v závislosti na druhu výsledku
| Název sborníku | Proceedings of Mathematical and Engineering Methods in Computer Science (MEMICS'12) |
|---|---|
| ISBN | 9783642360442 |
| ISSN | 0302-9743 |
| Počet stran výsledku | 13 |
| Strana od-do | 69-81 |
| Název nakladatele | Springer |
| Místo vydání | Netherlands |
| Místo konání akce | Znojmo |
| Datum konání akce | 2012 |
| Typ akce podle státní příslušnosti účastníků | EUR - Evropská |
| Kód UT WoS článku podle Web of Science | - |
Ostatní informace 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 |
| Specifikace | RIV/00216224:14330/13:00067580!RIV14-MSM-14330___ |
| Datum poslední aktualizace výsledku | 29.05.2014 |
| Kontrolní číslo | 56536902 |
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
| Projekt podporovaný MŠMT v programu LG | LG13010 - Zastoupení ČR v European Research Consortium for Informatics and Mathematics (2013 - 2015) |
|---|---|
| Podpora / návaznosti | Institucionální podpora na rozvoj výzkumné organizace |