# Translating Workflow Nets to Process Trees: An Algorithmic Approach
## Preliminaries
### Pattern Reduction
#### 3.3.1. Sequential Pattern  
The \(\rightarrow\)-operator, i.e., \(\rightarrow(Q_{1},...,Q_{n})\), describes sequential behavior, hence, any subnet describing _strictly sequential behavior_, describes the same language. If a transition \(t_{1}\) always, uniquely, enables transition \(t_{2}\), which in turn enables transition \(t_{3},...,t_{n}\), and, whenever \(t_{1}\) has fired, the only way to consume all tokens from \(t_{1}\bullet\) is by means of firing \(t_{2}\), and, similarly, the only way to consume all tokens from \(t_{2}\bullet\) is by means of firing \(t_{3}\), etc. ; then, \(t_{1},...,t_{n}\) are in a sequential relation. We visualize the \(\rightarrow\)-pattern in the left-hand side of Figure 9. Note that, in the visualization, we omit \(P_{i}\) and \(P_{o}\), respectively, i.e., \(\bullet t_{1}\) and \(t_{n}\bullet\). We formally define the notion of a sequential pattern as follows  
**Proposition 1** (\(\rightarrow\)-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{<}n\)__\((|t_{i}|{\bullet}|{\geq}1{\wedge}t_{i}{\bullet}{=}{\bullet}t_{i+1})\)_, transition_ \(t_{i}\) _enables_ \(t_{i+1}\)_; and_
2. \(\forall 1{\leq}i{<}n\)__\((\forall p{\in}t_{i}\bullet(\bullet p{=}\{t_{i}\}){\wedge}p{\bullet}{=}\{t_{i+1}\}))_, enabling is unique,_  
_then, system net \(SN{=}(N^{\prime}{=}(P^{\prime},T^{\prime},F^{\prime},\kappa|_{T^{\prime}}), \bullet t_{1},t_{n}\bullet)\)__\((P_{i}{=}\bullet t_{1}\) and \(P_{o}{=}t_{n}\bullet)\), with \(P^{\prime}{=}{\bullet}t_{1}{\cup}{\bullet}t_{2}{\cup}\cdots{\bullet}t_{n}{\cup} t_{n}\bullet\), \(F^{\prime}{=}\{(x,y){\in}F\mid y{\in}T^{\prime}{\lor}x{=}t_{n}\}\), is a feasible \(\rightarrow\)-pattern._  
Proof. : Observe that \(t_{1}\) is the only enabled transition in marking \(M_{i}{=}P_{i}\). By definition of the proposed pattern, after firing \(t_{i}\) (\(1{\leq}i{<}n\)), the only enabled transition is \(t_{i+1}\). After firing \(t_{n}\), we reach the final marking \(M_{f}\), which is a deadlock marking (the only deadlock marking) of the place-bordered subnet. Hence, any firing sequence of \(\Lambda(N^{\prime})\) can be written as \(\sigma_{1}{\cdot}\sigma_{2}{\cdot}\cdots\sigma_{n}\), s.t., \((\Lambda(N^{\prime}),M_{i})\xrightarrow{\sigma_{1}}(\Lambda(N^{\prime}),t_{1} \bullet)\xrightarrow{\sigma_{2}}\cdots\xrightarrow{\sigma_{n}}(\Lambda(N^{ \prime}),M_{f})\). Observe that each element of \(\sigma_{1}\) is a transition in \(\lambda(\kappa(t_{1}))\), each element of \(\sigma_{2}\) is a transition in \(\lambda(\kappa(t_{2}))\), etc. Furthermore, by definition of \(\lambda\), \(\sigma_{1}\) is a firing sequence describing (when projected on its visible labels) a memmber of \(\mathcal{L}_{\mathcal{Q}}(\kappa(t_{1}))\), \(\sigma_{2}\) describes as sequence in \(\mathcal{L}_{\mathcal{Q}}(\kappa(t_{1}))\), etc. Hence, the set of all firing sequences projected on their visible labels equals \(\mathcal{L}_{\mathcal{Q}}(\rightarrow(\kappa(t_{1}),\kappa(t_{2}),\ldots, \kappa(t_{n})))\). **Lemma 1** (\(\rightarrow\)-Pattern (Proposition 1) is Globally Language-Preserving). : _Let \(N{=}(P,T,F,\kappa){\in}\mathcal{N}_{\mathcal{Q}}\) and let \(SN{=}(N^{\prime}{=}(P^{\prime},T^{\prime}{=}\{t_{1},t_{2},\ldots,t_{n}\},F^{ \prime},\kappa|_{T^{\prime}}),\bullet t_{1},t_{n}\bullet)\) s.t. \(\theta_{\rightarrow}(N,SN)\) according to Proposition 1. The feasible pattern \(\theta_{\rightarrow}(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}\). We need to prove that \(\forall M,M^{\prime}{\in}\mathcal{M}(P^{\prime\prime})\) (\(\mathcal{L}_{N}^{v}(\Lambda(N),M,M^{\prime}){=}\mathcal{L}_{N^{\prime}}^{v}( \Lambda(N^{\prime\prime}),M,M^{\prime})\)).