# Translating Workflow Nets to Process Trees: An Algorithmic Approach
## Preliminaries
### Algorithm
For any \(t\)\(\in\)\(T\)\(\cap\)\(T^{\prime}\), if \(\
exists\)\(M\)\(\in\)\(\mathcal{R}(W^{\prime},[p_{i}])\)\(((W^{\prime},M)[t))\), then also \(\
exists\)\(M\)\(\in\)\(\mathcal{R}(W,[p_{i}])\)\(((W,M)[t))\). Similarly, if \(\
exists\)\(M\)\(\in\)\(\mathcal{R}(W^{\prime},[p_{i}])\)\(((W^{\prime},M)[t^{\prime}))\), then this is also holds for the transitions in \(SN\). In the case \(\exists\)\(M\)\(\in\)\(\mathcal{R}(W^{\prime},[p_{i}])\) s.t. \(\
exists\)\(\sigma\)\(\in\)\(T^{\prime\ast}\)\(\Big{(}(W^{\prime},M)\xrightarrow{\sigma}(W^{\prime},[p_{o}])\Big{)}\), again, by definition of the reductions, also \(M\)\(\in\)\(\mathcal{R}(W^{\prime},[p_{i}])\) and \(\
exists\)\(\sigma\)\(\in\)\(T^{\prime\ast}\)\(\Big{(}(W,M)\xrightarrow{\sigma}(W,[p_{o}])\Big{)}\), contradicting soundness of \(W\). (\(\Leftarrow\)) Assume that \(W^{\prime}\) is sound. Given that \(W^{\prime}\) and \(W\) only differ on \(t^{\prime}\) and \(SN\), respectively, the \"non-sound\" part of \(W\) needs to be part of \(SN\). However, it is easy to see that none of the patterns defined in Section 3.3 do not describe any non-sound construct. Hence, replacing \(SN\), implies that \(W^{\prime}\) needs to be unsound, which contradicts the assumption. **Lemma 6** (Pattern Reduction is Language Preserving in \(\Lambda\)). : _Let \(\oplus\)\(\in\)\(\{\rightarrow,\times,\wedge,\circ\}\), let \(W\)=\((P,T,F,p_{i},p_{o},\kappa)\)\(\in\)\(\mathcal{W}_{\mathcal{Q}}\), let \(SN\)\(\in\)\(\mathcal{SN}_{\mathcal{Q}}\), s.t., \(\theta_{\oplus}(W,SN)\), and, let \(W^{\prime}\)=\((P^{\prime},T^{\prime},F^{\prime},p_{i},p_{o},\kappa^{\prime})\)=\(\Theta_{\oplus}(W,SN)\)\(\in\)\(\mathcal{W}_{\mathcal{Q}}\). \(\mathcal{L}_{\mathcal{N}}^{v}\)\((\Lambda(W))\)\(=\)\(\mathcal{L}_{\mathcal{N}}^{v}\)\((\Lambda(W^{\prime}))\)._  
**Proof. ** It trivially follows from Lemmas 1-4. **Theorem 1** (Algorithm 1 is able to find Language-Equal Process Trees). : _Let \(W{=}\left(P,T,F,p_{i},p_{o},\ell\right){\in}\mathcal{W}\) and let \(W^{\prime}{=}\left(P^{\prime},T^{\prime},F^{\prime},p^{\prime}{}_{i},p^{\prime} _{o},\kappa\right){\in}\mathcal{W}_{Q}\) be the resulting WF-net of Algorithm 1 on \(W\). If \(P^{\prime}{=}\left\{P_{i},P_{o}\right\}\), \(T^{\prime}{=}\left\{t\right\}\), and \(F{=}\left\{\left(p_{i},t\right),\left(t,p_{o}\right)\right\}\), then \(\mathcal{L}_{Q}(\kappa(t)){=}\mathcal{L}_{\mathcal{N}}^{v}(W)\)._  
Proof. : Observe that \(W\) is sound. Lemma 5 implies that if we (continuously) revert the reductions applied by Algorithm 1, i.e., corresponding to all intermediate assignments of \(W\) in Algorithm 1, all reverted nets are sound. As a corollary of this fact, it follows that \(W\) is sound. Observe that Lemma 6 proves that the language of the unfoldings of all the intermediate WF-nets found is the same as well. Since the labels of the initial WF-net are all members of \(\Sigma\cup\left\{\tau\right\}\), their unfolding remains the same. Hence, we deduce \(\mathcal{L}_{Q}(\kappa(t)){=}\mathcal{L}_{\mathcal{N}}^{v}(W)\). It is important to note that neither the algorithm nor the supporting lemmas and proofs specify any condition on order and the size of the pattern(s) to be reduced. In fact, the size of the pattern reduced is not of influence with respect to any of the correctness proofs. Note that, indeed, \(\rightarrow\left(Q_{1},\rightarrow\left(Q_{2},\rightarrow\left(Q_{3},\tau \right)\right)\right)\) corresponds to \(\rightarrow\left(Q_{1},Q_{2},Q_{3}\right)\), and, hence, whether we iteratively find the first pattern or apply some form of pattern maximization strategy to instantly find the latter pattern is not at all of influence with respect to correctness of the proposed algorithm.