Thomas Hujsa
email: hujsa.thomas@gmail.com

Raymond Devillers

On Deadlockability, Liveness and Reversibility in Subclasses of Weighted Petri Nets

Keywords: Structural analysis, Weighted Petri net, Deadlockability, Liveness, Reversibility, Boundedness, Monotonicity, Fork-attribution, Join-free, Communication-free, Synchronizationfree, Asymmetric-choice

Liveness, (non-)deadlockability and reversibility are behavioral properties of Petri nets that are fundamental for many real-world systems. Such properties are often required to be monotonic, meaning preserved upon any increase of the marking. However, their checking is intractable in general and their monotonicity is not always satisfied. To simplify the analysis of these features, structural approaches have been fruitfully exploited in particular subclasses of Petri nets, deriving the behavior from the underlying graph and the initial marking only, often in polynomial time.

In this paper, we further develop these efficient structural methods to analyze deadlockability, liveness, reversibility and their monotonicity in weighted Petri nets. We focus on the join-free subclass, which forbids synchronizations, and on the homogeneous asymmetric-choice subclass, which allows conflicts and synchronizations in a restricted fashion.

For the join-free nets, we provide several structural conditions for checking liveness, (non-)deadlockability, reversibility and their monotonicity. Some of these methods operate in polynomial time. Furthermore, in this class, we show that liveness, non-deadlockability and reversibility, taken together or separately, are not always monotonic, even under the assumptions of structural boundedness and structural liveness. These facts delineate more sharply the frontier between monotonicity and nonmonotonicity of the behavior in weighted Petri nets, present already in the join-free subclass.

In addition, we use part of this new material to correct a flaw in the proof of a previous characterization of monotonic liveness and boundedness for homogeneous asymmetric-choice nets, published in 2004 and left unnoticed.

Introduction

In Petri nets, liveness preserves the possibility to fire any transition after a finite number of other firings, non-deadlockability-a weak form of liveness, also known as deadlock-freeness-states the absence of reachable deadlocks (i.e. markings that enable no transition), and reversibility ensures that the initial marking can be reached from any reachable marking, inducing the strong connectedness of the reachability graph. They are often studied together with boundedness, which designates the finiteness of the reachability graph.

These properties are required for many real-life applications, such as embedded and flexible manufacturing systems: liveness models the preservation of all functionalities over time; non-deadlockability ensures that some functionalities remain active; reversibility favors a regular, steady behavior from the start and enables the system to reset itself, i.e. solely through internal operations; and boundedness sets a limited amount of resources.

Weighted Petri nets and applications. In this paper, we investigate weighted Petri nets, which are well suited to the modeling of numerous real-life systems. In the domain of embedded systems, Synchronous Data Flow graphs [START_REF] Lee | Synchronous Data Flow[END_REF] have been introduced to model the communications between a finite set of periodic processes. These graphs can be modeled by weighted T-nets (also known as weighted marked graphs), a Petri net subclass in which each place has at most one input and one output. In the domain of flexible manufacturing systems (FMS), the weights make possible the modeling of bulk consumption or production of resources [START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF]. In these cases, weights allow a compact representation of the volumes of data or resources exchanged. An objective of the present paper is to extend the expressiveness of weighted T-nets so as to model more complex embedded applications while ensuring non-deadlockability (or even liveness), reversibility and boundedness efficiently.

Difficulty of analysis in the general case. In weighted Petri nets, liveness, boundedness and reversibility are decidable [START_REF] Esparza | Decidability issues for Petri nets-A survey[END_REF][START_REF] Araki | Decidable problems on the strong connectivity of Petri net reachability sets[END_REF][START_REF] De Frutos Escrig | Decidability of Home Space Property[END_REF][START_REF] Esparza | Decidability and complexity of Petri net problems-an introduction[END_REF]. However, checking liveness or boundedness is EXPSPACE-hard [START_REF] Esparza | Decidability issues for Petri nets-A survey[END_REF][START_REF] Cheng | Complexity results for 1-safe nets[END_REF][START_REF] Lipton | The reachability problem requires exponential space[END_REF], and checking reversibility is PSPACE-hard [START_REF] Esparza | Decidability and complexity of Petri net problems-an introduction[END_REF].

Subclasses and structural methods. A common approach to alleviate the difficulty of analysis is to consider specific subclasses of Petri nets and to relate the structure of a net to its behavior.

The subclass of homogeneous nets, in which each place has all its outputs weights equal, has been fruitfully studied in previous works under additional restrictions [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF][START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF]. In this paper, we focus on join-free (JF) nets, which do not have synchronizations, and homogeneous asymmetric-choice (HAC) nets, in which each pair p, p of input places of any synchronization satisfies the following: all the outputs of p are also outputs of p , or conversely. HAC nets generalize weighted T-nets as well as homogeneous JF (HJF) nets.

Structural properties do not always depend on a fixed initial marking. For example, structural liveness states the existence of a live marking and structural boundedness ensures boundedness for every initial marking. Polynomial-time characterizations of both properties are known for ordinary (unit-weighted) free-choice (OFC) nets (in which all conflicting transitions have equal enabling conditions), based on decompositions into specific subnets (e.g. siphons and traps) and inequalities on the rank of the inci-dence matrix of the net (Rank theorems) [START_REF] Barkaoui | A polynomial-time graph algorithm to decide liveness of some basic classes of bounded Petri nets[END_REF][START_REF] Desel | Free Choice Petri Nets[END_REF][START_REF] Silva | Linear algebraic and linear programming techniques for the analysis of place/transition net systems[END_REF]. From such structural conditions, polynomial-time methods checking the liveness of an initial marking have been deduced for bounded OFC nets [START_REF] Desel | Free Choice Petri Nets[END_REF].

