Soundness of Timed-Arc Workflow Nets

D 2014

Soundness of Timed-Arc Workflow Nets

MATEO, Jose A., Jiří SRBA a Mathias SOERENSEN

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

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"

Odkazy

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

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

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 10. 4. 2015 08:33, Prof. Jiří Srba, Ph.D.

Anotace

V originále

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.

Citovat

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, 2014, s. 51-70. ISBN 978-3-319-07733-8. Dostupné z: https://dx.doi.org/10.1007/978-3-319-07734-5_4.

@inproceedings{1297399,
   author = {Mateo, Jose A. and Srba, Jiří and Soerensen, Mathias},
   address = {Nizozemsko},
   booktitle = {Proceedings of the 35th International Conference on Application and Theory of {P}etri Nets and Concurrency ({ICATPN}'14)},
   doi = {http://dx.doi.org/10.1007/978-3-319-07734-5_4},
   keywords = {workflow nets; soundness; timed-arc Petri nets},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Nizozemsko},
   isbn = {978-3-319-07733-8},
   pages = {51-70},
   publisher = {Springer-Verlag},
   title = {Soundness of Timed-Arc Workflow Nets},
   url = {http://link.springer.com/chapter/10.1007/978-3-319-07734-5_4},
   year = {2014}
}

TY  - JOUR
ID  - 1297399
AU  - Mateo, Jose A. - Srba, Jiří - Soerensen, Mathias
PY  - 2014
TI  - Soundness of Timed-Arc Workflow Nets
PB  - Springer-Verlag
CY  - Nizozemsko
SN  - 9783319077338
KW  - workflow nets
KW  - soundness
KW  - timed-arc Petri nets
UR  - http://link.springer.com/chapter/10.1007/978-3-319-07734-5_4
L2  - http://link.springer.com/chapter/10.1007/978-3-319-07734-5_4
N2  - 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.
ER  -

MATEO, Jose A., Jiří SRBA a Mathias SOERENSEN. Soundness of Timed-Arc Workflow Nets. In \textit{Proceedings of the 35th International Conference on Application and Theory of $\{$P$\}$etri Nets and Concurrency ($\{$ICATPN$\}$'14)}. Nizozemsko: Springer-Verlag, 2014, s.~51-70. ISBN~978-3-319-07733-8. Dostupné z: https://dx.doi.org/10.1007/978-3-319-07734-5\_{}4.

Podrobný výpis o publikaci