# Translating Workflow Nets to Process Trees: An Algorithmic Approach
## Preliminaries
### Pattern Reduction
#### 3.3.2 Exclusive Choice Pattern  
The \(\times\)-operator, i.e., \(\times(Q_{1},...,Q_{n})\), describes \"execute one of \(Q_{1},...,Q_{n}\)\". In terms of a Petri net fragment, transitions \(t_{1},...,t_{n}\) are in an exclusive choice pattern if their pre- and post-sets are equal (yet non-overlapping). Consider Figure 10, in which we schematically depict the \(\times\)-pattern.  
We formalize the \(\times\)-pattern as follows.  
**Proposition 2** (\(\times\)-Pattern).: _Let \(N{=}(P,T,F,\kappa){\in}\mathcal{N}_{Q}\) and let \(T^{\prime}{=}\{t_{1},...,t_{n}\}{\subseteq}T\) (\(n{\geq}2\)). If and only if:_  
1. \(\bullet t_{1}{=}\bullet t_{2}{=}\cdots{=}\bullet t_{n}\)_, all pre-sets are shared among the members of the pattern;_
2. \(t_{1}{=}\bullet t_{2}{\bullet}=\cdots{=}t_{n}{\bullet}\)_, all post-sets are shared among the members of the pattern; and_
3. \(\forall 1{\leq}i{\leq}n\) (\(\bullet t_{i}{\
eq}t_{i}{\bullet}\))_, self-loops are not allowed,_  
_then, system net \(SN{=}\left(N^{\prime}{=}\left(P^{\prime},T^{\prime},F^{\prime},\kappa\right| _{T^{\prime}}\right),\bullet t_{1},t_{1}{\bullet}\right)\) (\(P_{i}{=}\bullet t_{1}\) and \(P_{o}{=}t_{1}{\bullet}\)), with \(P^{\prime}{=}\bullet t_{1}{\cup}t_{1}{\bullet}\), \(F^{\prime}{=}\{(x,y){\in}F\mid x{\in}T^{\prime}{\lor}y{\in}T^{\prime}\}\), is a feasible \(\times\)-pattern._  
Proof.: Observe that \(t_{1},t_{2},...,t_{n}\) are the only enabled transitions in \(N^{\prime}\) in marking \(M_{i}{=}P_{i}\). When we fire any one of these transitions, we immediately mark \(P_{o}\), which is the final marking of the system net. Hence, the set of firing sequences of the system net is the union of the set of sequences \((\Lambda(N^{\prime}),M_{i})\xrightarrow{\sigma}_{\Rightarrow}(\Lambda(N^{ \prime}),M_{i})\), where \(\sigma\) either corresponds to a labelled language of \(\mathcal{L}_{\mathcal{Q}}(\kappa(t_{1})\), or \(\mathcal{L}_{\mathcal{Q}}(\kappa(t_{2})\),..., or \(\mathcal{L}_{\mathcal{Q}}(\kappa(t_{n})\). Observe that, indeed, this set corresponds to \(\mathcal{L}_{\mathcal{Q}}(\times(\kappa(t_{1}),\kappa(t_{2}),\ldots,\kappa(t_{ n})))\).  
**Lemma 2** (\(\times\)-Pattern (Proposition 2) 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_{\times}(N,SN)\) according to Proposition 2. The feasible pattern \(\theta_{\times}(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{\setminus}P^{\prime}){\cup}P_{i}{\cup}P_{o}\). Observe that, similar to the sequential pattern, \(\Lambda(N)\) and \(\Lambda(N^{\prime\prime})\) are identical, except for \(\Lambda(N^{\prime})\) and \(\hat{\lambda}(t^{\prime})\), respectively. Again, the only connections between \(N^{\prime}\) and \(t^{\prime}\) with the identical parts of the two nets are through \(P_{i}\) (\"entering\") and \(P_{o}\)(\"exiting\"). Hence, if there exists a visible firing sequence in \(\mathcal{L}_{\mathcal{N}}^{v}(\Lambda(N),M,M^{\prime})\) that is not in \(\mathcal{L}_{\mathcal{N}}^{v}(\Lambda(N^{\prime\prime}),M,M^{\prime})\), this can only be due to different behavior described by \(\Lambda(N^{\prime})\) and \(\lambda(t^{\prime})\), again contradicting the feasibility of the pattern.