Substitutive Composition of Workflow Nets — Exact Mathematical Realization:

• Definition 3.12 [PETRI25, p. 11]
• Definition 3.13 [PETRI25, p. 11] (Separable Workflow Nets)

Mathematical Definition (Definition 3.12)

Let $N = (P, T, F)$ be a Petri net and $t \in T$. Let $N' = (P', T', F')$ be a WF-net such that $(P \cup T) \cap (P' \cup T') = \emptyset$. The substitutive composition $N[t \to N']$ is the Petri net $(P'', T'', F'')$ defined by:

• $P'' = P \cup (P' \setminus \{N'_{source}, N'_{sink}\})$
• $T'' = (T \setminus \{t\}) \cup T'$
• $F'' = \{(u, v) \in F \mid u \neq t \wedge v \neq t\} \cup \{(u, v) \in F' \mid u \neq N'_{source} \wedge v \neq N'_{sink}\}$

     $\cup \{(p, t') \mid (p, t) \in F \wedge (N'_{source}, t') \in F'\}$
     $\cup \{(t', p) \mid (t, p) \in F \wedge (t', N'_{sink}) \in F'\}$

Theorem 5.6 Completeness Property [PETRI25 p. 31]

Every sound and safe separable WF-net can be decomposed losslessly into POWL 2.0 without fall-through.