Similar techniques, sometimes in a weaker form, have been developed for other classes with weights, including JF and HAC nets [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Recalde | Modeling and analysis of sequential processes that cooperate through buffers[END_REF][START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF][START_REF] Barkaoui | On the Equivalence Between Liveness and Deadlock-Freeness in Petri Nets[END_REF][START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF][START_REF] Silva | Linear algebraic and linear programming techniques for the analysis of place/transition net systems[END_REF][START_REF] Hujsa | Polynomial Sufficient Conditions of Well-Behavedness and Home Markings in Subclasses of Weighted Petri nets[END_REF]. Also, several polynomial-time sufficient conditions of liveness, boundedness and reversibility, taken together, have been proposed for several classes [START_REF] Hujsa | Polynomial Sufficient Conditions of Well-Behavedness and Home Markings in Subclasses of Weighted Petri nets[END_REF][START_REF] Hujsa | On the Reversibility of Well-Behaved Weighted Choice-Free Systems[END_REF][START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF], some of which generalize the HJF and OFC nets.

Monotonic behavior. Many applications must fulfill the monotonicity of their properties, meaning their preservation upon any increase of the initial marking. Embedded and manufacturing systems, among others, need their behavior to be maintained regardless of any addition of initial data items or resources. Liveness, (non-)deadlockability, reversibility and boundedness are not monotonic in general, even when taken together, e.g. in HAC nets [START_REF] Desel | Free Choice Petri Nets[END_REF][START_REF] Heiner | On the Importance of the Deadlock Trap Property for Monotonic Liveness[END_REF][START_REF] Silva | Linear algebraic and linear programming techniques for the analysis of place/transition net systems[END_REF]. However, monotonic liveness (m-liveness) and monotonic non-deadlockability are fulfilled by OFC nets and some larger classes that contain HJF nets [START_REF] Desel | Free Choice Petri Nets[END_REF][START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Recalde | Modeling and analysis of sequential processes that cooperate through buffers[END_REF][START_REF] Barkaoui | A polynomial-time graph algorithm to decide liveness of some basic classes of bounded Petri nets[END_REF][START_REF] Barkaoui | On liveness and controlled siphons in Petri nets[END_REF][START_REF] Barkaoui | On the Equivalence Between Liveness and Deadlock-Freeness in Petri Nets[END_REF]. M-liveness+reversibility, meaning m-liveness and m-reversibility considered together, is also fulfilled by homogeneous (weighted) free-choice (HFC, also called equal-conflict or EC) nets [START_REF] Desel | Free Choice Petri Nets[END_REF][START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF]. In the HFC class, under some restrictions, liveness and non-deadlockability are equivalent, allowing to deduce the same results for the assumption of non-deadlockability [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF]. Decompositions and behavior. Several complex Petri net subclasses are decomposable into specific JF subnets induced by subsets of places, allowing to characterize properties of a marked Petri net (also called a Petri net system) in terms of the same properties in JF subsystems. In various studies (e.g. in [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF]), the relevant subsets of places considered are siphons, i.e. subsets P of places satisfying the following property on their surrounding transitions: the input set of P is included in the output set of P . Also, the subnets induced by such subsets P of places are typically P-subnets, i.e. subnets whose set of places equals P and whose set of transitions T equals the set of inputs and outputs of P in the original net.

Siphons form an important structure: once emptied (or insufficiently marked), there is no possibility to fire a transition having an input place in them, since they cannot receive new tokens from other transitions. A common necessary condition of liveness requests that siphons never become insufficiently marked. In OFC nets and several larger classes, the existence of marked traps in every siphon is of major importance to satisfy this condition [START_REF] Desel | Free Choice Petri Nets[END_REF][START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF][START_REF] Barkaoui | On liveness and controlled siphons in Petri nets[END_REF].

In the HAC class and its subclass of HFC nets, m-liveness has been expressed in terms of the mliveness of JF P-subnets induced by siphons [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF]. Exploiting this fact in a bottom-up approach, polynomial-time sufficient conditions of m-liveness for bounded JF nets were shown to propagate to the decomposable, bounded HFC nets [START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF]. For the Choice-free (CF) nets (not to be confused with freechoice nets), which form a subclass of the HFC nets, similar techniques have been exploited to deduce polynomial-time sufficient conditions of m-liveness+reversibility, using particular reversible JF subnets [START_REF] Hujsa | On the Reversibility of Well-Behaved Weighted Choice-Free Systems[END_REF].

For the larger class of weighted free-choice nets, which contains HFC nets, there exist polynomialtime sufficient conditions of decomposability into well-formed-i.e. structurally live and structurally bounded-JF nets [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF].

Moreover, in any m-live system, every siphon-induced P-subsystem is necessarily m-live, and the same applies to m-reversibility [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF][START_REF] Barkaoui | On liveness and controlled siphons in Petri nets[END_REF].

Hence, JF subnets form basic modules of major importance for the study of liveness and reversibility in decomposable classes.

Contributions. First, for the structural liveness analysis of HJF nets, we highlight the notion of subconsistency, which states the existence of a positive vector whose left-multiplication by the incidence matrix yields a non-null vector with no positive component. We use this algebraic notion to develop the first polynomial-time characterizations of structural deadlockability (meaning deadlockability of every marking) and structural liveness for HJF nets, without the classical assumption of structural boundedness (or conservativeness) exploited in previous studies [START_REF] Desel | Free Choice Petri Nets[END_REF][START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Silva | Linear algebraic and linear programming techniques for the analysis of place/transition net systems[END_REF] 1 .

To achieve it, we first restrict our attention to siphons as follows. In any HJF net whose set of places is its unique siphon, we show that sub-consistency is equivalent to structural deadlockability, and that non-sub-consistency is equivalent to structural liveness. Since sub-consistency can be checked with a linear program, these conditions can be evaluated in polynomial-time. Also, we extend this result to the rest of the HJF class, using a decomposition into minimal siphons.

Second, we use this new material to correct an erroneous proof of a previous characterization of m-liveness+boundedness for HAC nets, based on a decomposition of HAC nets into HJF subnets, published in 2004 in [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF] and left unnoticed.

Third, leaving out homogeneity, we provide a live and structurally bounded JF system that is not m-live, and a live, reversible and structurally bounded JF system that is not m-reversible. We deduce from them the non-monotonicity of non-deadlockability in this class under similar assumptions. These examples contrast with the HFC case, thus also with the HJF case [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF][START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF]. Besides, they show that a previous characterization of m-reversibility for live HFC nets, developed in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF] and based on the existence of an initially feasible sequence that contains all transitions and leads to the initial markingalso known as a T-sequence-, is not sufficient to ensure m-reversibility in live, structurally bounded, inhomogeneous JF nets.

Finally, we propose a sufficient condition of reversibility for strongly connected and live JF nets, exploiting T-sequences and the assumption that each reachable marking enables all the outgoing transitions of some place. We derive from this condition the first polynomial-time sufficient condition of m-liveness+reversibility for structurally bounded and structurally live JF nets, based on initial markings with a number of tokens linear in the weights. We also dedicate variants of these results to weighted S-nets, which form a subclass of JF nets.

Comparing with [START_REF] Hujsa | On Liveness and Deadlockability in Subclasses of Weighted Petri Nets[END_REF], we add Figure 7 to the study of the HJF nets in Section 3, we refine in Lemma 4.1 of Section 4 a previous result of [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF] for HAC nets to get rid of the pureness 2 assumption, we further investigate the non-monotonicity of behavioral properties in JF nets in Section 5 and we add the study, in Sections 5 and 6, of the reversibility property and its monotonicity in live JF nets. These new developments improve our understanding of the relationship between liveness, non-deadlockability, reversibility and boundedness in JF nets.

Table 1 recalls previous results of the literature and presents the new results developed in this paper. 1 In this case, the well-known necessary conditions of liveness based on siphons containing traps or based on the existence of a repetitive vector [START_REF] Desel | Free Choice Petri Nets[END_REF][START_REF] Silva | Linear algebraic and linear programming techniques for the analysis of place/transition net systems[END_REF][START_REF] Barkaoui | On liveness and controlled siphons in Petri nets[END_REF] do not help. 2 A net is pure if it does not contain two nodes x and y with an arc from x to y and an arc from y to x.

HAC

Variants of the property Results on liveness and L, R, L+R and D are not monotonic [START_REF] Heiner | On the Importance of the Deadlock Trap Property for Monotonic Liveness[END_REF]. are investigated m-liveness related Non-poly-time characterization of in [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF].

to the structure [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF]. m-L+B whose proof is erroneous [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF].

New: Correction of the proof. Organization of the paper. We formalize in Section 2 the notions used in this paper. In Section 3, we present the polynomial-time conditions for the structural deadlockability and liveness of HJF nets. Thereafter, in Section 4, we correct the proof of the mentioned previous result on the m-liveness+boundedness of HAC nets. We provide in Section 5 the counter-examples showing the non-monotonicity of liveness, non-deadlockability and reversibility in well-formed (i.e. structurally bounded and structurally live) JF nets. In Section 6, we recall previous results relating T-sequences to liveness and reversibility. Then, using T-sequences, we develop the new sufficient conditions of liveness and reversibility for strongly connected JF nets. Finally, Section 7 presents our conclusion and perspectives.

Definitions, notations and properties

In this section, we present the notions and notations used throughout the paper.

Weighted and ordinary nets

A (weighted) net is a triple N = (P, T, W ) where the sets P and T are finite and disjoint, P is the set of places, T is the set of transitions, P ∪ T is the set of the nodes of the net and W : (P × T ) ∪ (T × P ) → N is a weight function. An arc leads from a place p to a transition t (respectively from a transition t to a place p) if W (p, t) > 0 (respectively W (t, p) > 0). An ordinary net is a net whose weight function W takes its values in {0, 1}.

The incidence matrix of a net (P, T, W ) is a place-transition matrix I such that ∀p ∈ P , ∀t ∈ T , I[p, t] = W (t, p) -W (p, t), where the weight of a non-existing arc is 0. The pre-set (or input set) of element x of P ∪ T , denoted by • x, is the set {w|W (w, x) > 0}. By extension, for any subset E of

P or T , • E = x∈E • x. The post-set (or output set) of element x of P ∪ T , denoted by x • , is the set {y|W (x, y) > 0}. Similarly, E • = x∈E x • .
A transition with two or more input places represents a synchronization on its input places. A choiceplace, or a choice, is a place having at least two output transitions.

Markings, systems, firing sequences and reachability

A marking M of a net N = (P, T, W ) is a mapping M : P → N. The pair (N, M ) defines a system whose initial marking is M . The system (N, M ) enables

a transition t ∈ T if ∀p ∈ • t, M (p) ≥ W (p, t).
The marking M obtained from M by firing the enabled transition t, denoted by

M t - → M or M [t M , is defined as follows: ∀p ∈ P , M (p) = M (p) -W (p, t) + W (t, p). The system (N, M ) enables a place p ∈ P if ∀t ∈ p • , M (p) ≥ W (p, t).
The system (N, M ) enables a set T of transitions (respectively a set P of places) if (N, M ) enables each transition of T (respectively each place of P ).

A firing sequence σ of length n ≥ 1 on the set of transitions T , denoted by σ = t 1 t 2 . . . t n with t 1 , t 2 , . . . , t n ∈ T , is a mapping {1, . . . , n} → T . The firing sequence σ is feasible in (N, M 0 ) if the successive markings obtained, M 0

t 1 -→ M 1 t 2 -→ M 2 . . . tn -→ M n , are such that M k-1 enables the transition t k for each k ∈ {1, . . . , n}, also denoted M 0 σ -→ M n or M 0 [σ M n .
The Parikh vector Ψ(σ) : T → N associated with a finite sequence of transitions σ maps every transition t of T to the number of occurrences of t in σ.

A marking M is said to be reachable from the marking M if there exists a firing sequence σ feasible in (N, M ) such that M σ -→ M . The set of markings reachable from M is denoted by [M . The reachability graph of a system S = (N, M 0 ), denoted by RG(S), is the rooted and labelled directed graph with the set of vertices [M 0 , the initial state M 0 , the set of labels T , and the set of arcs

{(M, t, M ) | M, M ∈ [M 0 ∧ M [t M }.

Petri net properties

Main properties and monotonicity. Let S = (N, M 0 ) be a system. • N is well-formed if it is structurally bounded and structurally live.

• A behavioral property P is monotonic for S, or S is monotonically P, or S is m-P, if (N, M 0 ) satisfies P for every M 0 ≥ M 0 . A marking M is m-P if (N, M ) is m-P, where N is deduced from the context. The net N is m-P if, for every marking M such that (N, M ) satisfies P, (N, M ) is m-P. A set N of nets if m-P if every net of N is m-P. We shall typically instantiate P with the liveness and reversibility properties.

Properties defined only on nets extend to systems through their underlying net.

Vectors. The support of a vector V with index set I(V ), noted S(V ), is the set {i ∈ I(V )|V (i) = 0} of indices of nonnull components. We denote by 0 n (respectively 1 n ) the column vector of size n whose components are all equal to 0 (respectively 1). We may use the simpler notation 0 and 1 when n is deduced from the context.

Conservativeness, consistency and variants. Let N = (P, T, W ) be a net with incidence matrix I.

• N is conservative if there exists a vector X ≥ 1 such that X T • I = 0. In the particular case of X = 1 such that X T • I = 0, N is said 1-conservative.

• N is consistent (respectively sur-consistent, sub-consistent) if there exists a vector

Y ≥ 1 such that I • Y = 0 (respectively I • Y 0, I • Y 0)
. N is weakly sur-consistent (respectively weakly sub-consistent) if there exists a vector Y ≥ 1 such that I • Y ≥ 0 (respectively I • Y ≤ 0), i.e. if it is consistent or sur-consistent (respectively consistent or sub-consistent). Weak sur-consistency is also known as structural repetitiveness.

• N is partially consistent (respectively partially sur-consistent, partially sub-consistent) if there exists a vector Y 0 such that

I • Y = 0 (respectively I • Y 0, I • Y 0).

Petri nets subclasses

A weighted net N = (P, T, W ) is:

• a P-net (or S-net) if ∀t ∈ T : | • t| ≤ 1 and |t • | ≤ 1.
• a T-net (or generalized event graph, or weighted marked graph) if ∀p ∈ P :

| • p| ≤ 1 and |p • | ≤ 1.
• join-free (JF) (or generalized communication-free, or synchronization-free) if ∀t ∈ T :

| • t| ≤ 1.
• choice-free (CF) (or output-nonbranching) if ∀p ∈ P :

|p • | ≤ 1.
• fork-attribution (FA) if it is both JF and CF.

• free-choice (FC) (or Topologically Extended Free Choice, TEFC)

if ∀p 1 , p 2 ∈ P , p • 1 ∩ p • 2 = ∅ ⇒ p • 1 = p • 2 .
This class generalizes, with arbitrary weights, the ordinary free-choice (OFC) nets and the (weighted) equal-conflict (EC) nets of the literature [START_REF] Desel | Free Choice Petri Nets[END_REF][START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF].

• asymmetric-choice (AC) if ∀p 1 , p 2 ∈ P , p 1 • ∩ p 2 • = ∅ ⇒ p 1 • ⊆ p 2 • or p 2 • ⊆ p 1 • .
The class of AC nets contains the FC nets, hence also the FA, CF, JF, P-and T-nets.

• homogeneous if, ∀p ∈ P , ∀t, t ∈ p • , W (p, t) = W (p, t ). The homogeneous subclass of a class is identified by an additional prefix letter H. For instance, HFC nets denote the homogeneous FC nets, also called equal-conflict in [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF].

In Figure 1, some illustrations for these classes are presented. Figure 2 represents the inclusion relations between some special subclasses of weighted Petri nets considered in this paper. 2. Some classes and subclasses of weighted systems ordered by inclusion of their structurally defined elements. A proper structural inclusion does not necessarily represent a proper expressiveness inclusion. Each class is represented by its name surrounded by an ellipse, except the Fork-Attribution (FA) class, which is represented by the intersection of the CF set with the JF set, and the HJF class, which is represented by the intersection of the HFC set with the JF set.

p

Subsequences and graph structures

Subsequences and projections. The sequence σ is a subsequence of the sequence σ if σ is obtained from σ by removing some occurrences of its transitions. The projection of σ on the set T ⊆ T of transitions is the maximum subsequence of σ whose transitions belong to T , noted σ T . For example, the projection of the sequence σ = t 1 t 2 t 3 t 2 on the set {t 1 , t 2 } is the sequence t 1 t 2 t 2 .

Subnets, subsystems, components and coverings. Let N = (P, T, W ) and N = (P , T , W ) be two nets. N is a subnet of N if P is a subset of P , T is a subset of T , and W is the restriction of W to (P × T ) ∪ (T × P ). S = (N , M 0 ) is a subsystem of S = (N, M 0 ) if N is a subnet of N and its initial marking M 0 is the restriction of M 0 to P , i.e. M 0 = M 0 P .

N is a P-subnet of N if N is a subnet of N and T = • P ∪ P • , the pre-and post-sets being taken in N . S = (N , M 0 ) is a P-subsystem of S = (N, M 0 ) if N is a P-subnet of N and S is the corresponding subsystem of S.

Similarly, N is a T-subnet of N if N is a subnet of N and P = • T ∪ T • , the pre-and post-sets being taken in

N . S = (N , M 0 ) is a T-subsystem of S = (N, M 0 ) if N is a T-subnet of N and S is the corresponding subsystem of S.
Notice that a T-subnet (respectively P-subnet) is not necessarily a T-net (respectively P-net).

For weighted Petri nets, we define next some particular subsystems named P-(T-)components, which have been previously defined as subnets and studied in [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF].

A (weighted) P-component S of a system S is a strongly connected, well-formed and conservative JF P-subsystem of S. A (weighted) T-component S of a system S is a strongly connected, well-formed and consistent CF T-subsystem 3 of S.

We now define the union of subnets of a net and the covering of a net by some of its subnets. Consider two nets N 1 and N 2 that are subnets of a net N . The union of

N 1 = (P 1 , T 1 , W 1 ) and N 2 = (P 2 , T 2 , W 2 ) is the net N = (P , T , W ) such that P = P 1 ∪ P 2 , T = T 1 ∪ T 2 ,
and the new weight function W inherits the weights of the arcs defined by W 1 or W 2 . Generalizing inductively to a set C of subnets, the union of

C = {C 1 , . . . , C k } is the union of C 1 and the result of the union of C \ {C 1 }. A net N is covered by a set C of subnets if N is the union of C.
Unions and coverings naturally extend to subsystems and systems by considering the associated restrictions of markings to subsets of places.

Siphons and traps. Consider a net N = (P, T, W ). A non-empty subset D ⊆ P of places is a siphon (sometimes also called a deadlock) if

• D ⊆ D • . A non-empty subset Q ⊆ P of places is a trap if Q • ⊆ • Q.
Reduced graphs. The reduced graph R of a net N is the directed graph G = (V, A) obtained from N by contracting every maximal strongly connected subnet c of N into one single node g c ∈ V . The set A of arcs represents the connections that remain after the contraction: for any two distinct nodes g u , g u of R that represent respectively the distinct subnets u, u of N , we have an arc (g u , g u ) from g u to g u if W (q, q ) > 0 in N for some q ∈ u and q ∈ u . By definition, each reduced graph is acyclic. This is illustrated on Figure 3.

In what follows, without loss of generality, we consider connected nets that contain at least a place and a transition, unless otherwise specified.

Structural deadlockability and liveness of homogeneous JF nets

Deadlockability, liveness and related properties have been studied previously in the (weighted) join-free class, notably under the conservativeness (i.e. structural boundedness) assumption [START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF][START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Silva | Linear algebraic and linear programming techniques for the analysis of place/transition net systems[END_REF][START_REF] Hujsa | Polynomial Sufficient Conditions of Well-Behavedness and Home Markings in Subclasses of Weighted Petri nets[END_REF] or in more restricted subclasses [START_REF] Mayr | Results on Equivalence, Boundedness, Liveness, and Covering Problems of BPP-Petri Nets[END_REF][START_REF] Mayr | Complexity results for problems of communication-free Petri nets and related formalisms[END_REF]. 3 Actually, strongly connected and conservative JF nets are necessarily well-formed, and strongly connected and consistent CF nets are also well-formed [START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF][START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF]. In this section, we show that the notion of sub-consistency is a fundamental algebraic property characterizing structural deadlockability in the HJF nets covered by a (unique) minimal siphon 4 . As a corollary, we obtain for the same nets that structural liveness is equivalent to non-sub-consistency. Since sub-consistency can be checked with linear programming, we deduce a polynomial-time method checking structural deadlockability or structural liveness. We then generalize these conditions to all HJF nets, by means of coverings with minimal siphons. These results are dedicated to the HJF structure and do not apply to inhomogeneous JF nets.

3 6 1 2 1 1 1 1 2 2 5 1 1 2 2 2
The characterization of structural deadlockability for the HJF nets covered by a unique (minimal) siphon arises from a series of intermediate results.

First, we study a general relationship between deadlockability, non-liveness and sub-consistency in the JF class.

Second, using previous results on the CF class, we show that strongly connected JF nets are covered by strongly connected FA T-subnets that may either decrease, preserve or generate tokens in the JF system.

Third, we provide a variant of this classification, proving that sub-consistency is equivalent to structural deadlockability in strongly connected FA nets.

Fourth, we show that each strongly connected, sub-consistent JF net contains a strongly connected, sub-consistent (structurally deadlockable) FA T-subnet.

Finally, we prove by induction on the structure of the sub-consistent HJF nets covered by a unique siphon that every marking can reach a deadlock by directing tokens towards a sub-consistent, hence deadlockable, FA T-subsystem.

To simplify the development of these statements, we reveal and exploit the graph structures corresponding to minimal siphons in join-free nets (Lemma 3.1), namely quasi strongly connected nets, defined below.

Quasi-strong connectedness and siphons. A net is called quasi strongly connected if it is connected and becomes strongly connected once we omit the transitions with no output. We will use the next correspondence with siphons. Lemma 3.1. Let N = (P, T, W ) be a connected JF net. Then, P is the unique siphon of N if and only if N is quasi strongly connected.

Proof:

Assume that P is the unique siphon of N and that N is not quasi strongly connected. Let us consider a node g without input in the (finite, acyclic) reduced graph of N ; since P is a (non-empty) siphon, g is not a single transition and contains a place, so that the subnet induced by the union of g with its output transitions defines a maximal quasi strongly connected subnet N without input node and containing a place. Since N is not quasi strongly connected, the places of N define a smaller siphon of N , a contradiction.

Conversely, if N is quasi strongly connected, then P is a siphon. Suppose that a smaller siphon P exists. For any place p ∈ P \ P , and any directed path from p to some place of P , every place of this path belongs to P (by definition of siphons and by join-freeness). Since all places of a quasi strongly connected net belong to the same unique maximal strongly connected subnet of the net, P = P , a contradiction. Hence, P is the unique siphon of N .

Relating deadlockability to non-liveness and sub-consistency

We provide next a necessary condition for structural deadlockability in JF nets. Lemma 3.2. Let N be a JF net in which every place p has at least one output transition. If N is structurally deadlockable, it is sub-consistent.

Proof:

One can choose a sufficiently large marking M 0 , with M 0 (p) ≥ W (p, t) ∀p ∈ P , ∀t ∈ p • , that enables a sequence σ containing all transitions, leading to a marking M . Since N is structurally deadlockable, a sequence σ is feasible at M that leads to a deadlock M . From join-freeness, for each place p and each output transition t of p, we have M (p) < W (p, t). Let us define τ = σ σ . The Parikh vector Ψ(τ ) satisfies Ψ(τ ) ≥ 1. Moreover, for every place p, M (p) < M 0 (p), from which we deduce I •Ψ(τ ) ≤ -1, where I is the incidence matrix of N . Thus, N is sub-consistent.

The converse does not hold: the ordinary HJF net formed of two transitions t, t , a place p and two unit-weighted arcs such that t is the input of p and t is its output, is sub-consistent (look at Ψ(tt t )) and live for every initial marking.

The next equivalence between liveness and deadlock-freeness is inspired from [START_REF] Teruel | Liveness and home states in Equal Conflict systems[END_REF][START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF], restricted to HJF nets but extended to possibly unbounded nets. Lemma 3.3. Let S = (N, M 0 ) be a quasi strongly connected HJF system. S has a non-live transition if and only if it is deadlockable.

Proof:

As usual, we consider nets with T = ∅. It is clear that the reachability of a deadlock implies non-liveness. Now, if a transition t is dead in some reachable marking M , all transitions in ( • t) • are also dead in M since the net is HJF, and since | • t| = 1 we deduce that each transition in •• t can be fired only a finite number of times from M , leading to a marking at which these transitions are dead. One can iterate this process on each directed path that reaches some dead transition, leading to a deadlock by quasi strong connectedness.

The next lemma relates structural deadlockability to non-structural liveness in the systems for which liveness is equivalent to deadlock-freeness. Lemma 3.4. Let N be a net such that, for every marking M of N , deadlock-freeness of (N, M ) implies liveness of (N, M ). Then, N is structurally deadlockable if and only if it is not structurally live.

Proof:

Structural deadlockability obviously implies non-structural liveness for all Petri nets with T = ∅. For the converse, if N is not structurally live, every marking M is non-live for this net. Then, using the assumption that non-liveness of (N, M ) implies deadlockability of (N, M ), we deduce that a deadlock is reachable from every marking M , implying structural deadlockability of N . This result applies in particular to quasi strongly connected HJF nets by Lemma 3.3.

Previous results relating JF and CF nets to their FA subclass

Basing on previous works on the FA and CF classes, we exhibit fundamental structural and behavioral properties of JF nets, expressed in terms of FA nets: strongly connected JF nets are covered by strongly connected FA T-subnets, the latter benefitting from a structural classification for liveness and boundedness. Roughly speaking, actions performed in such FA T-subnets may either decrease, preserve or generate tokens in the associated area of the JF system.

Reverse-duality and covering. Structural results may be obtained directly from known properties of the reverse-dual net, which is defined by reversing arcs and swapping places with transitions. This method has been used for CF nets, whose reverse-dual class is the JF class [START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF]. In general, the relationship between the structure of a net and its behavioral properties cannot be deduced from known properties of the reverse-dual net. However, using reverse-duality, we obtain the next variation of Lemma 10 in [START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF], getting a first glimpse of the important role played by particular FA T-subnets in the behavior of JF nets since any sequence feasible in a T-subsystem is feasible in the system. Lemma 3.5. (Reverse-dual of Lemma 10 in [START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF]) Let N be a strongly connected JF net. For each transition t of N , there is a strongly connected FA T-subnet of N containing t.

In the following, we link the structure of FA nets to their behavior.

Structural liveness of CF nets. We deduce from Corollary 4 in [START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF] the next characterization of structural liveness for CF nets, which generalize FA nets. Lemma 3.6. A CF net is structurally live if and only if it is weakly sur-consistent.

A previous classification of strongly connected FA nets. Strongly connected FA nets have been previously studied, notably in [START_REF] Teruel | Structure Theory of Weighted Place/Transition Net Systems: The Equal Conflict Hiatus[END_REF][START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF] where they are presented as a natural generalization of weighted circuits. In the same studies (page 6 in [START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF] and Section 4.1 in [START_REF] Teruel | Structure Theory of Weighted Place/Transition Net Systems: The Equal Conflict Hiatus[END_REF]), it is explained that the class of strongly connected FA nets can be partitioned into three subclasses: "neutral", when the FA net is consistent and conservative; "absorbing", when the FA net is not weakly sur-consistent; or "generating", when the FA net is not structurally bounded. Figure 4 depicts an element of each class. This partition does not apply to strongly connected JF nets, even if one tries to replace non-weak sur-consistency by sub-consistency and even for their subclass of homogeneous P-nets, as shown in Figure 5.

1 1 3 1 1 1 1 t 1 t 2 t 3 1 1 2 1 1 1 1 t 1 t 2 t 3 1 1 1 1 1 1 1 t 1 t 2 t 3
p 2 1 2 3 t 1 t 2 -1 1 [ ] 2 1 0 [ ] p t 1 t 2 -1 1 [ ] 1 1 = 0 [ ] p t 1 t 2 -1 1 [ ] 1 2 0 [ ] p t 1 t 2 Figure 5
. The inequalities on the right show the homogeneous P-net on the left to be jointly sub-consistent, consistent and sur-consistent. Hence, these three properties cannot be used alone to tri-partition the class of strongly connected homogeneous P-nets.

Hence, this classification is tightly related to the FA structure. We will show in Lemma 3.13 that non-weak sur-consistency is equivalent to sub-consistency in strongly connected FA nets.

Small nets in Petri nets and sub-consistency in JF nets

We present below the notion of small nets and introduce associated results about decompositions into T-subnets. From this development, we express a variant of the previous classification of FA nets in terms of sub-consistency, and deduce the existence of a strongly connected sub-consistent FA T-subnet in every strongly connected sub-consistent JF net.

In the sequel, the general type P used in the next definition shall be specialized to consistency, sur-consistency or sub-consistency.

Definition 3.7. ([28])

A net of type P is said to be small P if it does not contain any non-empty proper 5 T-subnet of the same type P.

In strongly connected and partially sub-consistent JF nets, the strong connectedness of small subconsistent T-subnets is revealed next. Lemma 3.8. Let N be a strongly connected, partially sub-consistent JF net. Then, every small subconsistent T-subnet of N is strongly connected. Moreover, there exists such a (non-empty) strongly connected T-subnet in N .

Proof:

Denote by I the incidence matrix of N . By partial sub-consistency, there exists a vector π 0 such that I • π 0. Let us denote by J any small sub-consistent T-subnet of N . Such a subnet exists, since the T-subnet N π of N induced by the support of π is sub-consistent. We show that J is necessarily strongly connected. Suppose that J is not strongly connected. If J is not connected, it contains a proper sub-consistent T-subnet, contradicting the fact that J is small sub-consistent. Hence, J is connected.

Consider the reduced graph R of J. It is acyclic (so that it defines a partial order), connected (since so is J) and finite (so that there are maximal nodes). Let us consider any such maximal node g, meaning that g has some input in R (otherwise g would be R and J would be strongly connected) but no output in R. We show that the subgraph corresponding to g is a strongly connected T-subnet of N that contains at least a place and a transition. By definition, g contains a node and is strongly connected.

If g is a single place, then it has an input transition in J and no output in J, so that a sub-consistency vector µ J for J cannot yield a null or negative value (when left-multiplied by the incidence matrix I J of J) for this place, a contradiction. If g is a single transition, it has no output in J, hence no output in N since J is a T-subnet of N , contradicting the strong connectedness of N .

Thus, g contains at least a place and a transition. If g is not a T-subnet of J, this means that it contains a transition t lacking an input or an output. The transition t must have its (unique, since N is JF) input place in g, since g is strongly connected. It has all its outputs in g too, since g has no output in R (hence in J \ g) by the choice of g. We obtain a contradiction, implying that g is a T-subnet of J and N . Now, we show that g is sub-consistent. Denote by I J the sub-matrix of I restricted to J. Since J is sub-consistent, we have I J • µ J 0 for some integer vector µ J ≥ 1. Since g has some input node in R, it has some input node n in J, and since g is strongly connected while J is JF, n must be a transition. Because g is a maximal strongly connected subnet of J, any input transition of (a place of) g cannot have its input place in g. Denote by g the union of the net represented by g and all its input transitions in J with the arcs going from these inputs to g. (Notice that g is a P-subnet of J. Denote by µ g and µ g the restriction of µ J to (the transitions of) g and g (so that µ g , µ g ≥ 1) and by I g , I g the incidence matrices of g, g respectively. Since g has no output in R (nor in J), hence in particular no output transition in J, we have I g • µ g ≤ 0 (we may have equality if the negative values correspond to places not in g). Let p be a place of g that is an output of n. Then, (I g • µ g )(p) < 0, and g is sub-consistent.

J thus contains a proper T-subnet of the same type, i.e. a sub-consistent one, whereas J is small sub-consistent, a contradiction. We deduce that J is strongly connected, hence the claimed property.

This result is tightly related to the JF structure and does not apply to Petri nets with synchronizations, as illustrated in Figure 6.

The next result investigates small sub-consistent FA nets.

Lemma 3.9. Let N be a strongly connected FA net. Then, N does not contain any non-empty proper strongly connected T-subnet. Moreover, if N has the property of sub-consistency it is small for this property.

p 1 p 3 p 4 1 1 3 1 2 1 1 t 1 t 3 t 4 p 1 p 3 p 4 1 1 3 2 1 t 1 t 3
Figure 6. The net on the left is strongly connected, sub-consistent and is not JF. On the right, its unique nonempty, small, sub-consistent T-subnet, is neither strongly connected nor JF.

Proof:

Let us assume that N contains a non-empty proper strongly connected T-subnet F . Hence, there exists a node in N \ F . Since N is strongly connected, there exists a node n in N \ F that is an output of a node n in F . The node n cannot be a place (since F is strongly connected and n • = {n}, we should have that n is the only node of F , but then F is not a T-subnet). Thus, n is a transition and n is an output place of n that is not in F , contradicting the fact that F is a T-subnet.

If N is sub-consistent, Lemma 3.8 applies, implying that every small sub-consistent T-subnet of N is strongly connected, and there is a non-empty one in N ; from the first part of the claim, we deduce that N is small sub-consistent.

It can be seen that the second part of the above result becomes false when sur-consistency is considered instead of sub-consistency, as examplified in Figure 7.

p 1 p 2 t 1 t 2 0 1 1 -1 1 1 = 1 0 0 0 p 1 p 2 t 1 t 2 0 1 1 [ ] = 0 1 0 0 p 1 p 2 t 1 p 1 p 2 t 1 Figure 7.
The strongly connected FA net on the left is sur-consistent, but is not small sur-consistent, since it contains the proper, non-empty sur-consistent T-subnet induced by {t 1 }, which is depicted on the right. The incidence matrices of both nets show the sur-consistency of each net.

Structural deadlockability and sub-consistency in FA nets. To characterize structural deadlockability in FA nets, we need the next technical result. Lemma 3.10. (Propositions 16a, 18a in [START_REF] Sifakis | Structural properties of Petri nets[END_REF]) If a net is small sur-consistent, then it does not contain any consistent or sub-consistent T-subnet (either proper or not). If a net is small sub-consistent, then it does not contain any consistent or sur-consistent T-subnet (either proper or not).

We are now able to deduce the following necessary and sufficient condition. Lemma 3.11. Let N be any strongly connected FA net. N is structurally deadlockable if and only if it is sub-consistent.

Proof:

If N is sub-consistent, it is small sub-consistent (by Lemma 3.9). By Lemma 3.10 it is neither consistent nor sur-consistent, hence it is not weakly sur-consistent. By Lemma 3.6, it is not structurally live. By Lemma 3.4, it is structurally deadlockable. For the converse, suppose that N is structurally deadlockable. Then, Lemma 3.2 applies.

A variant of the classification of strongly connected FA nets. By relating sub-consistency to structural deadlockability and non-weak sur-consistency, we obtain a variant of the classification of [START_REF] Teruel | Structure Theory of Weighted Place/Transition Net Systems: The Equal Conflict Hiatus[END_REF][START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF], embodied by Lemma 3.13. To achieve it, we need the next lemma. Lemma 3.12. Consider any net N = (P, T, W ) with incidence matrix I having a consistency vector π 1 and a vector π ≥ 0 such that I • π 0 or I • π 0. Then, in both cases, N is sub-consistent and sur-consistent.

Proof:

Define π = π 1 +π, so that π ≥ 1, and π = k•π 1 -π, where k is any (sufficiently large) positive integer such that π ≥ 1. If I • π 0, then π is a sub-consistency vector for N and π is a sur-consistency vector. Similarly, if I • π 0, π is a sur-consistency vector and π is a sub-consistency vector. Lemma 3.13. (Variant of the classification for FA nets) Let N be a strongly connected FA net. N satisfies exactly one of the following properties: consistency, sub-consistency or sur-consistency.

Proof:

For this class, structural liveness is equivalent to weak sur-consistency (consistency or sur-consistency) (Lemma 3.6), while non-structural liveness is equivalent to structural deadlockability (Lemma 3.4) and sub-consistency (Lemma 3.11). We deduce that this class can be partitioned into two subclasses: the sub-consistent ones and the weakly sur-consistent ones. If N is both consistent and sur-consistent, it is also sub-consistent (by Lemma 3.12), a contradiction with the previous observation. We deduce the claim.

Existence of strongly connected sub-consistent FA T-subnets. Using the new classification, the next refinement of Lemma 3.8 reveals the FA structure. Lemma 3.14. Let N be a strongly connected, partially sub-consistent JF net. Then, every small subconsistent T-subnet of N is a strongly connected FA net. Moreover, N contains such a (non-empty) strongly connected FA T-subnet.

Proof:

Applying Lemma 3.8, every small sub-consistent T-subnet of N is strongly connected, and N contains such a non-empty T-subnet J. Suppose that J is not FA. By Lemma 3.5, we know that J is covered by strongly connected FA T-subnets. Since J is small sub-consistent, none of them is sub-consistent. Then, using the new classification (Lemma 3.13), each of them is either consistent or sur-consistent. By Lemma 3.10, J does not contain any consistent T-subnet nor any sur-consistent T-subnet. We obtain a contradiction, and J is FA.

Polynomial-time intermediary characterizations

In the following, we provide two characterizations of structural deadlockability and liveness for the HJF nets covered by a unique siphon, or equivalently quasi strongly connected HJF nets by Lemma 3.1.

The next theorem investigates structural deadlockability. The main step of the proof is illustrated in Figure 8.

Theorem 3.15. (Structural deadlockability)

Consider any quasi strongly connected HJF net. It is sub-consistent if and only if it is structurally deadlockable.

Proof:

Structural deadlockability and Lemma 3.2 imply sub-consistency. We prove the other direction by induction on the number n of places with several outputs.

Base case: n = 0. If N does not contain any choice, it is either a sub-consistent strongly connected FA net, or a single output-free transition together with its unique input place. In the first case, Lemma 3.11 applies, from which we deduce structural deadlockability. We see easily that the second case also implies structural deadlockability.

Inductive case: n > 0. Since N contains choices, it is not an FA net. We suppose that the claim is true for every n < n. If N is strongly connected, Lemma 3.14 applies, and N contains a sub-consistent, strongly connected FA T-subnet F . Otherwise, N contains an output-free transition, and we denote by F the T-subnet formed of this transition with its unique input place.

Let N be the subnet of N obtained by deleting all the places of F and their outgoing transitions. If N is empty, then all the places of N belong to F , in which case firing only in F leads to a deadlock (by Lemma 3.11 if F is strongly connected, trivially in the case of two nodes), since the net is homogeneous. Otherwise, in the rest of the proof, we suppose that N is not empty.

Let N 1 , . . . , N k be all the maximal connected (not necessarily strongly connected) subnets of N . In the following, we prove these subnets to be structurally deadlockable. Consider any such net N i . It cannot contain a transition without input, since such transitions do not occur in N and all outputs of the deleted places were deleted. Thus, since it is not empty, it contains a place.

Since all places of N belong to a same unique maximal strongly connected subnet of N , there is in N a directed path from a place of F to any place in N i , and reciprocally. Consequently, there is a deleted node u (not in N i ) input of some node in N i . Since each transition of N i has an input place in N i , and N is JF, u is a transition. By definition of N , the input place of u, and each input place of every other transition of the same kind, are deleted places and cannot belong to N i . Moreover, all the transitions of N that are outputs of places of N i have not been deleted and belong to N i , since otherwise their input would have been deleted. Let I be the incidence matrix of N and π be a sub-consistency vector for N . In the sequel, each union of a transition t with a subnet g of a net h is the net containing g, t and all arcs between t and g in h. We have two cases.

First case. Suppose that N i is quasi strongly connected. A transition t exists in N that has been deleted and is an input of N i , the input of t not being in N i . Also recall that N i has no output transition in N \ N i . Denote by N i the union of N i with its deleted input transitions (and the arcs from these transitions to N i ). If I i (respectively I i ) is the incidence matrix of N i (respectively N i ), the projection π i of π to N i satisfies I i • π i ≤ 0. Denoting by π i the projection of π to N i , we deduce that I i • π i 0: N i is sub-consistent. Since it is quasi strongly connected and contains strictly fewer choices than N , the induction hypothesis applies, and N i is structurally deadlockable.

Second case. Otherwise, suppose that N i has a different structure; it is not strongly connected. Recall that N i does not contain any transition having no input. Denote by R its reduced graph. Consider any node g of R that contains at least one place and one transition. If no such g exists in R, which is acyclic, it is clear that N i is structurally deadlockable. We consider the next cases for g.

Case a. If g has no input in R, it has some output in R, because N i is not strongly connected. g has necessarily a deleted input transition whose input has been deleted. Similarly to the "First case", the union of g with its deleted input transitions and its possible output transitions is a sub-consistent or consistent net. Thus, the union of g with its possible outgoing transitions is a sub-consistent subnet of N i that is quasi strongly connected.

Case b. If g has some input transition and some output in R, similarly to the previous cases, the union of g with its possible output transitions satisfies sub-consistency and is quasi strongly connected.

Case c. If g has some input transition in R and no output in R, it may have only output places in N . Using similar arguments as before, g satisfies sub-consistency and is quasi strongly connected.

In all cases, the induction hypothesis can be applied to the union of g with its possible output transitions, which all belong to N i . We deduce that every such subnet of N i is structurally deadlockable. By following the partial order defined by R on its directed paths, starting from the smallest nodes of R for this order (i.e. with no input in R), selecting adequate outputs in choice-places (always possible due to homogeneity) if needed, every node of R can be successively deadlocked, finally deadlocking N i .

Thus, N i is always structurally deadlockable. Its possible inputs in N are necessarily deleted transitions, while its possible outputs are necessarily deleted places. Since all deleted places belong to a structurally deadlockable T-subnet F of N , all the tokens produced in such places when deadlocking all N j , 1 ≤ j ≤ k, can be decreased by only firing transitions in F (since F is a T -subnet, and it is structurally deadlockable) until F deadlocks. Moreover, no deleted input transition of any N i is a transition of F ; thus, by homogeneity, one can fire in F while never firing such inputs of N i , and new tokens will not be produced in any N i in the process. We deduce that a firing sequence always exists that deadlocks all N i 's first, then deadlocks F , reaching a global deadlock. Figure 8 depicts three quasi strongly connected HJF nets 6 . The first one is structurally live and not sub-consistent; the second and the third ones are sub-consistent, thus structurally deadlockable.

We are now able to deduce the next corollary for structural liveness.

Corollary 3.16. (Structural liveness)

Consider a quasi strongly connected HJF net. It is structurally live if and only if it is not sub-consistent.

Proof:

If such a net is sub-consistent, then it is structurally deadlockable by Theorem 3.15, thus not structurally live. For the converse, if it is not structurally live, it is structurally deadlockable (Lemmas 3.3 and 3.4) and sub-consistent by Lemma 3.2.

Polynomial-time complexity. Checking the existence of a rational solution to I • Y 0, Y ≥ 1, and computing one when it exists, can be done in polynomial time with linear programming [START_REF] Grötschel | Geometric algorithms and combinatorial optimization[END_REF][START_REF] Silva | Linear algebraic and linear programming techniques for the analysis of place/transition net systems[END_REF].

p 1 p 2 p 3 1 1 1 1 1 1 1 1 t 1 t 2 t 3 t 4 p 1 p 2 p 3 1 1 3 1 1 2 2 1 t 1 t 2 t 3 t 4 p 1 p 2 p 3 p 4 1 1 3 1 1 2 2 t 1 t 2 t 3 1 1 2 1 t 4 t 5
Figure 8. Three quasi strongly connected HJF nets are pictured. On the left, it is not sub-consistent, hence it is structurally live (a token in p 1 yields liveness). The nets in the middle and on the right are sub-consistent. In both of them, there is a structurally deadlockable FA T subnet: the T-subnet F induced by t 4 in the middle, the T-subnet F induced by {t 4 , t 5 } on the right. In the proof, after the deletion of F and F with their outgoing transitions, the cycle t 1 p 1 t 3 p 3 remains in both nets. This cycle is strongly connected and sub-consistent, thus it can deadlock; when firings in this cycle occur in the initial nets (before deletion), tokens are produced only in p 2 , and t 2 shall never be fired. After the cycle deadlocks, F and F deadlock, inducing a global deadlock.

Multiplying this solution by an adequate rational number, we get an integer solution. Thus, Theorem 3.15 and Corollary 3.16 can be checked in polynomial time.

Generalization of the conditions to all HJF nets

A simple necessary condition for structural deadlockability is stated next. Lemma 3.17. If a net (P, T, W ) is structurally deadlockable, then P is a siphon.

Proof:

If P is not a siphon, then • P ⊆ P • , meaning that some input transition of some place in P has no input place: such a transition is always fireable, contradicting deadlockability. Thus, P is a siphon.

In Theorem 3.15 and Corollary 3.16, the nets considered are quasi strongly connected. Their set of places is their unique siphon by Lemma 3.1. We generalize Theorem 3.15 and Corollary 3.16 through the two following corollaries.

Corollary 3.18. (Structural deadlockability)

Consider a connected HJF net N = (P, T, W ). Denote by C the set of all the maximal quasi strongly connected subnets of N that contain at least one place and one transition. N is structurally deadlockable if and only if P is a siphon and each element of C is sub-consistent.

Proof:

Assume that N is structurally deadlockable. P is a siphon by Lemma 3.17. Consider a non-subconsistent element c of C. By Corollary 3.16, c is structurally live. In N , the outputs of nodes of c that do not belong to c may only be places while the inputs of nodes of c that do not belong to c may only be transitions: in the first case, each output transition belongs to c since c is a maximal quasi strongly connected subnet; in the second case, an input place would be the unique input of a transition t, such that t has no input in c, contradicting the definition of c. Thus, c remains structurally live in N , contradicting deadlockability.

Conversely, each element of c is sub-consistent and HJF, hence structurally deadlockable (Theorem 3.15). For each place p of N , either p has no output, or the maximal quasi strongly connected subnet containing p has a transition, belongs to C and is structurally deadlockable. Since P is a siphon, each transition of N has an input. Hence, for every marking M 0 , (N, M 0 ) can be deadlocked by following the paths of the reduced graph R of N , since each node of R denotes either a place with no output or a subnet of an element of C.

Corollary 3.19. (Structural liveness)

Let N = (P, T, W ) be a connected HJF net. Let C be the set of maximal quasi strongly connected subnets of N with no input node in N and containing a place and a transition. Then, N is structurally live if and only if no element of C is sub-consistent.

Proof:

If N is quasi strongly connected, then C contains only N , Corollary 3.16 applies and we obtain the claim. Otherwise, we suppose in the following that N is not quasi strongly connected, implying that each element of C has an output place in N (by connectedness and by definition of C).

If an element of C is sub-consistent, it is structurally deadlockable (by Theorem 3.15 since it is also HJF) with no input, hence N cannot be structurally live.

Conversely, if no element of C is sub-consistent, each is structurally live (by Corollary 3.16). Thus, there exists a marking for which all elements of C are live. Such live subsystems can generate an arbitrarily large number of tokens in their output places in N . There may also exist nodes without input, which are necessarily single transitions, hence also live subsystems. By join-freeness and homogeneity, an arbitrarily large number of tokens can reach each place of the system by following the directed paths in the reduced graph of N . We deduce structural liveness.

Polynomial-time complexity. The set of the maximal quasi strongly connected subnets of a join-free net forms a partition (or disjoint covering) of its nodes. Thus, the number of these subnets is linear in the size of the system. Determining these subnets and checking their sub-consistency are polynomial-time problems, and the conditions of Corollaries 3.18 and 3.19 can be checked in polynomial-time.

Improvements on a previous work on HAC nets

In this section, we focus on results of [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF]. First, we observe that the pureness assumption used in [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF], which forbids self-loops (i.e. nodes x such that • x ∩ x • = ∅), is not necessary. Then, we exhibit an incorrect argument of a proof in one of the central theorems of the same paper, which is based on quasi strongly connected HJF subnets. Finally, we correct this proof using Theorem 3.15.

Unnecessary pureness

The assumption of pureness, which forbids self-loops, is only exploited in the proof of the very first lemma of [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF] (Lemma 3.1), which is used in various later occasions. We provide next a refined proof of this lemma, leaving out the pureness assumption. From Theorem 3.2 in the same paper [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF], we know that (N D , M D 0 ) is live. Let us now proceed by contradiction and assume that (N D , M D 0 ) is unbounded. Since it is known that live and bounded Petri nets are consistent [START_REF] Silva | Linear algebraic and linear programming techniques for the analysis of place/transition net systems[END_REF], the net N is consistent. Hence, every P-subnet induced by any subset of places is also consistent. In particular, this is also the case for N D . If a system is unbounded, the underlying net is not structurally bounded. We recall the next characterization for this property, which can be found in various studies, e.g. in [START_REF] Silva | Linear algebraic and linear programming techniques for the analysis of place/transition net systems[END_REF].

Lemma 4.3. (Structural boundedness: Corollary 16 in [14])

A net with incidence matrix I is not structurally bounded if and only if there exists a vector X 0 such that I • X 0.

Applying Lemma 3.12, we get the sub-consistency and sur-consistency of N D . Each minimal siphon of an HAC net induces a quasi strongly connected HJF P-subnet (by [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF] and Lemma 3.1). Applying Theorem 3.15, N D is structurally deadlockable, contradicting the liveness of (N D , M D 0 ), which must thus be bounded. We deduce the validity of Theorem 5.2 in [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF].

Non-monotonic properties of inhomogeneous JF nets

Liveness, deadlockability, reversibility and boundedness, among other behavioral properties, are not always monotonic in weighted Petri nets. In this section, we delineate more sharply the frontier between the monotonicity of these properties and their non-monotonicity in subclasses of weighted Petri nets, notably in JF nets 7 .

Non-monotonic liveness. Liveness is known to be non-monotonic in some bounded HAC systems [START_REF] Heiner | On the Importance of the Deadlock Trap Property for Monotonic Liveness[END_REF] and monotonic in HFC nets (hence also in OFC and HJF nets) as well as in some other classes [START_REF] Desel | Free Choice Petri Nets[END_REF][START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Recalde | Modeling and analysis of sequential processes that cooperate through buffers[END_REF]. On the left of Figure 9, we show that liveness is not monotonic in the inhomogeneous JF class, even under the strong connectedness assumption. On the right of the same figure, we provide, as far as we know, the first structurally bounded, live, non m-live join-free system. Notice that this system is also reversible.

Non-monotonic reversibility. Reversibility is not always monotonic in structurally bounded Petri nets, even in the most basic cases. A simple example is a Petri net with one place p, one transition t and one unit-weighted arc going from p to t: if p does not contain any token, then the system is reversible, and the reachability graph contains only one marking; a single token in p allows to fire t once, leading to a deadlock, implying that the system is not reversible.

More relevant is m-liveness+reversibility, meaning monotonicity of both properties taken together, under the structural boundedness assumption. Indeed, these three properties are required by many applications, such as embedded systems. It has been shown in [START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF] that m-liveness+reversibility applies to all HFC nets, meaning that each live and reversible HFC system remains live and reversible upon any addition of tokens. Since all HJF nets are included in this class, they also satisfy m-liveness+reversibility.

However, when leaving out homogeneity, we show that reversibility is not always monotonic in JF nets, even if liveness and structural boundedness are assumed. Adding one token to p 3 on the right of

p 1 p 2 t 1 t 2 t 3 1 2 1 2 2 3 3 p 1 p 3 p 4 2 5 3 1 1 2 2 1 1 3 3 3 3 1 2 2 1 5 4 4 1 t 1 t 2 t 3 t 4 t 5 t 6 t 7 t 8 p 2 p 5
Figure 9. The live and strongly connected but unbounded JF system on the left is not m-live, since adding a token to p 1 allows to fire t 2 , leading to a deadlock. On the right, the JF system is strongly connected, structurally bounded (since it is 1-conservative), live and reversible; however, it is not m-live, since adding a token to p 3 and firing two times t 4 leads to a deadlock.

Figure 9 yields a first counter-example: firing two times t 4 leads to a deadlock, from which the initial marking cannot be reached. Another counter-example is derived from the same net by replacing the initial marking with the larger one (3, 1, 4, 0, 1): the system obtained is still live, but is no more reversible. Hence, liveness and reversibility are not monotonic in the class of JF nets, even when considered together and when structural boundedness is assumed.

Non-monotonic non-deadlockability. Adding a token to p 3 in the reversible and live, hence nondeadlockable, system on the right of Figure 9 provides a deadlockable initial marking. Thus, nondeadlockability is not monotonic in well-formed, reversible JF nets.

Reversibility of live systems: from homogeneity to inhomogeneity

Reversibility has been characterized non-trivially in several Petri net subclasses, leading to polynomialtime checking conditions, for instance in live OFC and HFC nets [START_REF] Desel | Free Choice Petri Nets[END_REF][START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF][START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF], some of which are sufficient but not necessary. One of these characterizations uses the notion of a T-sequence, defined as follows and exploited later in this section. Definition 6.1. (T-sequence [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF]) Consider a Petri net system S whose set of transitions is T , and denote by I its incidence matrix. A firing sequence σ of S is a T-sequence if it contains all transitions of T and I • Ψ(σ) = 0.

As a consequence of this definition, if a T-sequence is feasible in a system S = (N, M 0 ), its firing leads to the same marking M 0 and defines a circuit in the reachability graph of S.

For any Petri net system S = (N, M 0 ), the existence of a T-sequence feasible in S is a necessary condition for the liveness and reversibility-taken together-of S. In the HFC class, under the liveness assumption, the existence of an initially feasible T-sequence implies reversibility and its monotonicity [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF][START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF], as recalled next. Proposition 6.2. (M-reversibility of live HFC (or EC) systems [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF]) Consider a live Equal-Conflict (i.e. HFC) system S = (N, M 0 ) with N = (P, T, W ). The system S is m-reversible if and only if it enables a T-sequence.

Hence, this characterization also applies to live HJF nets. However, this result cannot be used for inhomogeneous JF nets, as detailed hereunder.

A limit for Proposition 6.2: inhomogeneous JF nets. We show that the existence of a feasible T-sequence in a live and structurally bounded JF system does not always induce reversibility, contrasting with the homogeneous case of Proposition 6.2: in Figure 9, the system on the right is live and reversible, thus enables a T-sequence; considering the same net with the larger marking (3, 1, 4, 0, 1), thus enabling the same T-sequence, liveness is retained while reversibility is lifted. An example of such a feasible T-sequence is α = (t 2 ) 3 (t 3 ) 2 (t 2 ) 2 t 3 t 1 t 3 t 6 t 5 t 6 t 4 t 8 t 7 t 3 t 6 t 4 t 8 t 7 .

In this section, we adapt a method of [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF] developed for live HFC systems to the case of live, strongly connected, inhomogeneous JF systems, leading to sufficient conditions of reversibility for the latter.

A previous method for reaching the initial marking in live HFC systems. In the HFC case, liveness and the existence of a feasible T-sequence are sufficient for reversibility, as described in Proposition 6.2. The proof of this result in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF] uses the following idea, assuming the existence of a feasible Tsequence σ r : for each set E of conflicting transitions (sharing an input place), the maximal subsequence of σ r that contains only transitions of E induces a local ordering that solves the associated conflicts (or choices); then, for any firing sequence σ feasible at the initial marking and leading to a marking M , one can reach the initial marking from M by firing transitions according to these orderings.

These proofs use the assumption of liveness and the structure of HFC nets: by liveness, one can always fire a transition; by homogeneity and by the free-choice structure, two conflicting transitions are either both enabled or both disabled by a marking. These assumptions ensure that any conflict resolution policy is achievable, in particular a policy leading to the initial marking.

To illustrate, an HJF system, hence an HFC system, is pictured on the left of Figure 10. Denoting by E the set {t 2 , t 3 } of conflicting transitions of this homogeneous system, and by σ r the T-sequence t 2 t 1 t 3 t 4 t 5 t 2 , the associated local ordering is t 2 t 3 t 2 . Then, if t 3 is fired first, the idea is to fire transitions until p 2 becomes enabled and t 2 is fired, implying that the prefix t 2 t 3 of the local ordering t 2 t 3 t 2 has been fired in a permuted fashion. Thereafter, the ordering can be used again as a policy solving the conflicts in E: the next transition to be fired in E is t 2 .

Extending the method to reach the initial marking in live, strongly connected, JF systems. So as to extend these steps to the inhomogeneous JF case, we simulate homogeneity with the help of enabled places: by firing only output transitions of enabled places, a conflict resolution policy can be constructed as in the homogeneous case. Since JF nets do not have synchronizations, all the transitions in the postset of an enabled place are enabled. We will provide an algorithm that complies with this constraint and that constructs a sequence leading to the initial marking. We shall deduce from it the following: if a T-sequence is feasible initially and every reachable marking enables some place, then the JF system is live and reversible.

To illustrate, an inhomogeneous JF system is pictured on the right of Figure 10. This system enables a T-sequence that is also enabled in the HJF system on the left. Using this T-sequence and the fact that each reachable marking enables some place, we will show that the initial marking can be reached from any reachable marking, which is highlighted in this example. We develop several conditions ensuring reversibility in live and strongly connected JF nets in the rest of this section, which is organized as follows.

First, we formalize in Subsection 6.1 notions and notations useful to this purpose. Second, in Subsection 6.2, we develop a general sufficient condition of reversibility for live, strongly connected JF nets, based on the existence of particular enabled places and on a feasible T-sequence. This result is a variation of Proposition 6.2. To achieve it, we derive variants of the proofs of Section 4 in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF].

Third, using this new condition in Subsection 6.3, we construct, for well-formed JF nets, a set of m-live+reversible markings in which the amount of tokens is not greater than the sum of the weights. Since every larger marking maintains the system live and reversible, we obtain a wide-ranging polynomial-time sufficient condition ensuring these properties.

Finally, in Subsection 6.4, we provide sufficient conditions of liveness and reversibility in the more restricted P-system (or S-system) case.

Additional notions and notations

To investigate the reversibility property, we borrow the following concepts from [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF][START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF]. Let S = (N, M 0 ) be any weighted system with N = (P, T, W ) and let σ be a sequence feasible in S.

Concatenation σ n : For a sequence σ and a positive integer n, σ n denotes the concatenation of σ taken n times, and σ ∞ denotes its infinite concatenation. Prefix sequence K n t i (σ): Assuming t i occurs at least n times in σ, with n ≥ 1, the largest prefix reachable marking enables some place, then the system is reversible. This result is a variation of Proposition 6.2. To achieve it, we derive variants of the proofs for HFC nets in Section 4 in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF], pointing out the differences between the HFC case and the JF case.

In [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF], for any live HFC system with a feasible T-sequence σ r , two algorithms are presented that construct, after any single firing of any transition, a firing sequence leading to the initial marking. These algorithms form two consecutive steps:

• After the firing of some transition t from the initial marking, Algorithm 1 fires transitions by following local orderings until all delayed occurrences are fired. The sequence obtained is denoted by σ t .

• Then, Algorithm 2 applies to the sequence tσ t resulting from Algorithm 1 and completes this sequence to reach the initial marking. The sequence obtained is denoted by σ t .

At the end, we obtain the sequence tσ t σ t whose Parikh vector is a multiple of the Parikh vector of the initial T-sequence σ r , hence it is also a T-sequence. These two steps are depicted in Figure 11.

M t M 0 M t t σ r σ t σ t Figure 11
. If the sequence σ r is feasible and t is fired, then Algorithm 1 builds the sequence σ t and Algorithm 2 computes the sequence σ t , which returns to the initial marking.

Once the existence of such sequences is proved, the method can be generalized to arbitrary sequences, constructing, from any reachable marking, some sequence that leads to the initial marking.

In the sequel, we consider any strongly connected JF system S = (N, M 0 ) enabling a T-sequence and such that each marking reachable in S enables at least one place. For each algorithm, we design a variant applying to S.

In [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF][START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF], an equal-conflict set E of a net N = (P, T, W ) is defined as a maximal subset of conflicting transitions such that, for all transitions t i , t j ∈ E, t i and t j have the same pre-set and, for each place p ∈ • t i , W (p, t i ) = W (p, t j ). In the case of strongly connected JF nets that contain at least two nodes, since synchronizations are not allowed, each transition has a unique input place, and we replace the equal-conflict sets by the post-sets of places in each algorithm.

We deduce Algorithm 1 below from Algorithm 1 in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF], replacing notably E t by p • , where E t denotes the equal-conflict set containing t and where p is the unique input place of t in the JF net considered. The inner loop terminates when p becomes enabled.

Algorithm 1 considers an initial firing of a single transition t and follows the local orderings induced by the T-sequence in some enabled places until all the delayed occurrences are fired. Otherwise, when no occurrence is delayed after the first firing of t, the result obtained is the empty sequence. An application of Algorithm 1 is given in Figure 12.

Algorithm 2, presented next, completes the sequence constructed by Algorithm 1 and leads to the initial marking, as illustrated in Figure 13 with the particular case that = 1.

Algorithm 2: Computation of the feasible sequence σ t after the end of Algorithm 1.

Data:

The sequences α = t σ t and κ = σ r , where ≥ 1 is the smallest integer such that

Ψ(α) ≤ • Ψ(σ r ); the marking M t such that M 0 α -→ M t Result: A completion sequence σ t that is feasible in (N, M t ) such that M t σ t -→ M 0 1 while Ψ(α) = Ψ(κ) do 2
Fire the transition t i whose next occurrence after its Ψ(α)(t i )-th appears first in κ;

α := α t i ; 4 end 5 α is of the form t σ t σ t ; 6 return σ t
The following theorem shows that Algorithm 2 is valid and terminates. It is a variant of Theorem 2 in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF]. Theorem 6.5. Let S = (N, M 0 ) be a strongly connected JF system, with N = (P, T, W ), in which a T-sequence σ r is feasible and every reachable marking enables some place. For every transition t enabled by M 0 such that M 0 t -→ M t , consider the sequence σ = σ t σ t , where σ t is constructed from M t by Algorithm 1 and σ t is built by Algorithm 2 after the execution of Algorithm 1. Then, σ = t σ is a T-sequence feasible in S and satisfying Ψ(σ) = k • Ψ(σ r ) for some integer k ≥ 1.

Proof:

In the proof of [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF], we replace each set E t i with ( • t i ) • . We use Lemma 6.4 and the rest of the proof remains the same.

p 1 p 2 p 3 p 4 t 1 t 2 t 3 t 4 t 5 2 1 1 2 1 1 1 2 1 1 3 3 p 1 p 2 p 3 p 4 t 1 t 2 t 3 t 4 t 5 2 1 1 2 1 1 1 2 1 1 3 3 Figure 13.
The marking reached at the end of Algorithm 1 by firing α = t 3 t 4 t 5 t 2 in the system on the left of Figure 12 is depicted on the left. Applying Algorithm 2 to this marking, the sequence t 1 t 2 is fired, completing α such that the initial marking is reached again, as shown on the right. In this example, the sequence of firings corresponding to t σ t σ t in Figure 11 is t 3 t 4 t 5 t 2 t 1 t 2 , whose Parikh vector equals Ψ(σ r ). Here, = 1 and κ = σ r .

We are now able to derive the next sufficient condition of reversibility, whose proof is illustrated in Figure 14. It is a variant of Corollary 1 in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF]. Corollary 6.6. Consider a strongly connected JF system S = (N, M 0 ), with N = (P, T, W ), in which every reachable marking enables at least one place. If S enables a T-sequence, then it is reversible.

Proof:

We prove by induction on the length n of any feasible sequence σ that, after the firing of this sequence, another sequence is feasible that leads to the initial marking. More precisely, we mimic the proof of Corollary 1 in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF] by replacing the property P(n) with the following one: "Consider a strongly connected JF system S = (N, M 0 ) enabling a T-sequence σ r and a sequence σ of length n such that every reachable marking enables some place. There exists a firing sequence σ such that M 0 σ σ -→ M 0 ." The main steps are illustrated in Figure 14.

The base case, with n = 0, is clear: σ = . For the inductive case, let us suppose that P(n -1) is true and let us write σ = t σ . The firing of t from M 0 leads to a marking M , and σ leads to M . Theorem 6.5 applies: a sequence σ t is feasible at M , leading to M 0 , such that t σ t is a T-sequence.

Since every marking M reachable from M enables at least one place, and σ t t is a T-sequence feasible at M , the induction hypothesis applies to (N, M ) and σ of length n -1, and a sequence σ exists that is feasible from M and leads to M . Thus, after the firing of σ, the sequence σ = σ σ t leads to the initial marking. We deduce reversibility.

M 0 M M t σ σ t σ σ r
Figure 14. Illustration of the general case in the proof of Corollary 6.6.

M-live+reversible markings for well-formed JF nets

As shown earlier, some strongly connected, structurally bounded, live and reversible JF nets are neither m-live nor m-reversible. In this subsection, using Corollary 6.6, we provide for this class a set of live and reversible markings with a number of tokens not greater than the sum of the weights. Since every larger marking also satisfies these properties, we obtain a wide-ranging polynomial-time sufficient condition of m-liveness+reversibility.

To get this result, we first need to introduce some definitions and develop a related property below, taking inspiration from [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF]. Definition 6.7. A system is T-decomposable if and only if it is covered by the set, called cover, of its T-components. Definition 6.8. (Conflict relations [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF]) Consider a net N = (P, T, W ) and two transitions t, t in T . We are now able to deduce the m-live+reversible markings for well-formed JF nets by combining Theorem 6.9 with results of [START_REF] Delosme | Polynomial Sufficient Conditions of Well-Behavedness for Weighted Join-Free and Choice-Free Systems[END_REF][START_REF] Hujsa | Polynomial Sufficient Conditions of Well-Behavedness and Home Markings in Subclasses of Weighted Petri nets[END_REF][START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF]. For that purpose, we denote by max p the maximum output weight of the place p and by gcd p the greatest common divisor of all the input and output weights of p. Theorem 6.10. (Polynomial-time sufficient condition of m-liveness+reversibility) Consider a strongly connected, well-formed JF system S = (N, M 0 ), with N = (P, T, W ), such that, for an arbitrary place p, M 0 (p) = max p , and for every other place p , M 0 (p ) = max p -gcd p . Then S is m-live and m-reversible.

Proof: S has the following particularities, proved in [START_REF] Delosme | Polynomial Sufficient Conditions of Well-Behavedness for Weighted Join-Free and Choice-Free Systems[END_REF][START_REF] Hujsa | Polynomial Sufficient Conditions of Well-Behavedness and Home Markings in Subclasses of Weighted Petri nets[END_REF]: at each reachable marking M , some place is enabled by M , implying the liveness of S. Moreover, every larger marking satisfies these properties.

It remains to prove that S enables a T-sequence.

Since N is well-formed and strongly connected, Theorem 6.9 applies and S is T-decomposable. Consequently, S satisfies the definition of the system ζ defined in Subsection 6.4 of [START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF].

Finally, we apply Theorem 6.12 of [START_REF] Hujsa | On Liveness and Reversibility of Equal-Conflict Petri Nets[END_REF], which states that ζ enables a T-sequence. Thus, S enables a T-sequence and Corollary 6.6 applies, implying the reversibility of S. Moreover, as detailed at the beginning of this proof, the assumptions on S are preserved by all the markings larger than M 0 . Furthermore, every larger marking also enables the same T-sequence.

We deduce the claim.

None of the JF systems depicted in Figures 10, 12 and 13 fulfills the conditions of Theorem 6.10, but the system in Figure 15 does, hence is m-live+reversible. The well-formedness of a JF net can be checked in polynomial time [START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF][START_REF] Teruel | Choice-Free Petri nets: a model for deterministic concurrent systems with bulk services and arrivals[END_REF], as well as the other conditions of the theorem.

Note that the marking depicted in Figure 15 can be reached in the system on the right of Figure 13 by firing two times t 4 . Then, from this marking, a multiple of the T-sequence can be completed to reach the initial marking again, since the input place of t 4 has only one output and thus, no delay is created by the firings of t 4 . We deduce the m-liveness+reversibility of all the JF systems in Figures 10,[START_REF] Barkaoui | A polynomial-time graph algorithm to decide liveness of some basic classes of bounded Petri nets[END_REF]

Sufficient conditions of reversibility for subclasses of live S-systems

We provide next a new sufficient condition of reversibility dedicated to the subclass of strongly connected S-nets, in which each transition has exactly one input and one output.

Theorem 6.11. Let S = (N, M 0 ) be a strongly connected, well-formed S-system in which every reachable marking enables some place. If M 0 enables exactly one place, then S is reversible.

Proof:

By Theorem 6.9, N is T-decomposable, meaning that each node belongs to some T-component of N . In the case of S-nets, each T-component is a well-formed circuit T-subsystem. Consider the unique place p enabled by M 0 . For each output transition t of p, t is enabled and belongs to some well-formed circuit T-subnet C (from the above). If the unique output of t is p, then the firing of t leads to M 0 again (since its input weight equals its output weight, from well-formedness). Otherwise, since the unique output of t is different from p, and since p is enabled, one can fire only occurrences of t until p becomes disabled at some marking M . Since M enables at least one place and p is the only place enabled by M 0 , the output p of t is the only place enabled by M .

This process can be iterated on any directed elementary10 path starting from p , for example in the circuit T-subnet C, implying the liveness and reversibility of the circuit T-subsystems induced by C at M 0 and M (since every well-formed and live circuit Petri net is reversible [START_REF] Teruel | On weighted T-systems[END_REF]). Now, by strong connectedness, for every transition t of the system, consider a directed elementary path µ = p t 1 p 1 . . . p t t. We prove by induction on the number n of transitions in µ that a sequence is feasible in S that contains all transitions in µ and leads to the initial marking M 0 .

If n = 1, from the above, t 1 can be fired from M 0 within a reversible circuit T-subsystem, hence the claim.

If n > 1, we assume the property to be true for every n < n. We fire t 1 until p is disabled, leading to a marking M 1 such that p 1 is the only place enabled by M 1 . Applying the inductive hypothesis to the number n -1 of transitions in the suffix µ 1 = p 1 . . . p t t of µ, there exists a sequence σ 1 feasible at M 1 , containing the transitions of µ 1 and leading to M 1 . Since M 0 is reachable from M 1 by firing inside a reversible circuit T-subsystem containing t 1 (from the case n = 1), we prove the inductive step (the desired sequence being the concatenation of the first firings of t 1 with σ 1 and the last firings in the circuit).

Thus, for every n, the property is true. We deduce that a sequence is feasible at M 0 that contains all transitions and reaches M 0 , i.e. a T-sequence is feasible in S. Applying Corollary 6.6, S is reversible.

We deduce a variant of Theorem 6.11 for the homogeneous case, embodied by the next sufficient condition. Corollary 6.12. Let S = (N, M 0 ) be a strongly connected, structurally bounded, live, homogeneous S-system. If M 0 enables exactly one place, then S is m-live+reversible.

Proof:

S is structurally bounded and live, thus well-formed. Since S is homogeneous and live, every reachable marking enables at least one place, and Theorem 6.11 applies. Moreover, in HFC systems, hence in homogeneous S-systems, liveness is monotonic, and, under the liveness assumption, reversibility is monotonic (Proposition 6.2). Hence the result.

Conclusion and perspectives

Join-free nets, which forbid synchronizations, form a fundamental subclass of weighted Petri nets. They constitute essential building blocks of more complex classes with synchronizations, allowing to deduce the behavior of systems from synchronizations of actions performed in their join-free subsystems. The monotonicity of behavioral properties, meaning their preservation upon any increase of the marking considered, is also tightly related to the monotonicity of relevant subsystems, which appear to be join-free in several classes, such as asymmetric-choice nets. In previous works, decomposition techniques, typically bottom-up approaches, have led to several polynomial-time sufficient methods checking usually intractable properties such as liveness and reversibility. In this paper, we sharpened and extended the work of [START_REF] Hujsa | On Liveness and Deadlockability in Subclasses of Weighted Petri Nets[END_REF] by providing more details and studying the reversibility property in conjunction with liveness and non-deadlockability. We developed further the structure theory of these properties in subclasses of weighted Petri nets that are composed of join-free modules.

For the homogeneous join-free nets, in which each place has all its ouput weights equal, we obtained polynomial-time characterizations of structural deadlockability and structural liveness, analyzing the underlying net only.

Using part of this new material, we corrected a previous erroneous proof of a characterization of monotonic liveness and boundedness in the homogeneous asymmetric-choice class, based on a decomposition into homogeneous join-free nets. Also, we delineated more sharply the frontier between monotonicity and non-monotonicity for liveness, non-deadlockability and reversibility in weighted Petri nets. Remarkably, this frontier appears already in the inhomogeneous join-free class under the structural liveness and structural boundedness assumptions.

Despite this frontier, we provided sufficient conditions for liveness, reversibility and their monotonicity in strongly connected join-free nets. One of them presents a set of monotonically live and reversible markings in which the number of tokens is not greater than the sum of the weights of the net, inducing a wide-ranging polynomial-time sufficient condition of m-liveness+reversibility. We also dedicated variants of these sufficient conditions to the weighted S-nets, a subclass of the join-free nets in which each transition has at most one input and one output.

These results enrich the set of efficient structural analysis techniques for weighted Petri nets. Perspectives encompass refinements and generalizations of these methods for asymmetric-choice nets and other modular classes, so as to obtain polynomial-time checking methods through bottomup approaches. For that purpose, we feel that new efficient conditions of decomposability for more expressive classes would be worth investigating. Various applications, including embedded systems, should benefit from these advances in the future.

Figure 4 .

 4 Figure 4. From left to right: an absorbing, a neutral and a generating FA net.

Lemma 4 . 1 .

 41 (Lemma 3.1 in[START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF]) Let N be an HAC net. If t is the only non-live transition from marking M 0 , there exists p ∈ • t and M ∈ [M 0 such that {p} is a siphon and M (p) < W (p, t).

  p

3

 3

  and 13, without the need of computing any T-sequence in this particular case.

Figure 15 .

 15 Figure 15. This JF system satisfies the conditions of Theorem 6.10: denoting its initial marking by M 0 , we haveM 0 (p 1 ) = max p1 -gcd p1 = 2 -1, M 0 (p 2 ) = max p2 = 2, M 0 (p 3 ) = max p3 -gcd p3 = 1 -1 and M 0 (p 4 ) = max p4 -gcd p4 = 3 -1.Hence it is m-live+reversible.

Table 1

 1

. Summary of results. The properties of liveness, deadlockability, reversibility and boundedness are denoted respectively by L, D, R and B. We denote by D the property of non-deadlockability.

  • A transition t is dead in S if no marking of [M 0 enables t. A deadlock, or dead marking, is a marking enabling no transition. S is deadlock-free if no deadlock belongs to [M 0 ; otherwise it is deadlockable. The net N is structurally deadlockable if, for every marking M , (N, M ) is deadlockable.

	• A transition t is live in S if for every marking M in [M 0 , there is a marking M in [M enabling
	t. S is live if every transition is live in S. N is structurally live if a marking M exists such that
	(N, M ) is live.
	• A marking M is a home state of S if it can be reached from every marking in [M 0 . S is reversible
	if its initial marking is a home state, meaning that RG(S) is strongly connected.

• S is bounded if an integer k exists such that: ∀M ∈ [M 0 , for each place p, M (p) ≤ k . N is structurally bounded if (N, M ) is bounded for each M .

  Figure1. The net on the left is HFC, the second one is HAC. The third net is homogeneous, non-AC since • t 1 = {p 1 , p 2 }, while p 1

	t 0	t 1	t 0			t 1	t 2	t 3		t 0	t 2	t 0 t 1
	2	3			2		3 3 3		2	2	t 1	3 3	2	2
	1	2 3	p 2	p 1	2	3	p 2			p 1	p 2	p
				• ⊆ p 2	• and p 2	• ⊆ p 1	• . Since they have synchronizations, they are not JF. However, the
	fourth net is HJF.
							Weighted Petri nets
					HAC
							OAC
					HFC		OFC			WFC
				CF					FA	HJF	JF
					T			Circuits		P
	Figure

  Figure 3. On the right, the reduced graph represents the net on the left. The node g c represents the subnet c defined by places p 4 , p 5 , p 6 , p 7 , p 8 and transitions t 3 , t 5 , t 6 , t 7 .

							p 8
	t 1	p 1		t 3	p 5		p 6	t 7	g t 1	g p 1	g c
	t 2	p 2	1	t 4	p 4	t 5	p 7	t 6	g t 2 g p 2	g t 4

  Figure 10. Two live and reversible systems. The system on the left is HJF, hence HFC; the one on the right is JF and inhomogeneous. On the left, t 2 and t 3 are enabled; depending on the marking reached, these transitions are either both enabled or both disabled. On the right, due to the inhomogeneity at place p 2 , some reachable markings enable t 2 and do not enable t 3 . In both systems, each reachable marking enables at least one place. On the left, the feasible T-sequence σ r = t 2 t 1 t 3 t 4 t 5 t 2 can be used to reach the initial marking from any reachable marking. For example, after a firing of t 3 on the left, the sequence t 4 t 5 leads to a marking that enables p 2 ; then, the sequence t 2 t 1 t 2 leads to the initial marking. Here, the whole sequence fired from the initial marking, namely t 3 t 4 t 5 t 2 t 1 t 2 , forms another T-sequence. On the right, the same feasible T-sequence σ r = t 2 t 1 t 3 t 4 t 5 t 2 is feasible initially. After firing t 3 , the sequence t 4 t 5 enables p 2 and t 2 t 1 t 2 leads to the initial marking. Again, the whole sequence t 3 t 4 t 5 t 2 t 1 t 2 is another feasible T-sequence. In both systems, after the first firing of t 3 , enabling p 2 makes possible the firing of the occurrences of t 2 and t 1 that appear before the first occurrence of t 3 in σ r . Then, the initial marking can easily be reached by firing the occurrences remaining in σ r , i.e. t 2 .

			1			p 3	1		t 4			1			p 3	1		t 4
	t 1	2	1	1 1	t 2	1 1	t 3	1 1	1 2	p 4	t 1	2	p 1	1 1	t 2	1 2	t 3	2	1 3	p 4
			1			p 2	2		t 5			1			p 2	3		t 5

  • t and t are in choice (or structural conflict) relation if and only if t = t or • t ∩ • t = ∅. • t and t are in coupled conflict relation if and only if there exist t 0 . . . t k ∈ T such that t = t 0 , t = t k , and for each i ∈ {1, . . . , k}, t i-1 and t i are in choice relation. It is an equivalence relation on the set of transitions, and each equivalence class is a coupled conflict set. We denote by C its quotient set, i.e. the set of coupled conflict sets. Theorem 6.9. Let S be a strongly connected, well-formed JF system. Then S is T-decomposable, being covered by the set of its T-components, which are well-formed and strongly connected FA T-subsystems. Let us write S = (N, M 0 ). By Theorem 20 in [14], since N = (P, T, W ) is well-formed, it is conservative. Denoting by rank(N ) the rank of the incidence matrix of N , we deduce from conservativeness that rank(N ) < |P | (where |P | denotes the number of places). In the strongly connected JF class, |P | equals the number of coupled conflict sets |C | of N , i.e. the number of post-sets of places in this case.

	Proof:

Thus, rank(N ) < |C | and Theorem 20 of

[START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF]

applies, hence N is T-allocatable

9

. Moreover, each JF net is also a weighted FC net (also known as a TEFC net

[START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF]

), meaning that Theorem 24 of

[START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF]

applies: S is T-decomposable, i.e. covered by T-components, which are well-formed and strongly connected CF T-subsystems (by definition), hence FA T-subsystems since S is JF.

In this paper, we study siphons that may contain traps, remarkably in JF nets. Hence, we cannot use the results of[START_REF] Barkaoui | On liveness and controlled siphons in Petri nets[END_REF]. Also, our nets will often be structurally repetitive (weakly sur-consistent), which is another well-known necessary condition of structural liveness (Prop. 10 in[START_REF] Silva | Linear algebraic and linear programming techniques for the analysis of place/transition net systems[END_REF]) that is not sufficient in the HJF class.

meaning that the subnet is different from the net considered.

Each of them has traps and is weakly sur-consistent (i.e. structurally repetitive).

In our examples, the properties of liveness and reversibility can be checked with the Tina Toolbox (http://projects.laas. fr/tina/)

Note that if p2 • contained more than two transitions, we could have various delays for several output transitions.

For the sake of brevity, the theory of allocations is not recalled here, since all details can be found in[START_REF] Teruel | Structure theory of Equal Conflict systems[END_REF].

A path is elementary if it does not contain the same node twice, apart from the first and last node if the path forms a cycle.

Proof:

Let H = {p|{t} = p • } and K = {p|{t} ⊂ p • }. H and K may not be simultaneously empty, since otherwise • t = H ∪ K = ∅ and t is live, whatever the initial marking. Let K = {p 1 , p 2 , . . . , p m }. If it is non-empty, since N is AC, we may assume without loss of generality that {t} ⊂ p • 1 ⊆ p • 2 ⊆ . . . ⊆ p • m . Since t is not live, there is a reachable marking M 1 such that t is dead (no marking reachable from M 1 enables t). From M 1 , the marking of H may only increase. If there is a place p in H such that M 1 (p) < W (p, t) and • p ⊆ {t} we are done since p • = {t}. Otherwise, for each place p ∈ H (if any), either for every marking M reachable from M 1 , M (p) ≥ W (p, t), or there is a transition t p = t in • p; since all those t p 's are live, there is a marking M 2 ∈ [M 1 such that M 2 (p) ≥ W (p, t) for each p ∈ H. If K = ∅, t is enabled at M 2 , contradicting our hypotheses. Otherwise, let v ∈ p • 1 \ {t}; since v is live, there is a marking M 3 ∈ [M 2 enabling v. Then, suppose that M 3 does not enable t. Thus, there exists a place p in K whose output set contains t and another transition u = v but does not contain v, such that M 3 (p ) < W (p , t). By definition of p 1 , p 1

• ⊆ p • and p • contains v, a contradiction with the definition of p . Thus, since the net is homogeneous, M 3 also enables t, contradicting again our hypotheses. Hence there is a place p ∈ H satisfying our claim.

Then, all the properties relying on this lemma in [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF] remain true for non-pure nets.

Correction of an erroneous argument in a previous proof for HAC nets

Consider the next characterization of [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF] for the m-live+bounded markings of HAC nets, where N D denotes the P-subnet of N induced by the set D of places and M D 0 is the restriction M 0 D .

Theorem 4.2. (Theorem 5.2 in [START_REF] Jiao | On liveness and boundedness of Asymmetric Choice nets[END_REF]) An HAC system (N, M 0 ) is monotonically live and bounded if and only if every place p is covered by a minimal siphon, and for every minimal siphon D, (N D , M D 0 ) is live and bounded.

Let us exhibit the problem that appears in the proof of this theorem. The paper correctly shows the "if" part, i.e. that the liveness and boundedness of all the P-subsystems induced by all the minimal siphons, which cover all places, implies the monotonic liveness and boundedness of the entire HAC system. It also proves that if (N, M 0 ) is live and bounded, then every place is covered by a minimal siphon, and that if N is live from each marking M ≥ M 0 then (N D , M D 0 ) is live for every minimal siphon D. However, to show that the existence of a minimal siphon D such that (N D , M D 0 ) is live and unbounded implies that (N, M 0 ) is not monotonically bounded, the authors use the next argument:

This argument is incorrect, since it considers that ∃p ∈ S, ∀k ∈ N, ∃M ≥ M 0 , ∃M ∈ [M : M (p) > k instead of the desired goal, which is: ∃p ∈ S, ∃M ≥ M 0 , ∀k ∈ N, ∃M ∈ [M : M (p) > k. Actually, the authors do not use there the fact that D is a minimal siphon. However, we are going to show that the authors had a correct intuition and the property they claim is valid. Other properties of the literature for HAC nets, like [START_REF] Barkaoui | On liveness and controlled siphons in Petri nets[END_REF][START_REF] Barkaoui | On the Equivalence Between Liveness and Deadlock-Freeness in Petri Nets[END_REF], do not help. sequence of σ preceding the n-th occurrence of t i in σ, thus containing n -1 occurrences of t i , is denoted by

The next transition function tnext: Consider some place p and sequences σ, κ such that Ψ(σ) Ψ(κ). Assume there exists a transition t in p • for which

)-th occurrence is the first to appear in κ, is returned by a function, called the next transition function and denoted by tnext(p • , σ, κ).

In Figure 10, consider the sequences

Local ordering: Let T be a subset of transitions. The local ordering of T induced by σ is the sequence σ ∞ T (obtained by projection).

In Figure 10, in any of the two systems, consider the set p 2 • = {t 2 , t 3 } and the feasible T-sequence σ r = t 2 t 1 t 3 t 4 t 5 t 2 . The local ordering associated to p 2

• is defined by σ 2 = (t 2 t 3 t 2 ) ∞ , which is the projection of σ ∞ r on the post-set p 2 • . Note that this is not an order in the usual sense, but it specifies in which ordering (i.e. sequence) the transitions should be considered.

Delayed occurrences: Consider a subset T ⊆ T of transitions and a transition t ∈ T . Denote by τ = σ ∞ T the local ordering of T induced by σ. An occurrence of t is delayed by the firing of a sequence α relatively to τ if there exists t ∈ T , t = t, such that, noting n = Ψ(α)(t ) and K = K n t (τ ), we have Ψ(α)(t) < Ψ(K)(t). In other words, an occurrence of the transition t is delayed by α relatively to the local ordering τ if t occurred (strictly) fewer times in α than in the largest finite prefix sequence K of τ preceding the n-th occurrence of t in τ . Intuitively, when t is fired the same number of times in α as in a prefix of τ , while t is fired fewer times in α than in the same prefix, t is said to be delayed.

In Figure 10, in any of the two systems, consider the feasible T-sequence σ r = t 2 t 1 t 3 t 4 t 5 t 2 , the set p 2 • = {t 2 , t 3 } and the associated local ordering τ 2 = (t 2 t 3 t 2 ) ∞ . If the sequence α = t 3 is fired first, then the local ordering defined by τ 2 is broken and one occurrence of t 2 is delayed 8

). Consequently, after the initial firing of α = t 3 , if one aims at removing the delay(s) as soon as possible, possibly by following the local orderings in others places first, the next transition to be fired in

In the sequel, every local ordering will correspond to the post-set of some place.

A sufficient condition of reversibility for live JF nets inspired from the HFC case

As explained earlier, the existence of a feasible T-sequence is necessary to fulfill both liveness and reversibility, but is not sufficient for reversibility in the JF class, even under the assumptions of liveness, structural boundedness and strong connectedness.

In this subsection, we obtain the next general sufficient condition of reversibility for live JF nets, embodied by Corollary 6.6: in a strongly connected JF system, if some T-sequence is feasible and each Algorithm 1: From the feasible T-sequence σ r and the transition t, with t ∈ p • , construction of a sequence σ t that fires the occurrences of p • delayed by t relatively to σ ∞ r p • by following the local orderings induced by σ r in other enabled places.

Data: The T-sequence σ r , which is feasible in S; the system (N, M t ) obtained by firing t in S; the input place p of t. Result: A sequence σ t feasible in (N, M t ) that fires the delayed occurrences of κ 0 = K 1 t (σ r ).

, the outer loop stops and no delayed occurrence remains.

The termination and validity of this algorithm are shown in Lemma 6.3 below, which is a variant of Lemma 2 in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF] for JF nets. Notice that the assumption of liveness of this previous result is replaced by strong connectedness and the fact that every reachable marking enables at least one place, implying liveness in the JF case [START_REF] Delosme | Polynomial Sufficient Conditions of Well-Behavedness for Weighted Join-Free and Choice-Free Systems[END_REF][START_REF] Hujsa | Polynomial Sufficient Conditions of Well-Behavedness and Home Markings in Subclasses of Weighted Petri nets[END_REF]. With these new assumptions, we do not need here the notion of fairness exploited in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF], as detailed in the following proof. Lemma 6.3. (Termination and validity of Algorithm 1) Let (N, M 0 ) be a strongly connected JF system in which a T-sequence σ r is feasible and each reachable marking enables at least one place. Then, for every transition t enabled by M 0 , with M 0 t -→ M t , Algorithm 1 terminates and computes a sequence σ t feasible at M t such that t σ t does not induce any delayed occurrence relatively to the local orderings based on σ r and on each post-set of each place.

Proof:

Comparing with the proof of Lemma 2 in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF], we replace the equal-conflict set E t with p • and have to handle the new assumptions.

Since the net is strongly connected, no place has an empty post-set.

Let us show that the inner loop always terminates and enables p. Since every reachable marking enables some place, firings can always occur. Now suppose that the inner loop does not terminate: an infinite feasible sequence α is fired that never enables p. Here, we do not need the notion of fairness used in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF] to obtain a contradiction. In [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF], the firings follow a fair ordering (meaning informally that each transition that is infinitely often enabled is fired an infinite number of times) induced by σ ∞ r . Combined with the fact that the loop does not terminate and that the system is live, this implies that each transition of the system is fired an infinite number of times in the HFC case.

In our JF case, if a transition is fired an infinite number of times, its input place is enabled infinitely many times too. Since the firing policy follows the local orderings induced by σ ∞ r for enabled places, and since the support of σ r is T , it also fires an infinite number of times each transition of the post-sets visited. Fairness is thus implicit in this process. Now, denote by Q the set of places whose post-set is fired an infinite number of times in α. The place p does not belong to Q since it is never enabled. By strong connectedness, there exists some directed path µ of the form p 0 t 0 p 1 . . . p such that p 0 is the only place of µ belonging to Q (It may be the case that p = p 1 ). Since p 0 belongs to Q, α fires t 0 an infinite number of times, implying that p 1 becomes enabled within a finite number of steps. Consequently, every transition of p 1

• is fired an infinite number of times, and p 1 must belong to Q, a contradiction.

We deduce that p becomes enabled within a finite number of steps and the inner loop terminates. The rest of the proof is directly deduced from [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF].

Before studying Algorithm 2, we give in Lemma 6.4 a property of the sequence α = t σ t obtained at the end of Algorithm 1. This result, derived from Lemma 3 in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF], compares the number of occurrences in α with other ones in prefixes of κ, and will prove useful for the study of Algorithm 2. Lemma 6.4. (Property of α = t σ t ) Let S = (N, M 0 ) be a strongly connected JF system in which a T-sequence σ r is feasible and each reachable marking enables at least one place. Consider the sequence σ t constructed by Algorithm 1 after the firing of any transition t in S. Consider the sequences α = t σ t and κ = σ r where ≥ 1 is the smallest integer such that Ψ(α) ≤ • Ψ(σ r ). Then, for each place p 0 , for every transition t ∈ p 0

• , for each transition t u such that t u = tnext(p 0

• , α, κ) is defined, with m = Ψ(α)(t u ) + 1 and K u = K m u (κ), we have that Ψ(α)(t ) = Ψ(K u )(t ). Besides, for every other place p 0 , for each transition t ∈ p 0

• , we have that Ψ(α)(t ) = Ψ(κ)(t ).

Proof: By Lemma 6.3, Algorithm 1 terminates and is correct. Consequently, at the end, there is no delayed occurrence of any transition in the system obtained. The equalities are then deduced as in the proof of Lemma 3 in [START_REF] Hujsa | On the Reversibility of Live Equal-Conflict Petri Nets[END_REF] by replacing E t with p • and E with p 0

• for some place p 0 .