Polynomial Time Verification of Reachability in Sound Extended Free-Choice Workflow Nets

Abstract

Workflow nets are a standard way for modeling and analyzing workflows. There are two aspects in a workflow: definition and instance. In form of workflow nets, a workflow definition and a workflow instance are respectively represented as a net structure and a marking. The correctness of the workflow definition can be checked by using a workflow nets' property, called soundness. On the other hand, the correctness of the workflow instance can be checked by using a Petri nets' well-known property, called reachability. The reachability problem is known to be intractable. In this paper, we have shown that the reachability problem for (i) sound extended free-choice workflow nets with a marking representing one workflow instance or (ii) acyclic well-structured workflow nets with a marking representing one or more workflow instances can be solved in polynomial time.

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 — 15 citations exist upstream.

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