Soundness of Timed-Arc Workflow Nets

D 2014

Soundness of Timed-Arc Workflow Nets

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

Basic information

Original name

Soundness of Timed-Arc Workflow Nets

Authors

MATEO, Jose A. (724 Spain), Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution) and Mathias SOERENSEN (208 Denmark)

Edition

Nizozemsko, Proceedings of the 35th International Conference on Application and Theory of {P}etri Nets and Concurrency ({ICATPN}'14), p. 51-70, 20 pp. 2014

Publisher

Springer-Verlag

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Netherlands

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

References:

Link

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/14:00080033

Organization unit

Faculty of Informatics

ISBN

978-3-319-07733-8

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-07734-5_4

Keywords in English

workflow nets; soundness; timed-arc Petri nets

Abstract

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 and 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, p. 51-70. ISBN 978-3-319-07733-8. Available from: 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 and 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, p.~51-70. ISBN~978-3-319-07733-8. Available from: https://dx.doi.org/10.1007/978-3-319-07734-5\_{}4.

Detailed Information on Publication Record