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.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Netherlands
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
WWW 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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-07734-5_4
Keywords in English workflow nets; soundness; timed-arc Petri nets
Tags core_B, firank_B
Tags International impact, Reviewed
Changed by Changed by: Prof. Jiří Srba, Ph.D., učo 2841. Changed: 10/4/2015 08:33.
Abstract
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.
PrintDisplayed: 5/10/2024 01:23