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

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).