# Translating Workflow Nets to Process Trees: An Algorithmic Approach
## Preliminaries
### Pattern Reduction  
In this section, we describe four patterns used to identify and replace process tree behavior. Furthermore, we propose a corresponding overarching reduction function, which shows how to reduce a PTree-WF-net containing any of these patterns. However, first, we present the general notion of a _feasible pattern_. Such a feasible pattern is a system net, formed by a _place-bordered fragment_ of a given PTree-net. Furthermore, the language of the unfolding of the system net needs to be equal to the language of the process tree it represents. We formalize the notion of a feasible pattern as follows. **Definition 8** (Feasible Pattern). : _Let \(\bigoplus\) denote the universe of process tree operators. Let \(N=(P,T,F,\kappa)\in\mathcal{N}_{\mathcal{Q}}\), let \(N^{\prime}=(P^{\prime},T^{\prime}=\{t_{1},...,t_{n}\}\), \(F^{\prime},k_{|T^{\prime}})\sqsubseteq N\) be a place-bordered fragment of \(N\) (\(N^{\prime}\sqsubseteq N\)) with correspondinginput places \(P_{i}^{\prime}\) and output places \(P_{o}^{\prime}\). Let \(M_{i}{=}P_{i}\) and \(M_{f}{=}P_{o}\). Given \(\oplus\in\bigoplus\), \(SN{=}(N^{\prime},M_{i},M_{f}){\in}\mathcal{SN}_{\mathcal{Q}}\) is a feasible \(\oplus\)-pattern, written \(\theta_{\oplus}(N,SN)\), iff:_  
\[\mathcal{L}_{\mathcal{Q}}\left(\oplus\left(\kappa\left(t_{1}\right),...,\kappa \left(t_{n}\right)\right)\right){=}\mathcal{L}_{\mathcal{N}}^{v}\left(\Lambda \left(N^{\prime}\right),M_{i},M_{f}\right) \tag{1}\]  
Observe that any place-bordered fragment of a WF-net that describes the same _local language_ as its corresponding process tree representation is a feasible pattern. As such, any feasible pattern is _locally language-preserving_. Transforming such a detected pattern within the given WF-net is straightforward, i.e., we add a new transition \(t^{\prime}\) to the WF-net with label \(\oplus\left(\kappa\left(t_{1}\right),...,\kappa\left(t_{n}\right)\right)\) and pre-set \(P_{i}\) and post-set \(P_{o}\). For example, consider the reduction of the choice construct between transitions \(t_{2}\) and \(t_{3}\) of Figure 3, i.e., depicted in Figure 6a, in which places \(p_{1}\) and \(p_{3}\) serve as the pre- and post-set of the newly added transition \(t_{2}^{\prime}\) with label \(\times(b,c)\). We formally define the notion of feasible pattern reduction as follows. **Definition 9** (Pattern Reduction). : _Let \(\oplus{\in}\{\rightarrow,\times,\wedge,\circlearrow\}\), let \(N{=}(P,T,F,\kappa){\in}\mathcal{N}_{\mathcal{Q}}\), let \(N^{\prime}{=}(P^{\prime},T^{\prime}{=}\left\{t_{1},...,t_{n}\right\},F^{\prime },\kappa|_{T^{\prime}}){\subseteq}N\) be a place-bordered fragment of \(N\) with corresponding input places \(P_{i}\) and output places \(P_{o}\). Let \(M_{i}{=}P_{i}\), \(M_{f}{=}P_{o}\) and let \(SN{=}\left(N^{\prime},M_{i},M_{f}\right)\) s.t. \(\theta_{\oplus}(N,SN)\). We let \(\Theta_{\oplus}(N,SN){=}N^{\prime\prime}{=}(P^{\prime\prime},T^{\prime\prime}, F^{\prime\prime},\kappa^{\prime})\) denote the \(\theta_{\oplus}(N,SN)\)-reduced PTree-net, with, for \(t^{\prime}{\
otin}T\):_  
\[P^{\prime\prime}{=}(P\backslash P^{\prime})\cup P_{i}\cup P_{o}\] \[T^{\prime\prime}{=}\left(T\backslash T^{\prime}\right)\cup\{t^{ \prime}\}\] \[F^{\prime\prime}{=}(F\backslash F^{\prime})\cup\{(p,t^{\prime}) \,|p{\in}P_{i}\}\cup\{(t^{\prime},p)\,|p{\in}P_{o}\}\] \[\kappa^{\prime}{=}\kappa|_{T\backslash T^{\prime}}\cup\{(t^{ \prime},\oplus(\kappa(t_{1}),...,\kappa(t_{n})))\}\]  
_A feasible pattern \(\theta_{\oplus}(N,SN)\) is globally language preserving iff \(\forall M,M^{\prime}{\in}\mathcal{M}(P^{\prime\prime})\left(\mathcal{L}_{ \mathcal{N}}^{v}(\Lambda(N),M,M^{\prime}){=}\mathcal{L}_{\mathcal{N}}^{v}( \Lambda(N^{\prime\prime}),M,M^{\prime})\right)\)_  
It is important to note that the notion of globally language-preserving is defined on the _unfolding_ of a net and its corresponding reduced net. For example, consider Figure 7. In the WF-net in Figure 7a, we observe concurrent behavior between a sequential construct between \(a\) and \(c\), and, activity \(b\).