Soundness of Timed-Arc Workflow Nets in Discrete and
Continuous-Time Semantics

J 2015

Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time Semantics

MATEO, Jose Antonio; Jiří SRBA and Mathias Grund SOERENSEN

Basic information

Original name

Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time Semantics

Authors

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

Edition

Fundamenta Informaticae, Państwowe Wydawnictwo Naukowe, 2015, 0169-2968

Other information

Language

English

Type of outcome

Article in a journal

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Netherlands

Confidentiality degree

is not subject to a state or trade secret

References:

URL

Impact factor

Impact factor: 0.658

RIV identification code

RIV/00216224:14330/15:00087227

Organization unit

Faculty of Informatics

DOI

https://doi.org/10.3233/FI-2015-1246

UT WoS

000358735900004

EID Scopus

2-s2.0-84938085299

Keywords in English

workflow nets; timed systems; system analysis

Changed: 5/4/2016 15:15, Prof. Jiří Srba, Ph.D.

Abstract

In the original language

Analysis of workflow processes with quantitative aspectslike timing is of interest in numerous time-critical applications. We suggest a workflow model based on timed-arc Petri nets and studythe foundational problems of soundness and strong (time-bounded) soundness.We first consider the discrete-time semantics (integer delays)and explore the decidability of the soundness problemsand show, among others, that soundness is decidable for monotonic workflow nets while reachability is undecidable.For general timed-arc workflow nets soundness andstrong soundness become undecidable, though we can design efficientverification algorithms for the subclass of bounded nets. We also discuss the soundness problem in the continuous-timesemantics (real-number delays) and show that for nets withnonstrict guards (where the reachability question coincides for bothsemantics) the soundness checking problem does not in generalfollow the approach for the discrete semantics and different zone-basedtechniques are needed for introducing its decidability in the bounded case.Finally, we demonstrate the usability of our theory onthe 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 (www.tapaal.net).

Cite

MATEO, Jose Antonio; Jiří SRBA and Mathias Grund SOERENSEN. Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time Semantics. Fundamenta Informaticae. Państwowe Wydawnictwo Naukowe, 2015, vol. 140, No 1, p. 89-121. ISSN 0169-2968. Available from: https://doi.org/10.3233/FI-2015-1246.

@article{1341639,
   author = {Mateo, Jose Antonio and Srba, Jiří and Soerensen, Mathias Grund},
   article_number = {1},
   doi = {https://doi.org/10.3233/FI-2015-1246},
   keywords = {workflow nets; timed systems; system analysis},
   language = {eng},
   issn = {0169-2968},
   journal = {Fundamenta Informaticae},
   title = {Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time Semantics},
   url = {http://content.iospress.com/articles/fundamenta-informaticae/fi1246},
   volume = {140},
   year = {2015}
}

TY  - JOUR
ID  - 1341639
AU  - Mateo, Jose Antonio - Srba, Jiří - Soerensen, Mathias Grund
PY  - 2015
TI  - Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time Semantics
JF  - Fundamenta Informaticae
VL  - 140
IS  - 1
SP  - 89-121
EP  - 89-121
PB  - Państwowe Wydawnictwo Naukowe
SN  - 01692968
KW  - workflow nets
KW  - timed systems
KW  - system analysis
UR  - http://content.iospress.com/articles/fundamenta-informaticae/fi1246
L2  - http://content.iospress.com/articles/fundamenta-informaticae/fi1246
N2  - Analysis of workflow processes with quantitative aspectslike timing is of interest in numerous time-critical applications. We suggest a workflow model based on timed-arc Petri nets and studythe foundational problems of soundness and strong (time-bounded) soundness.We first consider the discrete-time semantics (integer delays)and explore the decidability of the soundness problemsand show, among others, that soundness is decidable for monotonic workflow nets while reachability is undecidable.For general timed-arc workflow nets soundness andstrong soundness become undecidable, though we can design efficientverification algorithms for the subclass of bounded nets. We also discuss the soundness problem in the continuous-timesemantics (real-number delays) and show that for nets withnonstrict guards (where the reachability question coincides for bothsemantics) the soundness checking problem does not in generalfollow the approach for the discrete semantics and different zone-basedtechniques are needed for introducing its decidability in the bounded case.Finally, we demonstrate the usability of our theory onthe 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 (www.tapaal.net).
ER  -

MATEO, Jose Antonio; Jiří SRBA and Mathias Grund SOERENSEN. Soundness of Timed-Arc Workflow Nets in Discrete and Continuous-Time Semantics. \textit{Fundamenta Informaticae}. Pa\'nstwowe Wydawnictwo Naukowe, 2015, vol.~140, No~1, p.~89-121. ISSN~0169-2968. Available from: https://doi.org/10.3233/FI-2015-1246.

Přehled o publikaci