# Translating Workflow Nets to Process Trees: An Algorithmic Approach
## Preliminaries
### Pattern Reduction
#### 3.3.4 Loop Pattern  
The final operator we consider is the \(\odot\)-operator, i.e., the only operator with just two children. Hence, the fragments representing a loop pattern in the Ptree-net consist of two transitions. Consider the left-hand side of Figure 12, in which we schematically depict the loop pattern fragment. Conceptually, the loop operator requires us first to execute its leftmost child (the \"do-part\"). Secondly, its rightmost child is optionally executed (the \"redo-part\"). However, we always finish with  
Figure 11: Visualization of the \(\wedge\)-pattern reduction. Transitions \(t_{1},...,t_{n}\) have disjunct pre-sets, yet, their pre-sets have the exact same pre-sets. The same holds for the post-sets of transitions \(t_{1},...,t_{n}\). The replacing transition inherits all pre- and post-sets of \(t_{1},...,t_{n}\). the leftmost child. As such, the post-set of a transition corresponding to the do-part needs to be the pre-set of the transition that represents the redo-part. Furthermore, there should be no other way to enable the redo-part. Hence, the do-part needs to be the only transition that marks the pre-set of the redo-part. Similarly, to guarantee global language preservation, the do-part should be the only element in the post-set of its pre-set, i.e., no other transition may be enabled by the pre-set of the do-part. Reconsider Figure 8. Observe that \(p_{2}\) contains multiple incoming and outgoing arcs; hence, it describes neither a loop-pattern for transitions \(t_{2}\) and \(t_{3}\) nor for transitions \(t_{4}\) and \(t_{5}\). **Proposition 4** (\(\odot\)-Pattern). : _Let \(N{=}(P,T,F,\kappa){\in}\mathcal{N}_{\mathcal{Q}}\) and let \(t_{1}{\
eq}t_{2}{\in}T\). Iff:_  
1. \(\bullet t_{1}{=}t_{2}\bullet\)_, pre-set of_ \(t_{1}\) _is the post-set of_ \(t_{2}\)_;_
2. \(t_{1}{\bullet}{\bullet}{\bullet}t_{2}\)_, pre-set of_ \(t_{2}\) _is the post-set of_ \(t_{1}\)_;_
3. \(\forall p{\in}\bullet t_{1}\)_(_\(p{\in}{=}\{t_{1}\}\)_)_,_ \(t_{1}\) _is the only transition in the post-set of its pre-set;_
4. \(\forall p{\in}t_{1}{\bullet}\)_(_\(\bullet p{=}\{t_{1}\}\)_);_ \(t_{1}\) _is the only transition in the pre-set of its post-set,_  
_then, system net \(SN{=}\left(N^{\prime}{=}\left(P^{\prime},T^{\prime},F^{\prime},\kappa|_{\{t_{1 },t_{2}\}}\right),\bullet t_{1},t_{1}\bullet\right)\) (\(P_{i}{=}\bullet t_{1},\ P_{o}{=}t_{o}\bullet\)), with \(P^{\prime}{=}\bullet t_{1}{\cup}t_{1}\bullet\), \(T^{\prime}{=}\{t_{1},t_{2}\}\), \(F^{\prime}{=}\{(x,y){\in}F\ |\ x{\in}\{t_{1},t_{2}\}\lor y{\in}\{t_{1},t_{2}\}\}\) is a feasible \(\odot\)-pattern._  
Proof. : Observe that \(t_{1}\) is the only enabled transition in \(N^{\prime}\) in marking \(M_{i}{=}P_{i}\). When we fire it, we immediately mark \(P_{o}\), which is the final marking of the place-bordered system net. In the aforesaid marking, \(t_{2}\) is the only enabled transition. Firing \(t_{2}\) yields us with marking \(M_{i}\) again. We can repeat this infinitely. Hence, the labeled language described by the pattern is \(\{\sigma_{1}{\cdot}\sigma_{1}^{\prime}{\cdot}\sigma_{2}{\cdot}\sigma_{2}^{ \prime}\cdots\sigma_{n}\ |\ n\geq 1\land\forall 1{\leq}i{\leq}n\left(\sigma_{i}{ \in}\mathcal{L}_{\mathcal{Q}}(\kappa(t_{1}))\right)\land\forall 1{\leq}i{ \leq}n\left(\sigma_{i}^{\prime}{\in}\mathcal{L}_{\mathcal{Q}}(\kappa(t_{2})) \right)\}\), which equals \(\odot\left(\mathcal{L}_{\mathcal{Q}}(\kappa(t_{1})),\mathcal{L}_{\mathcal{Q}}( \kappa(t_{2}))\right)\)  
**Lemma 4** (\(\odot\)-Pattern (Proposition 4) is Globally Language-Preserving). : _Let \(N{=}(P,T,F,\kappa){\in}\mathcal{N}_{\mathcal{Q}}\) and let \(SN{=}(P^{\prime},T^{\prime}{=}\{t_{1},t_{2},\ldots,t_{n}\},F^{\prime},\kappa|_ {T^{\prime}}),\bullet t_{1},t_{1}\bullet\) s.t. \(\theta_{\odot}(N,SN)\) according to Proposition 4. The feasible pattern \(\theta_{\odot}(N,SN)\) is globally language-preserving._  
Proof. : Let \(N^{\prime\prime}\) denote the net obtained after reduction (cf. Definition 9) and let \(P^{\prime\prime}{=}(P\backslash P^{\prime}){\cup}P_{i}{\cup}P_{o}\).