# Translating Workflow Nets to Process Trees: An Algorithmic Approach
## Preliminaries
### Algorithm  
In this section, we present an algorithm that iteratively applies the reductions defined in Section 3.3. By doing so, the algorithm is able to translate a WF-net into a process tree. We prove that, if the algorithm terminates correctly, i.e., it finds a process tree, the input WF-net is sound. Moreover, we show that the language of the input WF-net equals the language of the process tree found. Figure 12: Visualization of the \(\odot\)-pattern reduction. The pre-set of transition \(t_{1}\) equals the post-set of \(t_{2}\) and vice versa. The replacing transition inherits the pre- and post-set of transition \(t_{1}\). Consider Algorithm 1, in which we present an algorithmic description of the reduction algorithm, on the basis of the proposed patterns in Section 3.3. ```
input :\(W\)= \((P,T,F,p_{i},p_{o},\epsilon)\in\mathcal{W}\) output :\(W^{\prime}\)= \((P^{\prime},T^{\prime},F^{\prime},p_{i},p_{o},\kappa)\)\(\in\)\(\mathcal{W}_{\mathcal{Q}}\)
1\(P^{\prime}\), \(T^{\prime}\), \(F^{\prime}\), \(\kappa\)\(\leftarrow\)\(P\), \(T,F,\ell\);
2 while\(\exists\)\(SN\)\(\in\)\(\mathcal{SN}_{\mathcal{Q}}\) s.t. \(\theta_{\oplus}(N,SN)\) for\(\oplus\)\(\in\)\(\{\rightarrow,\times,\wedge,\circ\}\)do
3\(P^{\prime}\), \(T^{\prime}\), \(F^{\prime}\), \(\kappa\)\(\leftarrow\)\(\Theta_{\oplus}(N,SN)\);
4 return\((P^{\prime}\), \(T^{\prime}\), \(F^{\prime}\), \(p_{i},p_{o},\kappa)\);
```  
**Algorithm 1**WF-net reduction  
As an input, the algorithm needs any WF-net \(W\), which, by definition, is also a PTWF-net. Initially, the elements of \(W\), excluding the initial and final place, are copied into variables \(P^{\prime}\), \(T^{\prime}\), \(F^{\prime}\), \(\kappa\). In case any pattern of the form \(\theta_{\oplus}(N,SN)\) is found in \(N\), the corresponding reduction \(\Theta_{\oplus}(N,SN)\) is applied (line 3). If no more pattern is found, the algorithm returns \((N,p_{i},p_{o},\kappa)\). The algorithm returns the most recent reduction, if no more pattern is found. Observe that, intentionally, the order and size of the patterns to be reduced is not specified, i.e., it is of no relevance to any of the lemmas and the theorems regarding the algorithms properties and correctness. In the case the obtained PTree-WF-net consists of just one transition, i.e., connected to place \(p_{i}\) (incoming) and place \(p_{o}\) (outgoing) (cf. Figure 5(e)), the label of the transition represents a process tree, describing the same language as the original WF-net. Furthermore, we can conclude that the original WF-net is, in fact, a sound WF-net. We prove these observations in Theorem 1. However, before this, we first present two useful lemmas. In Lemma 5, we prove that the proposed reduction rules are bidirectionally soundness preserving, i.e., if a PTree-WF-net is sound, the reduced PTree-WF-net is sound (and vice versa). In Lemma 6, we prove that, if we are able, from the initial marking \([p_{i}]\), to enable the observed fragment (enabling differs per fragment), then the language of the original net and the reduced net is equal (and vice versa). Observe that, trivially, the reduction rules applied on a PTree-WF-net yield a PTree-WF-net, i.e., none of the requirements of Definition 1 are violated on the resulting net. **Lemma 5** (Pattern Reduction is Soundness Preserving). : _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}}\). \(W^{\prime}\) is sound iff \(W\) is sound._  
**Proof. ** (\(\Rightarrow\)) Let \(t^{\prime}\)\(\in\)\(T^{\prime}\)\(\setminus\)\(T\). Assume that \(W\) is sound, yet \(W^{\prime}\) is not sound. By definition of any reduction \(\Theta_{\oplus}(W,SN)\), if \(W^{\prime}\) is not safe, then \(W\) is not safe.