=Paper=
{{Paper
|id=Vol-3730/poster3
|storemode=property
|title=Portable Nets: Modeling and Verification of Business Processes with multiple Start and End Points
|pdfUrl=https://ceur-ws.org/Vol-3730/poster3.pdf
|volume=Vol-3730
|authors=Mustafa Ghani,Holger Giese
|dblpUrl=https://dblp.org/rec/conf/apn/GhaniG24
}}
==Portable Nets: Modeling and Verification of Business Processes with multiple Start and End Points==
https://ceur-ws.org/Vol-3730/poster3.pdf
Portable Nets: Modeling and Verification of Business
Processes with multiple start and end points
Mustafa Ghani1 , Holger Giese1
1
Hasso Plattner Institute, University of Potsdam, Germany
Abstract
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.
Keywords
Petri Nets, Portable Nets, Soundness
Introduction Workflow Nets (WF-Nets) [1], a subclass of Petri Nets [2], are an established
mathematical framework to model and analyze business processes. The analysis of soundness
[1], a crucial behavioral correctness criterion of WF-Nets, requires a static net structure with a
dedicated source and sink place representing a unique start and end event. If a business process
contains a set of start and end events, one needs to translate this behavior to a WF-Net with
a dedicated source and sink place to ensure the required net structure for the verification of
soundness [3]. This yields numerous processing steps. To eliminate this overhead, we introduce
Portable Nets (P-Nets) as a novel class of Petri Nets. In this paper, we extend soundness for
P-Nets and apply the same verification technique used for WF-Nets in [4].
Portable 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
PNSE’24, International Workshop on Petri Nets and Software Engineering, 2024
∗
Corresponding author.
Envelope-Open mustafa.ghani@hpi.de (M. Ghani); holger.giese@hpi.de (H. Giese)
GLOBE https://hpi.de/giese/people/mustafa-ghani.html (M. Ghani);
https://hpi.de/giese/people/prof-dr-holger-giese.html (H. Giese)
Orcid 0009-0004-6056-2125 (M. Ghani); 0000-0002-4723-730X (H. Giese)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
(a) Portable Net N (b) Portable Net 𝑁
Figure 1: Portable Net 𝑁 = (𝑃, 𝑇, 𝐹) used to verify soundness of Portable Net N = (P, T, F)
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
final marking Mf . Formally, (N, Mi ) [𝜎⟩ (N, M1 ) [𝜎⟩ (N, Mf ), where [𝜎⟩ denotes a sequence of
firing transitions ti ∈ 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 [2],
two standard Petri Net analysis techniques, and define a corresponding P-Net 𝑁 = (𝑃, 𝑇, 𝐹) with
an initial marking M1 . 𝑁 is the P-Net that we obtain by adding an extra transition t0 ∈ 𝑇, which
connects 𝑃o ∈ 𝑃 and 𝑃i ∈ 𝑃. 𝑁 is visualized in Figure 1. For N and 𝑁 we prove the following
result: N is sound, if (𝑁, Mi ) is live and bounded. Therefore, we define three Lemmata.
Lemma 1. If 𝑁 is live and bounded, then N is a sound P-Net.
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 M2 +
Mi is reached. As 𝑁 is also bounded, M2 should be equal to the empty state. Hence, proper
termination, according to [4] is guaranteed. From the fact that 𝑁 is live, we can derive that
there are no dead transitions. Hence, N is a sound P-Net. ■
Lemma 2. If N is sound, then 𝑁 is bounded.
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 Mf , 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. ■
Lemma 3. If N is sound, then 𝑁 is live.
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 ti ∈ 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. Proof follows from Lemma 1, 2 and 3. ■
Related Work Literature proposes several variants of WF-Nets: Free-choice WF-Nets [4],
Resource-constrained WF-Nets [5], and Time Workflow Nets [6]. In [7], business processes
with multiple end events are considered, but a dedicated start event is still required. None
of them model business processes with a set of source and sink places while also providing a
corresponding soundness verification procedure without the need to execute modification steps
on the structure of the net.
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.
References
[1] W. M. Van der Aalst, The application of petri nets to workflow management, Journal of
circuits, systems, and computers 8, (1998).
[2] W. Reisig, Understanding Petri Nets, Springer, (2016).
[3] A. A. Kalenkova, W. M. van der Aalst, I. A. Lomazova, V. Rubin, Process mining using bpmn:
relating event logs and process models, Software & Systems Modeling 16, (2015).
[4] W. M. Van der Aalst, Verification of workflow nets, Int. Conf. on Application and Theory
of Petri Nets, (1997).
[5] K. Van Hee, N. Sidorova, M. Voorhoeve, Resource-constrained workflow nets, Fundamenta
Informaticae 71, (2006).
[6] H. Boucheneb, K. Barkaoui, Strongly generalized soundness of time workflow nets, Pro-
ceedings of 15th Int. Conference on Application of Concurrency to System Design (2015).
[7] D. Liu, J. Wang, S. C. Chan, J. Sun, L. Zhang, Modeling workflow processes with colored
petri nets, Computers in Industry 49, (2002).