# Translating Workflow Nets to Process Trees: An Algorithmic Approach
## Preliminaries
### Pattern Reduction
#### 3.3.3 Concurrent Pattern  
The concurrent pattern is the most complicated pattern that we consider in this paper. In the concurrent pattern, interference between its transitions is possible. The interference is achieved by requiring that the pre-sets and post-sets of the transitions do not have any overlap. Furthermore, the pre-set of the transition's pre-set places needs to be shared by all of these places, and, symmetrically, the post-set of the transition's post-set places needs to be shared by all of these places. That is, the enabling of the transitions in the pattern needs to be the same, and their post-set should jointly block any further action (i.e., within its local scope) until all places in their joint post-set  
Figure 10: Visualization of the \(\times\)-pattern reduction (dashed arcs are allowed to be part of the pattern, while solid arcs are required). All transitions in the pattern share the same pre- and post-set. The replacing transition inherits the aforesaid pre- and post-set. are marked. Consider the left-hand side of Figure 11, in which we schematically depict the concurrent pattern, which we formalize in Proposition 3. **Proposition 3** (\(\wedge\)-Pattern). : _Let \(N{=}(P,T,F,\kappa){\in}\mathcal{N}_{\mathcal{Q}}\) and let \(T^{\prime}{=}\{t_{1},...,t_{n}\}{\subseteq}T\) (\(n{\geq}2\)). If and only if:_  
1. \(\forall 1{\leq}i{<}j{\leq}n\left(\bullet t_{i}{\cap}t_{j}{=}\varnothing\right)\)_, no interaction between the member's pre-sets;_
2. \(\forall 1{\leq}i{<}j{\leq}n\left(t_{i}{\bullet}{\cap}t_{j}{=}\varnothing\right)\)_, no interaction between the member's post-sets;_
3. \(\forall 1{\leq}i{\leq}n\left(\forall p{\in}t_{i}\left(\bullet p{=}\{t_{i}\} \right)\right)\)_, pre-set places uniquely connect to a member;_
4. \(\forall 1{\leq}i{\leq}n\left(\forall p{\in}t_{i}\left(\bullet p{=}\{t_{i}\} \right)\right)\)_, post-set places uniquely connect to a member;_
5. \(\forall p{\in}\bullet T\left(\bullet p{\cap}\{t_{1},...,t_{n}\}{=}\varnothing\right)\)_, members do not influence other members;_
6. \(\forall p,p^{\prime}{\in}\bullet T\left(\bullet p{=}\bullet p^{\prime}\right)\)_, member's pre-sets share their pre-set;_
7. \(\forall p{\in}T\bullet\left(p{\in}\bullet\{t_{1},...,t_{n}\}{=}\varnothing\right)\)_, member firing does not affect other members;_
8. \(\forall p,p^{\prime}{\in}T\bullet\left(p{=}p^{\prime}\bullet\right)\)_, member's post-sets share their post-set;_
9. \(\forall t,t^{\prime}{\in}\bullet\left(\bullet T\right)\left(\bullet t{=}\bullet t ^{\prime}\right)\)_, pre-sets of enablers are equal;_
10. \(\forall t,t^{\prime}{\in}\left(T\bullet\right)\bullet\left(t{=}t^{\prime}\bullet\right)\)_, post-sets of enablers are equal,_  
_then, system net \(SN{=}\left(N^{\prime}{=}(P^{\prime},T^{\prime},F^{\prime},\kappa|_{T^{\prime}} )\right),\bullet T^{\prime},T^{\prime}\bullet\right)\) (\(P_{i}{=}{\bullet}T^{\prime},\quad P_{o}{=}T^{\prime}\bullet\right)\), with \(P^{\prime}{=}\bullet T{\cup}T\bullet\), \(F^{\prime}{=}\{(x,y){\in}F|(x{\in}P^{\prime}{\lor}y{\in}T^{\prime})\lor(x{ \in}T^{\prime}{\wedge}y{\in}P^{\prime})\}\) is a feasible \(\wedge\)-pattern._  
Proof. : Observe that \(t_{1},t_{2},...,t_{n}\) are the only enabled transitions in \(N^{\prime}\) in marking \(M_{i}{=}P_{i}\). Furthermore, since none of the transitions share any of their presets, the transitions can be fired in any order. Note that, by definition of the pattern, after all transitions have fired, we reach final marking \(M_{f}\) (which is a deadlock in the place-bordered system net). Hence, the labeled language described by the pattern equals \(\mathcal{L}_{\mathcal{Q}}(\kappa(t_{1}))\Rightarrow\mathcal{L}_{\mathcal{Q}}( \kappa(t_{2}))\cdots\Rightarrow\mathcal{L}_{\mathcal{Q}}(\kappa(t_{n}))\), which equals \(\wedge(\kappa(t_{1}),\kappa(t_{2}),...,\kappa(t_{n}))\). **Lemma 3** (\(\wedge\)-Pattern (Proposition 3) is Globally Language-Preserving).