Well-Formed Free-Choice Petri Nets Revisited

TL;DR

The paper addresses characterizing well-formed free-choice Petri nets, i.e., nets that admit a marking $M_0$ which is live and bounded. It introduces semi-T-components and their dual semi-S-components as structural proxies, revealing a symmetry between place- and transition-centric views and enabling a dual characterization of well-formedness. It proves that in strongly connected free-choice nets (and in well-formed nets) semi-T-components align with T-components and semi-S-components with S-components, recovering classical S-coverability and T-coverability results and the Hack duality that the reverse-dual net $\,\mathrm{rd}(N)\,$ is well-formed whenever $N$ is. The paper then presents a polynomial-time algorithm for deciding well-formedness based on allocations and bottom SCCs of induced subnets, placing the approach in relation to Rank-based methods. Overall, it provides symmetry-driven, concise proofs and practical graph-theoretic tools for verifying well-formedness in free-choice nets with potential implications for verification and synthesis of concurrent systems.

Abstract

The theory of free-choice Petri nets is an established field, initiated in the 1970s by Commoner and Hack at MIT. We revisit well-formed free-choice nets (those admitting markings that are both live and bounded) and provide a new characterization by introducing semi-T-components. This notion is dual to that of semi-S-components, which in turn correspond to the well-known minimal siphons. By highlighting the symmetry between these dual concepts, we derive the classical coverability theorems for T- and S-components, as well as the duality theorem -- stating that a free-choice net is well-formed if and only if its reverse-dual is also well-formed -- using arguments that are as symmetric as possible.

Theorems & Definitions (4)

