MATEO, Jose A., Jiří SRBA a Mathias SOERENSEN. Soundness of Timed-Arc Workflow Nets. In Proceedings of the 35th International Conference on Application and Theory of {P}etri Nets and Concurrency ({ICATPN}'14). Nizozemsko: Springer-Verlag. s. 51-70. ISBN 978-3-319-07733-8. doi:10.1007/978-3-319-07734-5_4. 2014.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Soundness of Timed-Arc Workflow Nets
Autoři MATEO, Jose A. (724 Španělsko), Jiří SRBA (203 Česká republika, garant, domácí) a Mathias SOERENSEN (208 Dánsko).
Vydání Nizozemsko, Proceedings of the 35th International Conference on Application and Theory of {P}etri Nets and Concurrency ({ICATPN}'14), od s. 51-70, 20 s. 2014.
Nakladatel Springer-Verlag
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Nizozemské království
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
WWW Link
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/14:00080033
Organizační jednotka Fakulta informatiky
ISBN 978-3-319-07733-8
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-07734-5_4
Klíčová slova anglicky workflow nets; soundness; timed-arc Petri nets
Štítky firank_B
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: Prof. Jiří Srba, Ph.D., učo 2841. Změněno: 10. 4. 2015 08:33.
Anotace
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.
VytisknoutZobrazeno: 19. 4. 2024 17:10