# Translating Workflow Nets to Process Trees: An Algorithmic Approach
## Preliminaries
### Workflow Nets
A sequence of transition firings \(\sigma{=}\{t_{1},t_{2},...,t_{n}\}\) is a _firing sequence_ of \((N,M)\), yielding marking \(M^{\prime}\), written \((N,M)\xrightarrow{\sigma}_{N}(N,M^{\prime})\), iff \(\exists M_{1},M_{2},...,M_{n-1}{\in}\mathcal{M}(P)\) s.t. \((N,M)\xrightarrow{t_{1}}(N,M_{1})\xrightarrow{t_{2}}(N,M_{2})\cdots(N,M_{n-1}) \xrightarrow{t_{n}}(N,M^{\prime})\). We write \((N,M)\xrightarrow{\sigma}_{N}\circ\), in case \(\sigma\) is a firing sequence in \((N,M)\), yet, we are not interested in the marking it leads to. In some cases, we simply write \((N,M){\leadsto}(N,M^{\prime})\), if \(\exists\sigma{\in}T^{*}\left((N,M)\xrightarrow{\sigma}(N,M^{\prime})\right)\). \(\mathcal{L}_{\mathcal{N}}(N,M,M^{\prime})=\left\{\sigma{\in}T^{*}\mid(N,M) \xrightarrow{\sigma}_{N}(N,M^{\prime})\right\}\)  
Figure 3: WF-net \(W_{1}\)[1] with initial marking \([p_{i}]\) and final marking \([p_{o}]\). denotes all firing sequences starting from marking \(M\), leading to marking \(M^{\prime}\). The _labeled-language_ of \(N\), conditional to markings \(M\) and \(M^{\prime}\), is defined as \(\mathcal{L}_{\mathcal{N}}^{v}(N,M,M^{\prime}){=}\ell(\mathcal{L}_{\mathcal{N}} (N,M,M^{\prime})){\downarrow}_{\mathbb{Z}}\). Finally, \(\mathcal{R}(N,M)=\left\{M^{\prime}{\in}\mathcal{M}(P)\mid\exists\sigma{\in}T^{ *}\left((N,M)\xrightarrow{\sigma}(N,M^{\prime})\right)\right\}\) denotes the reachable markings. Given a Petri net \(N{=}(P,T,F,\ell)\), and a designated initial and final marking \(M_{i},M_{f}{\in}\mathcal{M}(P)\), the triple \(SN{=}(N,M_{i},M_{f})\) denotes a _system net_. As system net \(SN{=}(N,M_{i},M_{f})\) is formed by \(N\), we write \(SN\) as a replacement for \(N\), e.g., \((SN,M)\) denotes a marked system net. Clearly, \(\mathcal{R}(SN,M)\), \(\mathcal{L}_{\mathcal{N}}(SN,M,M^{\prime})\), etc., are readily defined for arbitrary markings \(M\), \(M^{\prime}{\in}\mathcal{M}(P)\). The _language_ of \(SN\) is referred to as \(\mathcal{L}_{\mathcal{N}}(SN,M_{i},M_{f})\), for which we simply write \(\mathcal{L}_{\mathcal{N}}(SN)\) (respectively, \(\mathcal{L}_{\mathcal{N}}^{v}(SN),\mathcal{R}(SN)\), etc. ), i.e., we drop \(M_{i}\) and \(M_{f}\) from the notation as they are clear from context. \(\mathcal{SN}\) denotes the universe of system nets. A WF-net is a special type of Petri net, i.e., it has one unique start and one unique end place. Furthermore, every place/transition in the net is on a path from the start to the end place. We formally define a WF-net as follows. **Definition 1** (Labeled Workflow net (WF-net)). : _Let \(\Sigma\) denote the universe of (activity) labels, let \(\tau{\
otin}\Sigma\) and let \(\ell\): \(T{\rightarrow}\Sigma{\cup}\{\tau\}\). Let \(N=(P,T,F,\ell){\in}\mathcal{N}\) and let \(p_{i}{\
eq}p_{o}{\in}P\). Tuple \(W{=}(P,T,F,p_{i},p_{o},\ell)\) is a Workflow net (WF-net), iff:_  
1. \(\bullet p_{i}{=}\mathcal{O}\wedge\
exists p{\in}P{\setminus}\{p_{i}\}\)__\((\bullet p{=}\mathcal{O})\)_;_ \(p_{i}\) _is the unique source place._
2. \(p_{o}{\bullet}{=}\mathcal{O}\wedge\
exists p{\in}P{\setminus}\{p_{o}\}\)__\((p{\bullet}{=}\mathcal{O})\)_;_ \(p_{o}\) _is the unique sink place._
3. _Each element_ \(x{\in}P{\cup}T\) _is on a path from_ \(p_{i}\) _to_ \(p_{o}\)_._  
_We let \(\mathcal{W}\) denote the universe of WF-nets._  
Observe that a WF-net is a system net with \(M_{i}{=}[p_{i}]\) and \(M_{f}{=}[p_{o}]\). Hence, since a WF-net is formed by an underlying Petri net, and, has a well-defined initial and final marking, i.e., \([p_{i}]\) and \([p_{o}]\), we write \(\mathcal{L}_{\mathcal{N}}(W)\) (respectively, \(\mathcal{L}_{\mathcal{N}}^{v}(W)\),\(\mathcal{R}(W)\), etc.) as a shorthand notation for \(\mathcal{L}_{\mathcal{N}}(W,[p_{i}],[p_{o}])\). Of particular interest are _sound WF-nets_, i.e., WF-nets that are guaranteed to be free of _deadlocks_, _livelocks_ and _dead transitions_. We formalize the notion of _soundness_ as follows. **Definition 2** (Soundness). : _Let \(W{=}(P,T,F,p_{i},p_{o},\ell){\in}\mathcal{W}\). \(W\) is sound iff:_  
1.