• Definition 2.1: Place/transition Petri net, preset, postset, notation $N=(S_N,T_N,F_N)$
• Remark 2.2
• Definition 2.3: Subnet and the dot notation
• Definition 2.4: Marking, enabling, firing, effect $\Delta(\sigma)$, execution $M\xrightarrow{\sigma}$, reachability set $[M_0\rangle$] A marking of a net $N = (S, T, F)$ is a function $M \colon S \to \mathbb{N}$, attaching a number $M(s)$ of tokens (the marking of $s$) to each place $s \in S$. The symbol $\mathbf{0}$ denotes the zero marking, defined as $\mathbf{0}(s) = 0$ for all $s \in S$. For any $S' \subseteq S$, we may write $M|_{S'} = \mathbf{0}$ as a shorthand for $M|_{S'} = \mathbf{0}|_{S'}$; in this case, we also say that $S'$ is unmarked at $M$. A transition $t \in T$ is enabled at a marking $M$ if $M(s) \geq 1$ for all places $s \in {}^\bullet{t}$; this is denoted by $M \xrightarrow{t}$. The effect $\Delta(t) \colon S \to \mathbb{Z}$ of a transition $t$ is defined as: $\Delta(t)(s) = -1$ if $s \in {}^\bullet{t} \setminus {t}^\bullet$, $\Delta(t)(s) = +1$ if $s \in {t}^\bullet \setminus {}^\bullet{t}$, and $\Delta(t)(s) = 0$ otherwise. An enabled transition $t \in T$ may fire at a marking $M$, leading to a new marking $M' = M + \Delta(t)$; this is denoted by $M \xrightarrow{t} M'$. We extend this notation to $M \xrightarrow{\sigma}$ for firing sequences $\sigma \in T^* \cup T^\omega$, and to $M \xrightarrow{\sigma} M'$ for finite sequences $\sigma \in T^*$ (defined inductively by $M \xrightarrow{\varepsilon} M$, and $M \xrightarrow{\sigma t} M"$ if $M \xrightarrow{\sigma} M'$ and $M' \xrightarrow{t} M"$). Note that for $M \xrightarrow{\sigma} M'$ we have $M'=M+\Delta(\sigma)$, where $\Delta(t_1t_2\cdots t_m)=\sum_{i=1}^m\Delta(t_i)$. We also refer to $M \xrightarrow{\sigma}$ or $M \xrightarrow{\sigma} M'$ as an execution of $N$, which may be finite or infinite. For an (initial) marking $M_0$, we define its reachability set (the set of all markings reachable from $M_0$) as $[M_0\rangle = \{ M \mid M_0 \xrightarrow{\sigma} M \text{ for some } \sigma \in T^* \}.$ A non-strongly connected net consisting of two SCCs separated by the dashed arcs. Given a net $N=(S,T,F)$, a marking $M_0$ is bounded if its reachability set $[M_0\rangle$ is finite; that is, if there exists a bound $b\in\mathbb{N}$ such that $M(s)\leq b$ for all $M\in[M_0\rangle$ and all places $s\in S$. In this case we also say that the system $(N,M_0)$ is bounded. A transition $t\in T$ is live at a marking $M$ if for every marking $M' \in [M\rangle$, there exists a firing sequence $\sigma \in T^*$ such that $M' \xrightarrow{\sigma t}$. A marking $M_0$ is live if every transition $t \in T$ is live at $M_0$. In this case we also say that the system $(N,M_0)$ is live. A net $N$ is well-formed if there exists a marking $M_0$ that is live and bounded (that is, the system $(N, M_0)$ is both live and bounded). Given a net $N=(S,T,F)$, a transition $t \in T$ is dead at a marking $M$ if there is no firing sequence $\sigma \in T^*$ such that $M \xrightarrow{\sigma t}$. A marking $M$ is called a DL-marking if every transition $t \in T$ is either dead or live at $M$, and at least one transition is dead. A particular DL-marking is a dead marking (or a deadlock); that is, a marking $M$ at which all transitions are dead, provided that $T\neq\emptyset$. Note that, by definition, a transition $t \in T$ is not live at $M$ if and only if $t$ is dead at some $M' \in [M\rangle$. We recall some further standard facts: Given a net $N=(S,T,F)$ with $T \neq \emptyset$: If a marking $M_0$ is live, then every $M \in [M_0\rangle$ is also live. Consequently, there exists an infinite execution $M_0 \xrightarrow{\sigma}$ in which every transition $t \in T$ fires infinitely often.A marking $M_0$ is live if and only if no DL-marking is reachable from $M_0$. Proof: 1. This follows immediately from the definition of liveness: if $M_0$ is live, every transition must remain fireable from any reachable marking. The existence of the infinite sequence is a direct consequence of this property. 2. ($\Rightarrow$) If $M_0$ is live, every $t \in T$ is live at every $M \in [M_0\rangle$. Since a DL-marking requires at least one transition to be dead, no such marking can be reachable. ($\Leftarrow$) Let $L(M)$ and $D(M)$ denote the sets of transitions that are live and dead at $M$, respectively. Note that for any $M' \in [M\rangle$, we have $L(M) \subseteq L(M')$ and $D(M) \subseteq D(M')$. Moreover, for any transition $t \in T \setminus (L(M) \cup D(M))$, there exists $M' \in [M\rangle$ such that $t \in D(M')$. This readily implies that if $M_0$ is not live (that is, there exists $t \in T \setminus L(M_0)$), then a DL-marking $M$ is necessarily reachable from $M_0$. $\sqcap$$\sqcup$ =0 Figure \ref{['fig:wf_sc']} shows a net $N$ with five places and four transitions. As is standard, places are represented by circles and transitions by boxes. The graph of $N$ has two SCCs (a top SCC on the left and a bottom SCC on the right). The figure also depicts a marking $M_0$ of $N$, where each place contains a number of black tokens; this marking can be represented as the vector $(0,0,1,1,0)$. An execution of $N$ is, for instance: $(0,0,1,1,0) \xrightarrow{t_2} (1,0,0,0,1) \xrightarrow{t_1t_3} (0,0,1,1,1) \xrightarrow{t_2t_1t_3} (0,0,1,1,2) \xrightarrow{t_1t_4} (0,0,0,0,2).$ The execution demonstrates that $(N, M_0)$ is neither bounded (consider $\sigma=(t_2t_1t_3)^\omega$) nor live; the marking $(0,0,0,0,2)$ is a DL-marking, at which even all transitions are dead. We may also note that each SCC constitutes a well-formed subnet. However, if the arc $(t_2, s_2)$ or $(s_2, t_2)$ were added, the top SCC would no longer be well-formed. Theorem \ref{['th:wfImpSc']} provides an alternative proof of a well-known result (cf. Theorem 2.25 in de95). This proof is based on Proposition \ref{['prop:omitBotSCC']}, which deals with bottom SCCs; the proposition is also utilised in Section \ref{['sec:main']}. We note that while our current context is limited to plain nets, the proof remains valid for nets with weighted arcs as well. Let $B$ be a bottom SCC of a net $N$. For any execution $M \xrightarrow{\sigma}$ of $N$, whether finite or infinite, there exists an execution $M\xrightarrow{\sigma'}$, where $\sigma'$ is obtained from $\sigma$ by omitting all transitions from $T_B$; that is, $\sigma'=\sigma|_{T'}$ for $T'=T_N\setminus T_B$. Proof: Let $B$ be a bottom SCC of $N$; we define $S'=S_N\setminus S_B$ and $T'=T_N\setminus T_B$. Since $B$ is a bottom SCC, for each $t\in T_B$ we have ${t}^\bullet\subseteq S_B$. Consequently, $\Delta(w)|_{S'}\leq \mathbf{0}$ for all transition sequences $w\in (T_B)^*$; that is, $\Delta(w)(s)\leq 0$ for all $s\in S'$. On the other hand, for each $t'\in T'$, we have ${}^\bullet{t'}\subseteq S'$. Suppose, for the sake of contradiction, that $M\xrightarrow{\sigma}$ is an execution but $M\xrightarrow{\sigma'}$ is not; that is, $\sigma'=\sigma|_{T'}$ is not enabled at $M$. Then $\sigma$ must have a finite prefix $w_0t'_1w_1t'_2\cdots w_{m-1}t'_mw_mt'_{m+1}$ with $w_i\in(T_B)^*$ for all $i\in[0,m]$ and $t'_j\in T'$ for all $j\in[1,m{+}1]$, such that $M\xrightarrow{w_0t'_1w_1t'_2\cdots w_{m-1}t'_mw_m}M'\xrightarrow{t'_{m+1}}$, $M\xrightarrow{t'_1t'_2\cdots t'_m}M"$, and $t'_{m+1}$ is disabled at $M"$. Since $M"=M'-\Delta(w_0w_1\cdots w_m)$ and $\Delta(w_0w_1\cdots w_m)|_{S'}\leq\mathbf{0}$, it follows that $M"|_{S'}\geq M'|_{S'}$. Since $M'\xrightarrow{t'_{m+1}}$ and ${}^\bullet{t'_{m+1}}\subseteq S'$, the transition $t'_{m+1}$ must also be enabled at $M"$, yielding a contradiction. $\sqcap$$\sqcup$ =0 In a well-formed net, every bottom SCC is also a top SCC. Consequently, every well-formed net is either strongly connected or consists of a collection of pairwise unconnected, strongly connected well-formed components. Proof: Let $B$ be a bottom SCC of a net $N$ that is not a top SCC; hence, $F_N$ contains an arc $(x,y)$ such that $x\notin S_B\cup T_B$ and $y\in S_B\cup T_B$. We aim to show that $N$ is not well-formed. Specifically, we demonstrate that the existence of an infinite execution $M\xrightarrow{\sigma}$ of $N$ satisfying $T^\sigma_\infty=T_N$ (where $T^\sigma_\infty$ denotes the set of transitions occurring infinitely often in $\sigma$) implies that the marking $M$ is unbounded. Since such an infinite execution must exist for every live marking $M$, it follows that $N$ cannot possess a marking that is both live and bounded. We consider an infinite execution $M\xrightarrow{\sigma}$ of $N$ satisfying $T^\sigma_\infty=T_N$, and show that the reduced execution $M\xrightarrow{\sigma'}$ with $\sigma'=\sigma|_{T_N\setminus T_B}$ (which exists by Proposition \ref{['prop:omitBotSCC']}) demonstrates that $M$ is unbounded. We fix an arc $(x,y)$ such that $x\notin S_B\cup T_B$ and $y\in S_B\cup T_B$, and distinguish two cases based on the type of the arc $(x,y)$ (the two types are demonstrated by the arcs $(t_2,s_5)$ and $(s_2,t_4)$ in Figure \ref{['fig:wf_sc']}): Case 1: $x$ is a transition, and $y$ is a place ($x\in T_N\setminus T_B$, and $y\in S_B$). In the reduced execution $M\xrightarrow{\sigma'}$, the marking of $y$ is infinitely often increased (whenever $x$ fires). Since $B$ is a bottom SCC, we have ${y}^\bullet\subseteq T_B$. Because no transitions from $T_B$ occur in $\sigma'$, the marking of $y$ is never decreased in the execution $M\xrightarrow{\sigma'}$, and thus grows above any bound. Case 2: $x$ is a place, and $y$ is a transition ($x\in S_N\setminus S_B$, and $y\in T_B$). In the original execution $M\xrightarrow{\sigma}$, the marking of $x$ is infinitely often decreased by $y\in T_B$ and never increased by any transition from $T_B$, since ${}^\bullet{x}\cap T_B=\emptyset$. Hence, the reduced execution $M\xrightarrow{\sigma'}$ omits infinitely many decreases of the marking of $x$ while keeping all increases. This causes the marking of $x$ to grow above any bound in $M\xrightarrow{\sigma'}$. $\sqcap$$\sqcup$ =0 We recall the standard definition of free-choice nets. These nets are composed of interconnected subnets called clusters. See Figure \ref{['fig:five_clusters_and_bott_scc']} for an example. A net $N$ is a free-choice net if ${}^\bullet{t_1}\cap{}^\bullet{t_2}\neq\emptyset$ implies ${}^\bullet{t_1} = {}^\bullet{t_2}$, for all $t_1, t_2\in T_N$. A cluster of $N$ is a subnet $C = N[S_C \cup T_C]$ such that ${s}^\bullet = T_C$ for every $s \in S_C$ and ${}^\bullet{t} = S_C$ for every $t \in T_C$, where $S_C \cup T_C$ is an inclusion-maximal set satisfying this property. By $\mathbb{C}_{N}$ we denote the set of clusters of a free-choice net $N$. For any node $x\in S_N\cup T_N$, let $C(x)\in\mathbb{C}_N$ denote the cluster containing $x$. The inclusion-maximality ensures that all places $s$ with ${s}^\bullet=\emptyset$ belong to a single cluster; analogously, the same applies to all transitions $t$ with ${}^\bullet{t}=\emptyset$. Note the following standard (and easily verifiable) facts, where item 1 confirms that the cluster $C(x)$ is well-defined. Given a free-choice net $N$: The set of nodes $S_N\cup T_N$ is partitioned into clusters; that is, each $x\in S_N\cup T_N$ belongs to exactly one cluster $C(x)\in\mathbb{C}_N$.Any subnet of $N$ is itself a free-choice net.For any marking $M$ and any cluster $C\in\mathbb{C}_N$, either all transitions in $T_C$ are enabled at $M$, or none of them are. To understand well-formed free-choice nets, it suffices to consider strongly connected free-choice nets (by Theorem \ref{['th:wfImpSc']}) that contain at least one place and at least one transition (as other cases are trivial). In such nets, each cluster necessarily contains at least one transition and at least one place. In light of the all-or-none property (Proposition \ref{['prop:subFree']}(3)), it proves useful to examine subnets formed by selecting exactly one transition from each cluster and removing all transitions not chosen. Given a free-choice net $N$ where each cluster contains at least one transition, an allocation is a function $\alpha: \mathbb{C}_N \rightarrow T_N$ such that $\alpha(C)\in T_C$ for each cluster $C$. Given an allocation $\alpha$, we denote by $N_\alpha$ the subnet induced by the set $S_N$ of all places of $N$ and the set $T_{N_\alpha}=\{\alpha(C)\mid C\in\mathbb{C}_N\}$ of all chosen transitions. An allocation $\alpha$ is directed to a node $u \in S_N \cup T_N$ if from every node of $N_\alpha$ there is a path to $u$ in $N_\alpha$ (which implies that $u\in S_N\cup T_{N_\alpha}$). It is a directed allocation if it is directed to some node (that is, if $N_\alpha$ has exactly one bottom SCC). By the definition above, an allocation is a transition-allocation $\alpha$ which selects exactly one transition from each cluster. We will be particularly concerned with the bottom SCCs $Y$ of the nets $N_\alpha$. As a motivating observation, anticipating the duality to be discussed later, we note that it will subsequently be shown (see Proposition \ref{['prop:MDLtopSCC']}) that for every DL-marking $M$, there exists a top SCC $X$ of $N_\beta$ such that $M|_{S_X}=\mathbf{0}$, where $\beta$ is a place-allocation selecting one place in each cluster. We will observe that any strongly connected free-choice net $N$ (with $T_N\neq\emptyset$) is covered by the bottom SCCs of its subnets $N_\alpha$ induced by directed allocations $\alpha$. This motivates the following definition of semi-T-components of $N$, which correspond to the bottom SCCs of the subnets $N_\alpha$. We introduce this notion for general nets as an extension of the standard notion of T-components. It will turn out that for well-formed free-choice nets, every semi-T-component is in fact a T-component. A subnet $Y$ of a net $N$ is a semi-T-component of $N$ if $T_Y \neq \emptyset$ and the following conditions hold (where the pre- and post-functions "${}^\bullet{}$" refer to $N$, by our convention): $Y$ is strongly connected (which implies $S_Y\subseteq {}^\bullet{T_Y}\cap{T_Y}^\bullet$);$|{s}^\bullet \cap T_Y|=1$ for each $s\in S_Y$ (note that $|{}^\bullet{s} \cap T_Y|\geq 1$ follows from strong connectivity);${T_Y}^\bullet\subseteq S_Y$ (hence ${T_Y}^\bullet=S_Y\subseteq{}^\bullet{T_Y}$). The upper panel of Figure \ref{['fig:five_clusters_and_bott_scc']} shows a semi-T-component in bold. The lower panel highlights another semi-T-component in bold (the wavy arcs will be discussed later); in this case, it is explicitly depicted as the bottom SCC of $N_\alpha$ for a directed allocation $\alpha$. The upper panel shows a strongly connected free-choice net $N$ with five clusters, highlighting a proper semi-T-component of Type II but not Type I. The lower panel illustrates the net $N_{\alpha}$, where the set of $\alpha$-allocated transitions is $\{t_{11}, t_{21}, t_{31}, t_{42}, t_{51}\}$. Its bottom SCC (depicted in bold) is a proper semi-T-component of Type I ( with $(t_{21}, s_{11})$ viewed as an "excessive arc") and also of Type II (due to the "inbound arc" $(s_{32}, t_{31})$). Given a free-choice net $N$ where each cluster contains at least one transition, a subnet $Y$ is a semi-T-component of $N$ if and only if $Y$ is a bottom SCC of $N_\alpha$ for some allocation $\alpha$. If $N$ is, moreover, strongly connected, then any semi-T-component is the bottom SCC of $N_\alpha$ for some directed allocation $\alpha$. Proof: We start with the "if" direction ($\Leftarrow$) of the claimed equivalence. Let $B$ be a bottom SCC of $N_\alpha$ for some allocation $\alpha$; by definition, $S_B\cup T_B\neq \emptyset$ and the subnet $B$ is strongly connected. Since $\alpha$ is an allocation, each cluster of $N_\alpha$ contains precisely one transition. For any place $s \in S_N$, let $t_s$ denote its unique successor in $N_\alpha$, that is, the single transition satisfying $(s,t_s) \in F_{N_\alpha}$. Since $B$ is a bottom SCC, no arcs in $N_\alpha$ leave $B$. Thus, for each $s \in S_B$, we have $t_s \in T_B$, which implies $|{s}^\bullet \cap T_B| = 1$. Together with $S_B\cup T_B\neq \emptyset$, this also ensures $T_B \neq \emptyset$ (even if $S_B=\emptyset$). Finally, since there are no arcs $(t,s)\in F_N$ such that $t\in T_B$ and $s\notin S_B$, we have ${T_B}^\bullet \subseteq S_B$. We have established that $B$ is a semi-T-component. For the "only-if" direction ($\Rightarrow$), let $Y$ be a semi-T-component of $N$. Since $|{s}^\bullet\cap T_Y|=1$ for each $s\in S_Y$, every cluster of $N$ contains at most one transition from $T_Y$. We define an allocation $\alpha$ such that $\alpha(C) = t$ whenever $T_C \cap T_Y = \{t\}$, and $\alpha(C)$ is chosen arbitrarily if $T_C \cap T_Y = \emptyset$. Then $Y$ is a strongly connected subnet of $N_\alpha$, and since no arc leaves $Y$ in $N_\alpha$ (as ${T_Y}^\bullet \subseteq S_Y$), $Y$ is a bottom SCC of $N_\alpha$. Moreover, if $N$ is strongly connected and we choose $\alpha$ so that $\alpha(C)$ is a transition from $T_C$ with the shortest distance to $Y$ (thus $\alpha(C) = t$ whenever $T_C \cap T_Y = \{t\}$), then $\alpha$ is a directed allocation and $Y$ is the bottom SCC of $N_\alpha$. $\sqcap$$\sqcup$ =0 Every strongly connected free-choice net $N$ is covered by its semi-T-components; that is, each $t\in T_N$ belongs to $T_Y$ for some semi-T-component $Y$ of $N$. Proof: Given a strongly connected free-choice net $N$ and $t_0 \in T_N$, we define an allocation $\alpha$ such that for each cluster $C$, $\alpha(C)$ is a transition in $T_C$ with a shortest distance to $t_0$ in the graph $N$. In particular, $\alpha(C(t_0)) = t_0$. By this construction, from every node in $N_\alpha$ there exists a path to $t_0$ in $N_\alpha$. Hence $\alpha$ is a directed allocation, and $t_0$ belongs to the bottom SCC of $N_\alpha$, which is a semi-T-component of $N$ by Proposition \ref{['prop:botSemiT']}. $\sqcap$$\sqcup$ =0 Now we recall the standard definition of T-components for general nets. They are special cases of semi-T-components, which leads us to introduce the notion of proper semi-T-components. It will turn out that proper semi-T-components do not occur in well-formed free-choice nets; consequently, these nets are covered by T-components. A subnet $Y$ of a net $N$ is a T-component of $N$ if $T_Y \neq \emptyset$ and the following conditions hold: $Y$ is strongly connected;$|{s}^\bullet \cap T_Y| = 1 = |{}^\bullet{s} \cap T_Y|$ for each $s \in S_Y$;${T_Y}^\bullet = S_Y = {}^\bullet{T_Y}$. A semi-T-component $Y$ of $N$ is proper if it is not a T-component. By the definition of semi-T-components, such $Y$ must be of Type I, Type II, or both, where these types are defined as follows: Type I (informally called "excessive arc"): $|{}^\bullet{s} \cap T_Y| \geq 2$ for some $s \in S_Y$ (that is, $s$ has more than one input arc in $Y$);Type II ("inbound arc"): ${}^\bullet{T_Y} \setminus {T_Y}^\bullet\neq\emptyset$, that is, there is an arc $(s,t)\in F_N$ such that $s\notin S_Y={T_Y}^\bullet$ and $t\in T_Y$. In Figure \ref{['fig:five_clusters_and_bott_scc']}, the upper panel highlights a proper semi-T-component of Type II but not Type I. The lower panel shows a proper semi-T-component $Y$ that is of both Type I (since $|{}^\bullet{s_{11}} \cap T_Y| \geq 2$) and Type II (since $s_{32}\in{}^\bullet{T_Y} \setminus {T_Y}^\bullet$). If $N$ is a well-formed free-choice net, then each semi-T-component of $N$ is a T-component. Proof: Let $N$ be a well-formed free-choice net and $Y$ a semi-T-component of $N$; we aim to show that $Y$ is in fact a T-component. W.l.o.g. we assume that $N$ is strongly connected (recall Theorem \ref{['th:wfImpSc']}). As $T_Y \neq \emptyset$, the net $N$ is not a single place; hence, the strong connectivity of $N$ ensures that every cluster in $N$ contains at least one transition. We choose a directed allocation $\alpha:\mathbb{C}_N\to T_N$ such that $Y$ is the bottom SCC of $N_\alpha$, which is possible by Proposition \ref{['prop:botSemiT']}. Let $M_0$ be a live and bounded marking of $N$ (which exists, since $N$ is well-formed). We note that $(N_\alpha,M_0)$ is deadlock-free. Indeed, if there were an execution $M_0\xrightarrow{\rho}M$ of $N_\alpha$ where $M$ is a dead marking (meaning that each cluster $C$ contains a place $s$ with $M(s)=0$), then $M_0\xrightarrow{\rho}M$, as an execution of $N$, would contradict the assumption that $(N,M_0)$ is live. We can thus fix an arbitrary infinite execution $M_0 \xrightarrow{\sigma}$ of $N_\alpha$. Let $T^\sigma_\infty$ denote the nonempty set of transitions occurring infinitely often in $\sigma$. Due to the boundedness of $M_0$, if $t\in T^\sigma_\infty$ and ${t}^\bullet\cap S_C\neq\emptyset$ for some cluster $C$, then the transition $\alpha(C)$ must also belong to $T^\sigma_\infty$ (otherwise tokens would accumulate indefinitely in $S_C$ throughout the execution $M_0\xrightarrow{\sigma}$). Hence, if $t\in T^\sigma_\infty$ and there is a path from $t$ to $t'$ in $N_\alpha$, then $t'\in T^\sigma_\infty$. Our construction of $\alpha$ as an allocation directed to the bottom SCC $Y$ thus guarantees that $T_Y\subseteq T^\sigma_\infty$. Let $\sigma'$ arise from $\sigma$ by omitting all transitions from $T_Y$, that is, $\sigma'=\sigma|_{T_N\setminus T_Y}$. Since $Y$ is a bottom SCC of $N_\alpha$, $M_0 \xrightarrow{\sigma'}$ is also an execution of $N_\alpha$ (by Proposition \ref{['prop:omitBotSCC']}). Furthermore, $\sigma'$ must be finite; otherwise, we would derive $T_Y\subseteq T^{\sigma'}_\infty$ as before, which contradicts the definition of $\sigma'$. We thus obtain $T^\sigma_\infty=T_Y$. This excludes the possibility that $Y$ is a proper semi-T-component of Type II (inbound arc). Indeed, if there were a place $s\in {}^\bullet{T_Y}\setminus {T_Y}^\bullet$, then in the execution $M_0 \xrightarrow{\sigma}$, the marking of $s$ would be infinitely often decreased (by transitions from $T_Y$) while only finitely many times increased (by transitions in $\sigma'$), which contradicts the boundedness of $(N,M_0)$. Hence, ${T_Y}^\bullet=S_Y={}^\bullet{T_Y}$. It remains to exclude that $Y$ is a proper semi-T-component of Type I. For the sake of contradiction, let $s_0$ be a place in $S_Y$ and $t_1,t_2$ be two distinct transitions in $T_Y$ such that $\{t_1,t_2\}\subseteq{}^\bullet{s_0}$. In this case, we consider a simple cycle in the strongly connected subnet $Y$ that contains the arc $(t_1,s_0)$. Such a cycle exists because there is a simple path from $s_0$ to $t_1$ in $Y$; moreover, the cycle cannot contain the arc $(t_2, s_0)$. Let $S'\subseteq S_Y$ and $T'\subseteq T_Y$ denote the sets of places and transitions in this cycle, respectively. For each $t\in T'$, we have $|{}^\bullet{t}\cap S'|=1\leq |{t}^\bullet\cap S'|$. For each $t\in T_Y\setminus T'$, we have $|{}^\bullet{t}\cap S'|=0\leq |{t}^\bullet\cap S'|$ (recall that each cluster contains at most one transition from $T_Y$). Crucially, for the transition $t_2 \in T_Y$, we have a strict inequality: if $t_2 \in T'$, then $|{}^\bullet{t_2} \cap S'| = 1 < 2 \leq |{t_2}^\bullet \cap S'|$ (due to the arc $(t_2,s_0)$ and the arc $(t_2,s)$ belonging to the cycle, where $s\neq s_0$); otherwise, $|{}^\bullet{t_2} \cap S'| = 0 < 1 \leq |{t_2}^\bullet \cap S'|$. Since $T_Y=T^\sigma_\infty$, the strict imbalance at $t_2$ ensures that the sum of tokens on the set $S'$ increases above any bound in the execution $M_0 \xrightarrow{\sigma}$, which contradicts the boundedness of $(N, M_0)$. $\sqcap$$\sqcup$ =0 The following lemma summarises the crucial points of the previous propositions and proofs. (In this paper, we regard a lemma as a crucial step towards the main theorem; it is typically built upon several supporting propositions.) Every well-formed free-choice net $N$ is covered by T-components, that is, each $t\in T_N$ is in $T_Y$ for some T-component $Y$ of $N$. A set of such T-components covering $N$ can be constructed in polynomial time. Moreover, there is no proper semi-T-component in $N$. Proof: The first claim (the T-coverability theorem) and the last claim follow from the facts that every strongly connected free-choice net $N$ is covered by semi-T-components (Proposition \ref{['prop:semiTcover']}), and that each semi-T-component is a T-component if $N$ is, moreover, well-formed (Proposition \ref{['prop:noProperSemiT']}). The construction of an allocation directed to $t_0\in T_N$, and of the bottom SCC containing $t_0$, in the proof of Proposition \ref{['prop:semiTcover']}, is clearly polynomial in the size of the net $N$. This implies the second claim of the lemma. $\sqcap$$\sqcup$ =0 A non-well-formed net coverable by T-components (one of them is highlighted in bold on the left, the second one is symmetric) and a proper semi-T-component (highlighted in bold on the right) of both Type I (excessive input arc at $s_1$) and Type II (inbound arcs $(s_5,t_6)$ and $(s_6,t_7)$). Figure \ref{['fig:not_wf_covered']} shows a net $N$ that is covered by T-components (as well as by S-components defined below). The net has also a proper semi-T-component, which indicates that it is not well-formed. The T-components have a natural counterpart: the S-components. For defining S-components, as well as semi-S-components, the concept of reverse-dual nets is convenient; it consists in exchanging the roles of places and transitions while reversing the arcs between them. Let $N = (S,T,F)$ be a net. The reverse-dual net of $N$ is the net $\mathit{rd}(N)=(T,S,F^{-1})$. The next proposition highlights some simple observations: Let $N$ be a net. Then: $\mathit{rd}(\mathit{rd}(N))=N$.If $N$ is strongly connected, then so is $\mathit{rd}(N)$.If $N$ is free-choice, then so is $\mathit{rd}(N)$; moreover, if $C$ is a cluster of $N$, then $\mathit{rd}(C)$ is a cluster of $\mathit{rd}(N)$. We could use Proposition \ref{['prop:ScorrespT']} (below) as a definition of "S-notions", but for better transparency we provide an explicit definition, by which Proposition \ref{['prop:ScorrespT']} becomes a straightforward observation. A subnet $X$ of a net $N$ is a semi-S-component of $N$ if $S_X \neq \emptyset$ and the following conditions hold: $X$ is strongly connected (which implies $T_X\subseteq {}^\bullet{S_X}\cap{S_X}^\bullet$);$|{}^\bullet{t} \cap S_X|=1$ for each $t\in T_X$ (note that $|{t}^\bullet \cap S_X|\geq 1$ follows from strong connectivity);${}^\bullet{S_X}\subseteq T_X$ (hence ${}^\bullet{S_X}=T_X\subseteq{S_X}^\bullet$). If b) is strengthened to "$|{}^\bullet{t} \cap S_X|=1=|{t}^\bullet \cap S_X|$ for each $t\in T_X$" and c) is strengthened to "${}^\bullet{S_X}=T_X={S_X}^\bullet$", then $X$ is an S-component. A semi-S-component $X$ of $N$ is proper if it is not an S-component. Such $X$ must be of Type I, Type II, or both, where these types are defined as follows: Type I (informally called "excessive arc"): $|{t}^\bullet \cap S_X| \geq 2$ for some $t \in T_X$ (that is, $t$ has more than one output arc in $X$);Type II ("outbound arc"): ${S_X}^\bullet \setminus {}^\bullet{S_X}\neq\emptyset$, that is, there is an arc $(s,t)\in F_N$ such that $s\in S_X$ and $t\notin T_X={}^\bullet{S_X}$. A subnet $X$ of a net $N$ is an S-component (a semi-S-component, a proper semi-S-component, of Type I and/or Type II) of $N$ if and only if $\mathit{rd}(N)[S_X\cup T_X]$ is a T-component (a semi-T-component, a proper semi-T-component, of Type I and/or Type II) of $\mathit{rd}(N)$. Using Propositions \ref{['prop:rdProp']} and \ref{['prop:ScorrespT']}, we can readily derive Propositions \ref{['prop:topSemiS']} and \ref{['prop:semiScover']}, the analogues of Propositions \ref{['prop:botSemiT']} and \ref{['prop:semiTcover']}, after introducing the notion of place-allocations, an analogue of (transition-)allocations. Given a free-choice net $N$ where each cluster contains at least one place, a place-allocation is a function $\beta: \mathbb{C}_N \rightarrow S_N$ such that $\beta(C)\in S_C$ for each cluster $C$. Given a place-allocation $\beta$, we denote by $N_\beta$ the subnet induced by the set $T_N$ of all transitions of $N$ and the set $S_{N_\beta}=\{\beta(C)\mid C\in\mathbb{C}_N\}$ of all chosen places. A place-allocation $\beta$ is co-directed from a node $u \in S_N \cup T_N$ if for every node $v$ of $N_\beta$ there is a path from $u$ to $v$ in $N_\beta$ (which implies that $u\in S_{N_\beta}\cup T_{N}$). It is a co-directed allocation if it is co-directed from some node (that is, if $N_\beta$ has exactly one top SCC). Given a free-choice net $N$ where each cluster contains at least one place, a subnet $X$ is a semi-S-component of $N$ if and only if it is a top SCC of $N_\beta$ for some place-allocation $\beta$. If $N$ is, moreover, strongly connected, then any semi-S-component is the top SCC of $N_\beta$ for some co-directed place-allocation $\beta$. Every strongly connected free-choice net $N$ is covered by its semi-S-components; that is, each $s\in S_N$ belongs to $S_X$ for some semi-S-component $X$ of $N$. The above discussed duality is illustrated in Figure \ref{['fig:five_clusters_dual']}. A reverse-dual net $\mathit{rd}(N)$ of the net $N$ from Figure \ref{['fig:five_clusters_and_bott_scc']} (top panel). The blue subnet depicts the net $N_{\beta}$ where $\{s_{11}, s_{21}, s_{31}, s_{42}, s_{51}\}$ is the set of $\beta$-allocated places. Its top SCC (depicted in bold) is a semi-S-component of Type I (due to the "excessive arc" $(t_{11}, s_{21})$) and also of Type II (due to the "outbound arc" $(s_{31}, t_{32})$). It is now tempting to formulate S-coverability of well-formed free-choice nets as an analogue of T-coverability (Lemma \ref{['lem:Tcover']}). However, we cannot readily confirm that proper semi-S-components do not exist in well-formed free-choice nets; that is, an analogue of Proposition \ref{['prop:noProperSemiT']} is not immediate. Nevertheless, the following proposition is immediate. If $N$ is a free-choice net such that its reverse-dual net $\mathit{rd}(N)$ is well-formed, then each semi-S-component of $N$ is an S-component. This implies that $N$ is covered by S-components (that is, each $s\in S_N$ is in $S_X$ for some S-component $X$ in $N$). The issue of S-coverability will thus be settled by the following lemma. If a free-choice net $N$ is covered by S-components and there are no proper semi-S-components in $N$, then $N$ is well-formed. We postpone the proof of the lemma, first noting the main consequence that implies the well-known coverability theorems and duality theorem (cf. de95). For a free-choice net $N$, the following conditions are equivalent: $N$ is well-formed,$N$ is covered by T-components and there are no proper semi-T-components in $N$,$N$ is covered by S-components and there are no proper semi-S-components in $N$,the reverse-dual net $\mathit{rd}(N)$ is well-formed. Proof: Let $N$ be a free-choice net. Recall that $\mathit{rd}(N)$ is a free-choice net as well, by Proposition \ref{['prop:rdProp']}. a)$\Rightarrow$b): If a) holds, that is, $N$ is well-formed, then b) holds by Lemma \ref{['lem:Tcover']}. b)$\Rightarrow$d): If b) holds, then $\mathit{rd}(N)$ is covered by S-components and there are no proper semi-S-components in $\mathit{rd}(N)$, by the assumption b) and Proposition \ref{['prop:ScorrespT']}. Hence, $\mathit{rd}(N)$ is well-formed by Lemma \ref{['lem:feasiblewf']}; that is, d) holds. d)$\Rightarrow$c): If $\mathit{rd}(N)$ is well-formed, then $\mathit{rd}(N)$ is covered by T-components and there are no proper semi-T-components in $\mathit{rd}(N)$, by Lemma \ref{['lem:Tcover']}. Hence, $\mathit{rd}(\mathit{rd}(N))$ is covered by S-components and there are no proper semi-S-components in $\mathit{rd}(\mathit{rd}(N))$, by Proposition \ref{['prop:ScorrespT']}. Since $\mathit{rd}(\mathit{rd}(N))=N$, c) is established. c)$\Rightarrow$a): This follows by Lemma \ref{['lem:feasiblewf']}. $\sqcap$$\sqcup$ =0 The proof of Theorem \ref{['thm:wfChar']} will thus be finished by proving Lemma \ref{['lem:feasiblewf']}. We consider a free-choice net $N_0$ such that $N_0$ is covered by S-components and there are no proper semi-S-components in $N_0$. We aim to demonstrate that $N_0$ is well-formed. We start by noting the token-conservation property of S-components, for any net $N$. If $X$ is an S-component of a net $N$, the sum of tokens in the places of $X$ remains constant during any execution of $N$. Consequently, if a net $N$ is covered by S-components, then $N$ is structurally bounded (that is, $(N, M_0)$ is bounded for every initial marking $M_0$). Proof: The first part is clear by recalling that for any S-component $X$ of $N$ we have: $|{}^\bullet{t}\cap S_X|=|{t}^\bullet\cap S_X|=1$ for each $t\in T_X$, and $|{}^\bullet{t}\cap S_X|=|{t}^\bullet\cap S_X|=0$ for each $t\in T_N\setminus T_X$ (since ${}^\bullet{S_X}=T_X={S_X}^\bullet$). The consequence follows by observing that for a fixed set $\text{SC}$ of S-components that cover the net $N$, and for all $M\in[M_0\rangle$ we have $\sum_{s\in S_N} M(s)\leq \sum_{X\in\text{SC}_N}\sum_{s\in S_X}M(s)=\sum_{X\in\text{SC}_N}\sum_{s\in S_X}M_0(s).$ $\sqcap$$\sqcup$ =0 Hence, the considered free-choice net $N_0$ is structurally bounded. The following proposition is a crucial step for establishing structural liveness (the existence of at least one live marking) of $N_0$. Recall that a marking $M$ of a net $N$ is a DL-marking if each transition of $N$ is either dead or live at $M$ and at least one transition is dead. Let $M$ be a DL-marking of a free-choice net $N$. Then there exists a semi-S-component $X$ of $N$, such that $M|_{S_X}=\mathbf{0}$. Proof: Given a DL-marking $M$ of a free-choice net $N$, we present $T_N$ as the disjoint union $T{}_{\text{dead}} \sqcup T{}_{\text{live}}$ of the sets of transitions that are dead and live at $M$, respectively, where $T{}_{\text{dead}} \neq \emptyset$. For each cluster $C\in\mathbb{C}_N$ with $T_C\neq\emptyset$, we thus have either $T_C\subseteq T{}_{\text{dead}}$ or $T_C\subseteq T{}_{\text{live}}$. Let $\mathbb{C}{}_{\text{dead}} = \{C \in \mathbb{C}_N \mid T_C\subseteq T{}_{\text{dead}} \text{ and } T_C\neq\emptyset\}$ be the set of dead clusters at $M$. (We ignore the possible cluster collecting all places $s\in S_N$ with ${s}^\bullet=\emptyset$.) We define a partial place-allocation $\beta\colon\mathbb{C}{}_{\text{dead}}\to S_N$ such that, for each $C\in\mathbb{C}{}_{\text{dead}}$, the place $s = \beta(C) \in S_C$ satisfies $M(s)=0$ and ${}^\bullet{s}\subseteq T{}_{\text{dead}}$. This choice is indeed possible: if for each $s\in S_C$ we had either $M(s)\geq 1$ or ${}^\bullet{s}\cap T{}_{\text{live}}\neq\emptyset$, then $C$ would not be dead at $M$, since it could eventually become enabled by firing transitions from $T{}_{\text{live}}$. Let $D$ be the subnet of $N$ induced by the set of places $S_D=\{s\mid s=\beta(C)\text{ for some } C\in\mathbb{C}{}_{\text{dead}}\}$ and the set of transitions $T_D=T{}_{\text{dead}}$. (See the illustration in Figure \ref{['fig:dl_marking_dual']}.) Let $X$ be a top SCC of the subnet $D$ (which might be a single place, but not a single transition). Hence $X$ is strongly connected, $S_X\neq\emptyset$, and $|{}^\bullet{t}\cap S_X|=1$ for each $t\in T_X$ (since each cluster of $D$, and thus also of its strongly connected subnet $X$, contains precisely one place). Moreover, ${}^\bullet{S_X}\subseteq T_X$ (where the notation "${}^\bullet{}$" refers to the net $N$), since ${}^\bullet{S_X}\subseteq T_D=T{}_{\text{dead}}$ and $X$ is a top SCC of $D$ (thus having no incoming arcs in $D$). The subnet $X$ is thus a semi-S-component of $N$ with $M(s)=0$ for all $s\in S_X$, the existence of which we aimed to establish. $\sqcap$$\sqcup$ =0 A free-choice net with a DL-marking $M$. Cluster C5 is live, the other clusters are dead. The blue subnet $D$ corresponds to a partial place-allocation selecting places in dead clusters that are unmarked and have no live input transitions. The top two SCCs of $D$ (in bold) are unmarked semi-S-components (that are in this case proper; one of Type I & II, the other of Type II only). Proposition \ref{['prop:MDLtopSCC']} thus confirms the motivating observation made in Remark \ref{['rem:bottomYtopX']}, since the semi-S-component $X$ in the proof is a top SCC of $N_{\beta}$ for some place-allocation $\beta$. Note that the partial place-allocation $\beta$ constructed in the proof can be extended to a (total) place-allocation if every cluster contains at least one place. We continue the plan to show that the net $N_0$ under consideration is well-formed; its structural boundedness has already been established. The following proposition establishes the structural liveness of $N_0$, relying on the fact that $M_0$ is live if and only if no DL-marking is reachable from $M_0$ (Proposition \ref{['prop:dlmarking']}). This proposition thus completes the proof of Lemma \ref{['lem:feasiblewf']}. The proposition is more general than what is strictly required to conclude the proof of Lemma \ref{['lem:feasiblewf']}. In particular, it highlights the significance of proper semi-S-components of Type II and will also be utilised in Section \ref{['sec:alg']}. Recall that a proper semi-S-component $X$ of Type II has at least one outbound arc $(s,t)$ with $s\in S_X$, $t\notin T_X$, and ${t}^\bullet\cap S_X=\emptyset$. If a free-choice net $N$ has no proper semi-S-component of Type II (that is, one with an outbound arc), then any marking $M_0$ of $N$ that places at least one token in each semi-S-component (for instance, the marking $M_0$ where $M_0(s)=1$ for all $s \in S_N$) is live. Proof: For any marking $M_0$ satisfying the assumption, no DL-marking $M$ is reachable. Indeed, the semi-S-component $X$ guaranteed for such an $M$ by Proposition \ref{['prop:MDLtopSCC']} would necessarily be either an S-component or a proper semi-S-component of Type I, but not of Type II; for such $X$, each transition $t\in {S_X}^\bullet$ satisfies $|{}^\bullet{t}\cap S_X|=1\leq|{t}^\bullet\cap S_X |$. However, this semi-S-component $X$ would have lost all its tokens during the hypothetical execution from $M_0$ to $M$, which is impossible. It follows that $M_0$ is live, by Proposition \ref{['prop:dlmarking']}. $\sqcap$$\sqcup$ =0 We propose Algorithm \ref{['alg:wf']}, with Algorithm \ref{['alg:semiT']} as its subprocedure. The restriction to strongly connected nets in the input of Algorithm \ref{['alg:wf']} is harmless, due to Theorem \ref{['th:wfImpSc']} and the availability of linear-time algorithms for computing the SCCs of a graph. Correctness relies primarily on Theorem \ref{['thm:wfChar']}. Specific arguments are presented via inline comments in the algorithms, referring to the points summarised in the following proposition. If a free-choice net $N$ is covered by T-components, then $N$ is well-formed if and only if there exists no proper semi-T-component of Type II in $N$.If $Y$ is a subnet of a net $N$ and $t \in T_N \setminus T_Y$, then $Y$ is a semi-T-component in $N$ if and only if it is a semi-T-component in the net $N_t$ obtained from $N$ by removing the transition $t$.If $Y$ is a subnet of a net $N$ and $(\{s\}\cup{}^\bullet{s})\cap (S_Y\cup T_Y)=\emptyset$, then $Y$ is a semi-T-component in $N$ if and only if it is a semi-T-component in the net $N_s$ obtained from $N$ by removing the nodes in $\{s\} \cup {}^\bullet{s}$.In a net $N$, there exists a proper semi-T-component of Type II if and only if there is some $s \in {}^\bullet{T_Y} \setminus {T_Y}^\bullet$, where $Y$ is a semi-T-component in the net $N_s$ obtained from $N$ by removing the nodes in $\{s\} \cup {}^\bullet{s}$. Proof: 1. Let $N$ be a free-choice net covered by $T$-components. Then the free-choice net $\mathit{rd}(N)$ is covered by S-components; thus, $\mathit{rd}(N)$ is structurally bounded (by Proposition \ref{['prop:SConserv']}). Hence, $\mathit{rd}(N)$ is well-formed if and only if there is no proper semi-S-component of Type II in $\mathit{rd}(N)$; specifically, the $\Leftarrow$ direction follows from Proposition \ref{['prop:noProperSwf']}, while the $\Rightarrow$ direction is due to Theorem \ref{['thm:wfChar']}(a)$\Rightarrow$(c). Consequently, $N$ is well-formed if and only if there is no proper semi-T-component of Type II in $N$ (recall that $N$ is well-formed if and only if $\mathit{rd}(N)$ is well-formed, by Theorem \ref{['thm:wfChar']}(a)$\Leftrightarrow$(d)). 2. and 3. The claims follow readily from an inspection of the conditions imposed on semi-T-components in Definition \ref{['def:semiTcomp']}. (The subnet $Y$ is strongly connected, $T_Y\neq\emptyset$, $|{s}^\bullet \cap T_Y|=1$ for each $s\in S_Y$, ${T_Y}^\bullet=S_Y$.) 4. Recall that a semi-T-component $Y$ in a net $N$ is a proper semi-T-component of Type II if and only if there exists $s \in {}^\bullet{T_Y} \setminus {T_Y}^\bullet$; by definition of semi-T-components (implying ${T_Y}^\bullet=S_Y$), we have $(\{s\}\cup{}^\bullet{s})\cap (S_Y\cup T_Y)=\emptyset$. The claim thus follows from item 3. $\sqcap$$\sqcup$ =0 Deciding if a free-choice net is well-formed InputInput OutputOutput A strongly connected free-choice net $N$. Yes, with a set $\mathit{TCover}$ of T-components that cover $N$, if $N$ is well-formed (wf); No, with a proper semi-T-component (psTc) $Y$ of $N$, if $N$ is not well-formed. $\mathit{TCover} \leftarrow \emptyset$ $\mathit{covered} \leftarrow \emptyset$ *[r]Set of transitions covered by $\mathit{TCover}$ $\mathit{covered} \neq T_N$ Select $t \in T_N \setminus \mathit{covered}$ Create an allocation $\alpha$ directed to $t$ Let $Y$ be the bottom SCC of $N_\alpha$ Hence $t$ belongs to $T_Y$, and $Y$ is an sTc in $N$ (cf. Prop. \ref{['prop:botSemiT']}). $Y$ is a proper semi-T-component (a psTc) No, $Y$ $\mathit{TCover} \leftarrow \mathit{TCover} \cup \{Y\}$ $\mathit{covered} \leftarrow \mathit{covered} \cup T_Y$ Construction of $\mathit{TCover}$ is complete, $N$ is covered by T-components. Hence $N$ is wf iff there is no psTc of Type II in $N$ (Prop. \ref{['prop:algcorrect']}(1)). Search for a psTc of Type II in $N$ follows. For each $s\in S_N$ check if $s\in {}^\bullet{T_Y}\setminus{T_Y}^\bullet$ for some sTc $Y$, that is, if some $t\in T_{C(s)}$ belongs to some sTc $Y$ in the net $N_s$ of Prop. \ref{['prop:algcorrect']}(4). This is impossible if $s$ is a unique place in its cluster $C(s)$, since $N$ is strongly connected. place $s \in S_{N}$ such that $|S_{C(s)}| > 1$ $T'\leftarrow T_{C(s)}\setminus{}^\bullet{s}$ $T'\neq\emptyset$ Construct the subnet $N_s$ resulting from $N$ by removing the set of nodes $\{s\} \cup {}^\bullet{s}$ $N_s$ (is a free-choice net that) might not be strongly connected. Call Algorithm \ref{['alg:semiT']} for $N_s$ and $T'$ It returns an sTc $Y$ in $N_s$ intersecting $T'$, if any exists. Algorithm \ref{['alg:semiT']} returns $Y$ (hence $T_Y\cap T'\neq\emptyset$) No, $Y$ *[r] $s\in {}^\bullet{T_Y}\setminus{T_Y}^\bullet$ in $N$ (since $T'\subseteq T_{C(s)}={s}^\bullet$ and ${}^\bullet{s}\cap T_Y=\emptyset$); hence $Y$ is a psTc of Type II in $N$. No psTc of Type II exists in $N$; $N$ is well-formed. Yes, $\mathit{TCover}$ Deciding if a transition set in an fc net intersects some semi-T-component InputInput OutputOutput Repeatrepeat A (general) free-choice net $N$ and a set $T_0\subseteq T_N$. A semi-T-component $Y$ such that $T_Y\cap T_0\neq\emptyset$, if such $Y$ exists; No otherwise. A semi-T-component (sTc) $Y$ is "admissible" if $T_Y\cap T_0\neq\emptyset$. $\mathit{Net} \leftarrow N$ *[r]$\mathit{Net}$ is a variable for successively reduced subnets of $N$ Mark each $t\in T_{\mathit{Net}}$ as good iff for each node $u\in\{t\}\cup{t}^\bullet$ there is a path from $u$ to $T_0$ By a path from $u$ to $T_0$ we mean a path from $u$ to some $t \in T_0$. Note that for every admissible $Y$, every $t\in T_Y$ is good; indeed: any sTc $Y$ is strongly connected, and satisfies ${T_Y}^\bullet=S_Y$. $T_0$ does not contain any good transition No*[r]Clearly, no admissible sTc exists. all $t\in T_{\mathit{Net}}$ are good Note that each place $s\in S_{\mathit{Net}}$ with ${s}^\bullet=\emptyset$ also satisfies ${}^\bullet{s}=\emptyset$. $\mathit{Net} \leftarrow$ the subnet of $\mathit{Net}$ obtained by removing all isolated places, if there are any Now each cluster of $\mathit{Net}$ has at least one transition. Create an allocation $\alpha$ for $\mathit{Net}$ directed to $T_0$ That is, for every node $u$ of $\mathit{Net}_\alpha$ there is a path from $u$ to $T_0$. a bottom SCC $Y$ of $\mathit{Net}_\alpha$ $Y$ is an sTc by Prop. \ref{['prop:botSemiT']}, and $T_Y\cap T_0\neq\emptyset$ due to the choice of $\alpha$ Some $t\in T_0$ is good and there exist non-good transitions in $\mathit{Net}$: $\mathit{Net} \leftarrow$ the subnet of $\mathit{Net}$ obtained by removing all non-good transitions $T_0 \leftarrow$ the subset of $T_0$ obtained by removing all non-good transitions $\mathit{Net}$ remains a free-choice net, cf. Prop. \ref{['prop:subFree']}(2). The set of admissible sTcs remains unchanged, cf. Prop. \ref{['prop:algcorrect']}(2). That Algorithms \ref{['alg:wf']} and \ref{['alg:semiT']} run in polynomial time is straightforward from their structure, combined with the use of standard graph algorithms such as Depth-First Search (DFS). Note that we have strived for clarity of presentation rather than for optimization. Further remarks are provided in Section \ref{['sec:remarks']}. Due to duality, the algorithms can be adapted to use semi-S-components instead of semi-T-components; this corresponds to operating on the reverse-dual net $\mathit{rd}(N)$ instead of $N$. Semi-T-components and semi-S-components are the two central concepts supporting the theory developed in Section \ref{['sec:main']}. Given a free-choice net $N$, the sets $S_X$ of semi-S-components $X$ (satisfying ${}^\bullet{S_X} \subseteq {S_X}^\bullet$) correspond to minimal siphons. These have traditionally played a crucial role in classical proofs, such as the proof of Commoner's Theorem (see Appendix \ref{['commoner.app']}) and the proof of S-coverability for well-formed free-choice nets (see, e.g., Chapters 4 and 5 in de95, where minimal siphons are essential, or Theorem 5.34 in DBLP:books/sp/BestD24, where Commoner's Theorem is employed extensively). Dually, semi-T-components $Y$ correspond to what might be termed minimal T-traps, that is, transition subsets $T_Y \subseteq T$ satisfying ${T_Y}^\bullet \subseteq {}^\bullet{T_Y}$. While we utilize these structures to derive the T-coverability of well-formed free-choice nets, neither T-traps nor semi-T-components appear to have played such a prominent role in the history of T-coverability results as they do in the present paper. The archetypal proof in de95 employs T-invariants and an exchange lemma, whereas the original proof by Hack hack72 resorts to a reduction technique that is semi-formally justified. A polynomial-time algorithm for deciding the well-formedness of strongly connected free-choice nets, which is quite different from Algorithm \ref{['alg:wf']}, was proposed in Chapter 6 of de95. This algorithm is based on the Rank Theorem for free-choice nets DBLP:conf/apn/EsparzaS89aDBLP:conf/apn/Desel92, which can be reduced to solving systems of linear equations. Another algorithm for deciding the well-formedness of free-choice nets, relying on a modified version of the Rank Theorem, was described by Kemper and Bause in DBLP:conf/apn/KemperB92 and later improved in DBLP:conf/apn/Kemper93 and kemper_cover. This algorithm achieves an overall time complexity of $O(|S||T|^2)$ for deciding the well-formedness of (strongly connected) free-choice nets. To the best of our knowledge, this is currently the most efficient algorithm known. Barkaoui and Minoux proposed a polynomial-time algorithm for deciding the liveness of bounded free-choice nets DBLP:conf/apn/BarkaouiM92. This was later improved and extended by Barkaoui, Couvreur and Dutheille in DBLP:conf/apn/BarkaouiCD95; with respective complexity $O(|S||T||F|)$, that is $O(|S|^2|T|^2)$. As already mentioned, our Algorithm \ref{['alg:wf']} adopts a dual approach to theirs, being based on semi-T-components. We plan to further explore whether this approach can be optimized to match the bounds achieved by algorithms based on the Rank Theorem. Given a net $N$, a set $Q\subseteq S_N$ is a trap if ${Q}^\bullet\subseteq{}^\bullet{Q}$, and it is a siphon if ${}^\bullet{Q}\subseteq{Q}^\bullet$. We will use the fact that the union of traps is itself a trap; thus, every set $R\subseteq S_N$ contains a unique maximal trap $Q\subseteq R$, namely the union of all traps contained in $R$. Additionally, we recall that if $Q$ is a trap such that $M_0|_{Q} \neq \mathbf{0}$, then $M|_{Q} \neq \mathbf{0}$ for all markings $M \in [M_0\rangle$. On the other hand, if $R$ is a siphon and $M|_{R}=\mathbf{0}$, then all transitions from ${R}^\bullet$ are dead at $M$ (since ${}^\bullet{R}\subseteq{R}^\bullet$). We present Algorithm \ref{['alg:maxTrap']}, a standard procedure for computing the maximal trap $Q$ inside a set of places $R$ (which may, in particular, be a siphon). The algorithm also provides layers of "leaking transitions" for $R$. We observe some simple facts regarding these transitions (Proposition \ref{['prop:maxTrapFacts']}), which allow us to provide a smooth proof of Commoner's Theorem. Construction of the maximal trap $Q$ inside a set of places $R$ InputInput OutputOutput Repeatrepeat A net $N$ and a set of places $R \subseteq S_N$. The maximal trap $Q\subseteq R$. $Q \leftarrow R$*[r]$Q$ is a variable whose value will be returned at the end $T_{exit} \leftarrow {Q}^\bullet\setminus {}^\bullet{Q}$*[r]each $t\in T_{exit}$ causes that $Q$ is not a trap $T_{exit} = \emptyset$ $Q$ *[r]the returned $Q$ is a trap no place $s\in{}^\bullet{T_{exit}}$ can be in the maximal trap inside $Q$ $Q \leftarrow Q \setminus {}^\bullet{T_{exit}}$ For any net $N$ and any set $R\subseteq S_N$, Algorithm \ref{['alg:maxTrap']} returns the maximal trap $Q\subseteq R$. Moreover, it also yields nonempty subsets $T_1,T_2,\ldots,T_m$ of the set ${R}^\bullet$ as successive values of the variable $T_{exit}$, where $m\leq |R\setminus Q|$ and each subset is produced during a single iteration of the cycle. We view $T{}_{\text{leak}}=\bigcup_{i\in[1,m]} T_i$ as the set of leaking transitions. Since the sets $T_i$, for $i \in [1, m]$, are pairwise disjoint (by item \ref{['item:disjoint']} of Proposition \ref{['prop:maxTrapFacts']}), each leaking transition $t \in T{}_{\text{leak}}$ has a well-defined exit index $\mathit{ei}(t) \in [1, m]$, defined as $\mathit{ei}(t) = i$ if $t \in T_i$. (See Figure \ref{['fig:commoner']} for an illustration with $m=3$. For a free-choice net, the condition ${}^\bullet{T_i} \cap {}^\bullet{T_j} = \emptyset$ holds for $i \neq j$, but this is not true in general.) Given a net $N$ and a set $R\subseteq S_N$, where $Q$ is the maximal trap inside $R$, the transitions from the set $T{}_{\text{leak}}=\bigcup_{i\in[1,m]} T_i$ satisfy: If $\mathit{ei}(t)=i{+}1$ (that is, $t\in T_{i+1}$), then there exists some place $s_t$ satisfying $s_t\in {}^\bullet{t}\cap (R\setminus \bigcup_{j\in[1,i]}{}^\bullet{T_j})$; the construction of $T_{i+1}$ also ensures $s_t\not\in\bigcup_{j\in[1,i+1]}{T_j}^\bullet$.$R\cap {}^\bullet{T{}_{\text{leak}}}=R\setminus Q$ (that is, $R\setminus {}^\bullet{T{}_{\text{leak}}}=Q$).For each $t\in T{}_{\text{leak}}$ we have ${}^\bullet{t}\cap Q={t}^\bullet\cap Q=\emptyset$. For any free-choice net $N$ with no isolated places and any marking $M_0$ of $N$, the following two conditions are equivalent: $(N,M_0)$ is live.Every nonempty siphon $R\subseteq S_N$ contains a trap $Q\subseteq R$ such that $M_0|_{Q}\neq \mathbf{0}$. Proof: We fix a free-choice net $N$ and establish the two implications. 1. b) $\Rightarrow$ a): (This implication holds even if isolated places are present.) We assume that $(N, M_0)$ is nonlive and show that there exists a nonempty siphon $R$ such that every trap $Q \subseteq R$ satisfies $M_0|_{Q} = \mathbf{0}$. Since $M_0$ is nonlive, there exists a DL-marking $M \in [M_0\rangle$ (by Proposition \ref{['prop:dlmarking']}). We fix such an $M$ and choose a semi-S-component $X$ of $N$ such that $M|_{S_X} = \mathbf{0}$ (which exists by Proposition \ref{['prop:MDLtopSCC']}). Observe that $S_X$ is a nonempty siphon, since $S_X \neq \emptyset$ and ${}^\bullet{S_X} = T_X \subseteq {S_X}^\bullet$ by Definition \ref{['def:Snotions']}. Furthermore, every trap $Q\subseteq S_X$ satisfies $M|_{Q}=\mathbf{0}$, which implies $M_0|_{Q}=\mathbf{0}$ since $M\in[M_0\rangle$ (recall that $M_0|_{Q}\neq\mathbf{0}$ implies $M'|_{Q}\neq\mathbf{0}$ for every $M'\in[M_0\rangle$). 2. a) $\Rightarrow$ b): Now we assume that the fixed free-choice net $N$ has no isolated places and consider a marking $M_0$ and a nonempty siphon $R$ satisfying $M_0|_{Q}=\mathbf{0}$ for the maximal trap $Q\subseteq R$. We will show that $M_0$ is nonlive. Since $N$ has no isolated places, we have ${}^\bullet{R} \subseteq {R}^\bullet \neq \emptyset$. We complete the proof by constructing a marking $M \in [M_0\rangle$ at which all transitions in ${R}^\bullet$ are dead. If the maximal trap $Q\subseteq R$ satisfies $Q = R$, then all transitions in ${R}^\bullet$ are already dead at $M_0$ (since $M_0|_{R} = \mathbf{0}$ and ${}^\bullet{R} \subseteq {R}^\bullet$). We thus further assume that $R \setminus Q$ is nonempty, and consider the nonempty set $T{}_{\text{leak}}=\bigcup_{i\in[1,m]}T_i$ of the respective leaking transitions. Now we stepwise construct an execution Exec from $M_0$ by firing the leaking transitions in $T{}_{\text{leak}}$ as frequently as possible, while preserving the invariant that $Q$ remains unmarked. Having constructed a prefix $M_0 \xrightarrow{\sigma} M$ of Exec (starting with $M_0 \xrightarrow{\varepsilon} M_0$, where $M_0 |_{Q} = \mathbf{0}$), we prolong it whenever there exists a transition in ${R}^\bullet$ that is not dead at $M$. In this case, we select a shortest sequence $M \xrightarrow{\sigma'} M'$ such that $M'$ enables some $t_0 \in {R}^\bullet$. We then extend the prefix to $M_0 \xrightarrow{\sigma}M\xrightarrow{\sigma'} M'$. Note that $M' |_{Q} = \mathbf{0}$ because $M |_{Q} = \mathbf{0}$ by the invariant, and no transition from ${R}^\bullet\supseteq{}^\bullet{R}\supseteq{}^\bullet{Q}$ occurs in $\sigma'$. Hence, ${}^\bullet{t_0}\cap R\subseteq R\setminus Q\subseteq {}^\bullet{T{}_{\text{leak}}}$ (recall Proposition \ref{['prop:maxTrapFacts']}). Consequently, there exists some place $s\in{}^\bullet{t_0}\cap{}^\bullet{T{}_{\text{leak}}}$; thus, ${}^\bullet{t_0} = {}^\bullet{t}$ for some $t\in T{}_{\text{leak}}$, due to the free-choice property (as illustrated in Figure \ref{['fig:commoner']} for $s=s_{21}$ and $t = t_{21}$). Hence, $M'$ enables $t$ as well, and we prolong the prefix of Exec to $M_0\xrightarrow{\sigma\sigma'}M'\xrightarrow{t}M"$. Since $M'|_{Q}=\mathbf{0}$ and ${t}^\bullet\cap Q=\emptyset$ (by item 3 of Proposition \ref{['prop:maxTrapFacts']}), we preserve the invariant: $M"|_{Q}=\mathbf{0}$. We finish the proof by showing that Exec is finite, ending in a marking $M$ where all transitions in ${R}^\bullet$ are dead. Otherwise, Exec would be an infinite execution that fires transitions from $T{}_{\text{leak}}$ infinitely often, while firing no other transitions from ${R}^\bullet$. Consider a transition $t\in T{}_{\text{leak}}$ with the maximal exit index $\mathit{ei}(t)$ among those fired infinitely often, and recall the place $s_t$ from Proposition \ref{['prop:maxTrapFacts']}. The marking of $s_t$ is decreased infinitely often (whenever $t$ fires) but increased only finitely many times (by leaking transitions with strictly higher exit indices than $\mathit{ei}(t)$)---a contradiction. $\sqcap$$\sqcup$ =0 Layers of leaking transitions $T_1=\{t_{11},t_{12}\}$, $T_2$, $T_3$ for a free-choice net; $t_0\in{R}^\bullet\setminus T{}_{\text{leak}}$. Best E, Devillers R. Petri Net Primer - A Compendium on the Core Model, Analysis, and Synthesis. Springer, 2024. ISBN 978-3-031-48277-9. doi: 10.1007/978-3-031-48278-6. URL https://doi.org/10.1007/978-3-031-48278-6.Commoner FG. Deadlocks in Petri Nets. Technical Report CA-7206-2311, Applied Data Research, Wakefield, Mass., 1972.Hack MH. Analysis of Production Schemata by Petri Nets. Technical report, Massachussetts Institute of Technology, MAC TR-94, 1974 (based on his MSc thesis, 1972).Esparza J, Silva Suárez M. On the analysis and synthesis of free choice systems. In: Rozenberg G (ed.), Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, Bonn, Germany, June 1989, Proceedings], volume 483 of Lecture Notes in Computer Science. Springer, 1989 pp. 243--286. doi: 10.1007/3-540-53863-1_28. URL https://doi.org/10.1007/3-540-53863-1_28.Esparza J, Silva Suárez M. Circuits, handles, bridges and nets. In: Rozenberg G (ed.), Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, Bonn, Germany, June 1989, Proceedings], volume 483 of Lecture Notes in Computer Science. Springer, 1989 pp. 210--242. doi: 10.1007/3-540-53863-1_27. URL https://doi.org/10.1007/3-540-53863-1_27.Esparza J. Synthesis Rules for Petri Nets, and How they Lead to New Results. In: Baeten JCM, Klop JW (eds.), CONCUR '90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, volume 458 of Lecture Notes in Computer Science. Springer, 1990 pp. 182--198. doi: 10.1007/BFB0039060. URL https://doi.org/10.1007/BFb0039060.Esparza J, Silva Suárez M. Top-down synthesis of live and bounded free choice nets. In: Rozenberg G (ed.), Advances in Petri Nets 1991, Papers from the 11th International Conference on Applications and Theory of Petri Nets, Paris, France, June 1990, volume 524 of Lecture Notes in Computer Science. Springer, 1990 pp. 118--139. doi: 10.1007/BFB0019972. URL https://doi.org/10.1007/BFb0019972.Desel J, Esparza J. Free Choice Petri Nets, volume 40 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1995.Gaujal B, Haar S, Mairesse J. Blocking a transition in a free choice net and what it tells about its throughput. J. Comput. Syst. Sci., 2003. 66(3):515--548. doi: 10.1016/S0022-0000(03)00039-4. URL https://doi.org/10.1016/S0022-0000(03)00039-4.Wehler J. Free-Choice Petri Nets without Frozen Tokens, and Bipolar Synchronization Systems. Fundam. Informaticae, 2010. 98(2-3):283--320. doi: 10.3233/FI-2010-228. URL https://doi.org/10.3233/FI-2010-228.van der Aalst WMP. Free-choice Nets with Home Clusters are Lucent. Fundam. Informaticae, 2021. 181(4):273--302. doi: 10.3233/FI-2021-2059. URL https://doi.org/10.3233/FI-2021-2059.Kemper P, Bause F. An Efficient Polynomial-Time Algorithm to Decide Liveness and Boundedness of Free-Choice Nets. In: Jensen K (ed.), Application and Theory of Petri Nets 1992, 13th International Conference, Sheffield, UK, June 22-26, 1992, Proceedings, volume 616 of Lecture Notes in Computer Science. Springer, 1992 pp. 263--278. doi: 10.1007/3-540-55676-1_15. URL https://doi.org/10.1007/3-540-55676-1_15.Kemper P. O(|P||T|)-Algorithm to Compute a Cover of S-components in EFC-nets. Technical Report Forschungsbericht Nr. 543, Department of Computer Science, University of Dortmund, 1994.Barkaoui K, Minoux M. A Polynomial-Time Graph Algorithm to Decide Liveness of Some Basic Classes of Bounded Petri Nets. In: Jensen K (ed.), Application and Theory of Petri Nets 1992, 13th International Conference, Sheffield, UK, June 22-26, 1992, Proceedings, volume 616 of Lecture Notes in Computer Science. Springer, 1992 pp. 62--75. doi: 10.1007/3-540-55676-1_4. URL https://doi.org/10.1007/3-540-55676-1_4.Barkaoui K, Couvreur J, Dutheillet C. On Liveness in Extended non Self-Controlling Nets. In: Michelis GD, Diaz M (eds.), Application and Theory of Petri Nets 1995, 16th International Conference, Turin, Italy, June 26-30, 1995, Proceedings, volume 935 of Lecture Notes in Computer Science. Springer, 1995 pp. 25--44. doi: 10.1007/3-540-60029-9_32. URL https://doi.org/10.1007/3-540-60029-9_32.Jančar P. A concise proof of Commoner's theorem. CoRR, 2024. abs/2401.12067. doi: 10.48550/ARXIV.2401.12067. 2401.12067, URL https://doi.org/10.48550/arXiv.2401.12067.Best E, Devillers R, Jančar P. Coverability in Well-Formed Free-Choice Nets. In: Amparore EG, Mikulski L (eds.), Application and Theory of Petri Nets and Concurrency - 46th International Conference, PETRI NETS 2025, Paris, France, June 22-27, 2025, Proceedings, volume 15714 of Lecture Notes in Computer Science. Springer, 2025 pp. 86--108. doi: 10.1007/978-3-031-94634-9_5. URL https://doi.org/10.1007/978-3-031-94634-9_5.Tarjan RE. Depth-First Search and Linear Graph Algorithms. SIAM J. Comput., 1972. 1(2):146--160. doi: 10.1137/0201010. URL https://doi.org/10.1137/0201010.Desel J. A Proof of the Rank Theorem for Extended Free Choice Nets. In: Jensen K (ed.), Application and Theory of Petri Nets 1992, 13th International Conference, Sheffield, UK, June 22-26, 1992, Proceedings, volume 616 of Lecture Notes in Computer Science. Springer, 1992 pp. 134--153. doi: 10.1007/3-540-55676-1_8. URL https://doi.org/10.1007/3-540-55676-1_8.Kemper P. Linear Time Algorithm to Find a Minimal Deadlock in a Strongly Connected Free-Choice Net. In: Marsan MA (ed.), Application and Theory of Petri Nets 1993, 14th International Conference, Chicago, Illinois, USA, June 21-25, 1993, Proceedings, volume 691 of Lecture Notes in Computer Science. Springer, 1993 pp. 319--338. doi: 10.1007/3-540-56863-8_54. URL https://doi.org/10.1007/3-540-56863-8_54.