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

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.

Cite this work

No public copy is stored for this record, so only the metadata is cited.

Stored only when both papers are in the corpus — 46 citations exist upstream.

Papers that cite the same references — the relational fallback while embeddings are still backfilling.