Soundness of Timed-Arc Workflow Nets

December 12, 2017 in by

by José Antonio Mateo, Jiří Srba, Mathias G. Sørensen
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.
Reference:
José Antonio Mateo, Jiří Srba, Mathias G. Sørensen. Soundness of Timed-Arc Workflow Nets. In Proceedings of the 35th International Conference on Applications and Theory of Petri Nets (ICATPN’14). Volume 8489 of Lecture Notes in Computer Science. Springer, June 2014.
Bibtex Entry:
@string{jun="June"}
@inproceedings{MSS-petrinets14,
  author =        {Mateo, Jos{'e} Antonio and Srba, Ji{v{r}}{'i} and
                   S{o}rensen, Mathias G.},
  booktitle =     {{P}roceedings of the 35th {I}nternational
                   {C}onference on {A}pplications and {T}heory of
                   {P}etri {N}ets ({ICATPN}'14)},
  editor =        {Ciardo, Gianfranco and Kindler, Ekkart},
  month =         jun,
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Soundness of Timed-Arc Workflow Nets},
  volume =        {8489},
  year =          {2014},
  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.},
  doi =           {10.1007/978-3-319-07734-5_4},
  url =           {http://www.cassting-project.eu/wp-content/uploads/
                  MSS-petrinets14.pdf},
  category =      {conf},
  wps =           {wp1},
  partners =      {AAU},
  casstingpart =  {100},
}