A Branching-Process-Based Method to Check Soundness of Workflow Systems

Guanjun Liu, Wolfgang Reisig, Changjun Jiang, Mengchu Zhou

Research output: Contribution to journalArticlepeer-review

46 Scopus citations

Abstract

Workflow nets (WF-nets) as a class of Petri nets are widely used to model and analyze workflow systems. Soundness is an important property of WF-nets, which guarantees that the systems are deadlock-and livelock-free and each task has a chance to be performed. Van der Aalst has proven that the soundness problem is decidable for WF-nets and we have also shown that it is PSPACE-complete for bounded ones. Since the definition of soundness is based on reachability and Van der Aalst has proven that a sound WF-net must be bounded, the soundness detection can be carried out via the reachability graph analysis. However, the state explosion problem is a big obstacle to this technique. The unfolding technique of Petri nets can effectively avoid/alleviate this problem. This paper proposes an algorithm to generate a finite prefix of the unfolding of a WF-net, called basic unfolding. Furthermore, a necessary and sufficient condition is proposed to decide soundness based on basic unfolding. In addition, some examples illustrate that the unfolding technique can save the storage space effectively.

Original languageEnglish (US)
Article number7527679
Pages (from-to)4104-4118
Number of pages15
JournalIEEE Access
Volume4
DOIs
StatePublished - 2016

All Science Journal Classification (ASJC) codes

  • General Computer Science
  • General Materials Science
  • General Engineering

Keywords

  • Petri nets
  • branching processes
  • business process model
  • soundness
  • unfolding

Fingerprint

Dive into the research topics of 'A Branching-Process-Based Method to Check Soundness of Workflow Systems'. Together they form a unique fingerprint.

Cite this