Workflow Nets, a subclass of Petri Nets, are suitable to model and analyze business processes formally. However, since Workflow Nets require a single source and sink place, they do not account for business processes with multiple start and end events. To model this behavior with Workflow Nets, it is required to manually reduce the net structure to a single source and sink place. Given this limitation, we propose Portable Nets, a novel class of Petri Nets designed to model business processes containing multiple start and end events. Tailored to Portable Nets, we extend the notion of soundness, a key correctness criterion for Workflow Nets, and provide a corresponding verification approach.
CEUR ceur-ws.org
Workflow Nets (WF-Nets) [
A Petri Net N = (P, T, F) is a P-Net if:
• there is a set of source places Pi ⊂ P, such that ∀ pi ∈ Pi : • pi = ∅;
• there is a set of sink places Po ⊂ P, such that ∀ po ∈ Po : po• = ∅;
• the sets Pi and Po are pairwise disjoint; and
• ∀ x ∈ P ∪ T : x is on the path from at least one pi ∈ Pi to at least one po ∈ P0.
A P-Net System Ω = (N, Mi) is a P-Net N = (P, T, F) with an initial marking Mi:= ∀ pi ∈ Pi: Mi(pi)
= 1 ∧ ∀ p ∈ P ⧵ {Pi}: Mi(p) = 0. Let [N, Ms⟩ be the set of reachable markings of Ω. Mf ∈ [N, Ms⟩ is
https://hpi.de/giese/people/mustafa-ghani.html (M. Ghani);
(a) Portable Net N
(b) Portable Net
called final marking of Ω, if ∀ po ∈ Po (⊂ P) : Mf (po) = 1 and for all p ∈ P⧵ {Po} : Mf (p) = 0. Ω is
sound, if for any reachable marking M1 ∈ [N, Ms⟩ starting from Mi, it is possible to reach the
ifnal marking M f. Formally, (N, Mi) [⟩ (N, M1) [⟩ (N, Mf), where [⟩ denotes a sequence of
ifring transitions t i ∈ T = t1,t2,...tn with n ∈ ℕ, such that [⟩ leads from Mi over M1 to Mf, and
there are no dead transitions. To check if N is sound, we employ liveness and boundedness [
Proof. is live, i.e. for every reachable state M1 ∈ [ , Ms⟩, there is a firing sequence, which
starts from the initial marking Mi (i.e. ∀ i ∈ i : Mi ( i) ≥ 1), that leads to a state in which t0
is enabled, i.e. ∀ o ∈ o : Mf ( o) ≥ 1. Since o is the set of input place of t0 ∈ , for any state
M1 reachable from the initial state Mi, it is possible to reach a state, where at least all places
of o are marked with at least one token. Suppose that M2 and Mf ∈ [ , Ms⟩ are reachable
states, where M2 is an arbitrary reachable marking and Mf := ∀ o ∈ : o is marked. Consider
that following marking M2 + Mf. In this state, t0 is enabled. If t0 fires, then the state M 2 +
Mi is reached. As is also bounded, M2 should be equal to the empty state. Hence, proper
termination, according to [
Proof. Suppose that N is sound and (N, Mi) is not bounded. Since N is not bounded, there are two markings M1 and M2 reachable from the initial marking Mi, such that (N, Mi) [⟩ (N, M1), (N, M1) [⟩ (N, M2) and M2 > M1. However, since N is sound, we know that there is a firing sequence , which leads to the final marking M f, such that (N, Mi) [ ⟩ (N, Mf). Therefore, there is a marking M3 such that (N, M2) [ ⟩ (N, M3) and M3 > Mf. Hence, it is not possible that N is both sound and not bound. So if N is sound, then (N, Mi) is bounded. From the fact that N is sound and (N, Mi) is bounded, we can deduce that ( , Mi) is bounded. If transition t0 ∈ fires, the net returns to the initial marking. ■
Proof. Assume N is sound. By Lemma 2 we know that ( , Mi) is bounded. Because N is sound, we know that marking Mi is a home-marking of , i.e., for every state reachable from ( , Mi) it is possible to return to ( , Mi). In (N, Mi), it is possible to fire an arbitrary transition t i ∈ T. This is also the case in . Therefore, ( , Mi) is live because for every state reachable from ( , Mi), it is possible to reach a state, which enables an arbitrary transition. ■ Theorem 1. A P-Net N is sound, if ( , Mi) is live and bounded.
Proof follows from Lemma 1, 2 and 3.
■
Related Work Literature proposes several variants of WF-Nets: Free-choice WF-Nets [
Conclusion We have presented P-Nets as a novel class of Petri Nets without the structural restrictions of a WF-Net, which requires a single source and sink place to verify soundness. P-Nets facilitate soundness verification of business processes with a set of start and end events. In contrast to WF-Nets, it is not required for P-Nets to perform numerous processing steps to translate such a business process with a set of start and end events into a net structure with a dedicated source and sink place. In future research, we aim to explore the general compositionality of two sound P-Nets while preserving soundness.