| Identifikační kód | RIV/00216224:14330/14:00080033 |
|---|
| Název v anglickém jazyce | Soundness of Timed-Arc Workflow Nets |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2014 |
|---|
| 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 | 3 |
|---|
| Počet domácích tvůrců | 1 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Jose A. Mateo (státní příslušnost: ES - Španělské království)
Jiří Srba (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2753057)
Mathias Soerensen (státní příslušnost: DK - Dánské království) |
|---|
| Popis výsledku v anglickém jazyce | Analysis of workflow processes with quantitative aspects like timing is of interest in numerous time-critical applications. We suggest a workflow model based on timed-arc Petri nets and study the foundational problems of soundness and strong (time-bounded) soundness. We explore the decidability of these problems and show, among others, that soundness is decidable for monotonic workflow nets while reachability is undecidable. For general timed-arc workflow nets soundness and strong soundness become undecidable, though we can design efficient verification algorithms for the subclass of bounded nets. Finally, we demonstrate the usability of our theory on the case studies of a Brake System Control Unit used in aircraft certification, the MPEG2 encoding algorithm, and a blood transfusion workflow. The implementation of the algorithms is freely available as a part of the model checker TAPAAL. |
|---|
| Klíčová slova oddělená středníkem | workflow nets; soundness; timed-arc Petri nets |
|---|
| Stránka www, na které se nachází výsledek | http://link.springer.com/chapter/10.1007/978-3-319-07734-5_4 |
|---|
| DOI výsledku | 10.1007/978-3-319-07734-5_4 |
|---|