Kamel Barkaoui
email: kamel.barkaoui@cnam.fr

Hanifa Boucheneb
email: hanifa.boucheneb@polymtl.ca

Zhiwu Li

Exploiting local persistency for reduced state space generation

Keywords: Petri nets, reachability analysis, state explosion problem, persistent sets, partial order techniques, step graphs

This paper deals with the partial order techniques of Petri nets, based on persistent sets and step graphs methods. To take advantage of the strengths of each method, it proposes the persistent step sets as a parametric combination of the both methods. The persistent step sets method allows to fix, for each marking, the set of transitions S to be covered by the selected steps and then to control their maximal length and number. Depending on the parameter S, it computes covering-steps, persistent sets, persistent-step sets or other kinds of combination of both methods. Moreover, this persistent step selective search preserves, at least, deadlocks of Petri nets.

Furthermore, this paper provides two practical computation procedures of the persistent step sets based on the strong-persistent sets and the weak-persistent sets, respectively. Finally, to achieve further reductions, it shows how to weaken the sufficient conditions used in the literature to build persistent sets.

Introduction

The state explosion problem is the main obstacle for the verification of concurrent systems, as they are generally based on an interleaving semantics, where all possible firing orders of concurrent actions are exhaustively explored. Different techniques for fighting this problem have been proposed such as structural analysis, symmetries and partial orders.

The structural analysis attempts to find a relationship between the behaviour of the net and its structure, where the initial marking is considered as a parameter. The net structure can be studied through its associated incidence matrix and the corresponding net state equation leading mainly to the concept of place invariants [START_REF] Desel | what is a petri net?[END_REF]. It can also be studied through topological properties of the interplay between conflict and synchronisation of remarkable substructures of the net such siphons and traps. In both cases, the aim of these studies is to highlight necessary and/or sufficient structural conditions to check general behavioural properties such as liveness [START_REF] Chen | New Petri net structure and its application to optimal supervisory control: Interval inhibitor arcs[END_REF][START_REF] Li | On controllability of dependent siphons for deadlock prevention in generalized petri nets[END_REF], for large subclasses of place/transition nets [START_REF] Kamel Barkaoui | On the equivalence between liveness and deadlock-freeness in petri nets[END_REF][START_REF] Barkaoui | On liveness and controlled siphons in petri nets[END_REF].

The second well-accepted technique to tackle combinatorial explosion in modelchecking consists in exploiting symmetries over states and the transition relation [START_REF] Junttila | On the symmetry reduction method for petri nets and similar formalisms[END_REF] to build a quotient graph of equivalence classes of states, that may be exponentially smaller than the full state graph, while preserving many behavioural properties of interest.

The partial order techniques have been proven to be the most successful in practice. We distinguish two classes of partial order techniques: partial order reduction techniques [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem[END_REF][START_REF] Peled | All from one, one for all: on model checking using representatives[END_REF][START_REF] Peled | Stutter-invariant temporal properties are expressible without the next-time operator[END_REF][START_REF] Valmari | A stubborn attack on state explosion[END_REF][START_REF] Valmari | The state explosion problem[END_REF][START_REF] Valmari | Can stubborn sets be optimal?[END_REF] and step graph techniques [START_REF] Franc ¸ois Vernadat | Covering step graph[END_REF]. Partial order reduction techniques, such as the ample sets [START_REF] Peled | All from one, one for all: on model checking using representatives[END_REF][START_REF] Peled | Stutter-invariant temporal properties are expressible without the next-time operator[END_REF], the stubborn sets [START_REF] Valmari | A stubborn attack on state explosion[END_REF][START_REF] Valmari | The state explosion problem[END_REF][START_REF] Valmari | Can stubborn sets be optimal?[END_REF] and the persistent sets [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem[END_REF], deal with the state explosion problem by avoiding as much as possible to explore firing sequences that are equivalent w.r.t. the properties of interest (deadlock freeness, deadlocks, reachability, liveness, or linear properties) 1 . The step graph methods explore all the transitions of the state space but some of them are fired together in atomic steps. They aim to reduce the depth of the marking graph while the purpose of the partial order reduction techniques is to reduce its breadth.

The common characteristics of all these methods is to reduce the state space to be explored, by selecting the actions or sets of actions (steps) to be executed from each state. The selection procedure of actions or steps relies on the notion of independent actions. Two actions are said to be independent, if whenever they are enabled, they can be fired in both orders and the firing of one of them does not inhibit the occurrence of the other. Moreover, their firing in both orders leads to the same state. Both of these conditions constitute the well known diamond property.

Each of the partial order reduction methods above provides sufficient conditions that ensure, at least, preservation of deadlocks markings (i.e., markings with no enabled transitions). Thus, the set ST of the selected transitions or steps is only empty for the deadlock markings. The other sufficient conditions are generally based on the structure of the model, the property to be verified and the current marking. Their aim is to ensure independency between transitions of ST and the others. Indeed, for the ample sets method [START_REF] Peled | All from one, one for all: on model checking using representatives[END_REF][START_REF] Peled | Stutter-invariant temporal properties are expressible without the next-time operator[END_REF], there is no transition outside ST that is firable before all transitions of ST and, at the same time, is dependent of at least a transition of ST . For the stubborn sets method [START_REF] Valmari | A stubborn attack on state explosion[END_REF][START_REF] Valmari | The state explosion problem[END_REF][START_REF] Valmari | Can stubborn sets be optimal?[END_REF], ST contains at least an enabled transition that cannot be disabled by the transitions outside ST and each of its transitions t is independent of all transitions outside ST that are firable before t. The persistent sets method [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem[END_REF] is a particular case of the stubborn sets method, where all transitions of ST are enabled.

For the covering-steps graph method [START_REF] Franc ¸ois Vernadat | Covering step graph[END_REF], the set of steps to be fired from each marking must cover the set of enabled transitions. To achieve more reductions, in [START_REF] Ribet | On combining the persistent sets method with the covering steps graph method[END_REF], the authors have combined this technique with the persistent sets method. This combination consists to firstly compute a persistent set for the current marking and then look for firing steps within this persistent set. For these approaches, the transitions within the same step are neither in weak-conflict 2 nor in structural conflict with the partially enabled transitions.

This paper deals with the persistent sets and the step graph methods. To take advantage of the strengths of each method, it investigates their combination and proposes persistent-step sets method. Persistent step sets method is a parametric combination of persistent sets with step graphs that allows to fix, for each marking, the set of transitions S to be covered by the selected steps and then to control their maximal length and number. Depending on the parameter S, it computes covering-steps [START_REF] Franc ¸ois Vernadat | Covering step graph[END_REF], persistent sets [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem[END_REF], persistent step sets [START_REF] Ribet | On combining the persistent sets method with the covering steps graph method[END_REF] or other combinations of both methods. Furthermore, this paper establishes weaker sufficient conditions to build persistent sets.

The rest of the paper is organised as follows. Section 2 fixes some classical definitions and notations used throughout the paper. Section 3 presents the strong-persistent sets [START_REF] Ribet | On combining the persistent sets method with the covering steps graph method[END_REF][START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem[END_REF], the weak-persistent sets (a weaker version of the strong-persistent sets) and the step graph methods, while pointing out their weaknesses. Section 4 provides a formal definition of persistent step sets and proves that they yield graphs preserving deadlocks of Petri nets. Section 5 establishes two parametric computation procedures of persistent step sets (Algorithm 1 and Algorithm 2) that are based on strong-persistent sets and weak-persistent sets, respectively. Section 6 presents some experimental results of Algorithm 1 and its comparison with the tool TINA 3 . Section 7 shows how to weaken the sufficient conditions used to build strong persistent sets, while preserving deadlocks of Petri nets. It also reports some results of experimental comparison of the algorithms proposed in this paper. Conclusions are presented in Section 8.

Preliminaries

Let P be a nonempty set. A multi-set over P is a function M : P -→ N, N being the set of natural numbers, defined also by the linear combination over P :

p∈P M (p) × p.
We denote by P MS and 0 the set of all multi-sets over P and the empty multi-set, respectively. Operations on multi-sets are defined as usual. Notice that any subset X ⊆ P can be defined as a multi-set over P : X = p∈X 1 × p.

For X ∈ 2 T and Y ⊆ T , we define the operator ⊗ by:

X ⊗ Y = {x ∪ {y} | x ∈ X ∧ y ∈ Y } and ⊗Y = ∅ ⊗ Y = {{y} |y ∈ Y }.
An ordinary Petri net (PN in short) is a tuple P N = (P, T, pre, post) where:

-P and T are finite and nonempty sets of places and transitions with P ∩ T = ∅, -pre and post are the backward and forward incidence functions over the set of transitions T (pre, post : T -→ 2 P ).

For t ∈ T, pre(t) and post(t) are the sets of input and output places of t, denoted also by • t and t • , respectively. Similarly, the sets of input and output transitions of a place p ∈ P are defined by

• p = {t ∈ T | p ∈ t • } and p • = {t ∈ T | p ∈ • t}, respectively.
Two transitions t and t ′ are in structural conflict, denoted by

t ⊥ t ′ iff pre(t) ∩ pre(t ′ ) = ∅. We denote by CF S(t) = {t ′ ∈ T |t ⊥ t ′ } = ( • t)
• the set of transitions in structural conflict with t. They are in structural weak-conflict iff t ⊥ * t ′ , where ⊥ * is the transitive closure of ⊥. We denote by CF S * (t) = {t ′ ∈ T |t ⊥ * t ′ } the set of transitions in structural weak-conflict with t. Notice that t ∈ CF S(t) and CF S(t) ⊆ CF S * (t).

A marking of an ordinary Petri net indicates the distribution of tokens over its places. It is defined as a multi-set over places. A marked PN is a pair N = (P N, M 0 ), where PN is an ordinary Petri net and M 0 ∈ P MS is its initial marking. Starting from its initial marking, PN evolves by firing enabled transitions. For the following, we fix a marked PN N , a marking M ∈ P MS and a transition t ∈ T of N .

The transition t is enabled at M , denoted by M [t iff all the required tokens for firing t are present in M , i.e., M ≥ pre(t). The transition t is partially enabled in M iff t is not enabled in M and, at least, one of its input places is marked. In case t is enabled at M , its firing leads to the marking M ′ = Mpre(t) + post(t). The notation M [t M ′ means that t is enabled at M and M ′ is the marking reached from M by t. We denote by En(M ) the set of transitions enabled at M , i.e., En(M ) = {t ∈ T | M ≥ pre(t)}. The marking M is a deadlock iff En(M ) = ∅.

For any subset X ⊆ T of transitions. We denote by Ω(X) the sets of all finite and infinite sequences of transitions over X including the empty sequence ǫ. A sequence ω ∈ Ω(X) is elementary if the occurrence of each transition in the sequence does not exceed 1. For any non-empty sequence of transitions ω = t 1 t 2 ...t n ∈ Ω(T ) -{ǫ}, the usual notation M [t 1 t 2 ...t n means that there exist markings M 1 , ..., M n such that

M 1 = M and M i [t i M i+1 , for i ∈ [1, n-1] and M n [t n .
The sequence ω is said to be a firing sequence of M . The notation M [t 1 t 2 ...t n M ′ gives, in addition, the marking reached by the sequence. The marking M ′ is said to be reachable from M by ω. By convention, we have M [ǫ M . We denote by -→ M the set of markings reachable from

M , i.e., -→ M = {M ′ ∈ P MS |∃ω ∈ Ω(T ), M [ω M ′ }. A firing sequence ω of M is maximal if either it
is infinite or it is finite and ends with a deadlock marking. Two sequences of transitions ω and ω ′ are equivalent, denoted by ω ≡ ω ′ iff they are identical or each one can be obtained from the other by a series of permutations of transitions.

If ω ≡ ω ′ then ∀M ′ , M ′′ ∈ P MS , (M [ω M ′ ∧ M [ω ′ M ′′ ) ⇒ M ′ = M ′′
. We denote by [ω] the set of transitions in ω. The firing sequences of N are the firing sequences of its initial marking.

The different possible evolutions of N are represented in a marking graph M G defined by the structure M G = ( -→ M 0 , [ , M 0 ). Let n be a natural number. The marked PN N is n-bounded iff for every reachable marking of M 0 , the number of tokens in each place does not exceed n. It is safe iff it is 1-bounded. It is bounded iff it is k-bounded for some natural number k.

A firing step τ of N is a non-empty subset of transitions (τ ⊆ T ) fired simultaneously and atomically from a marking of N . From an interleaving semantic point of view, it represents an abstraction of all firing orders of its transitions. For instance, τ = {t 1 , t

and ∀t ′ ∈ En(M ) -τ, M ≥ pre(t ′ ) + t∈τ pre(t). A step graph of N is a structure SG = (M M, R, M 0 ), where M M ⊆ -→ M 0 is a subset of reachable markings, M 0 is the initial marking and R ⊆ M M × 2 T × M M is the relation defined by (M, τ, M ′ ) ∈ R ⇒ M [τ M ′ .
For the rest of paper, we fix an ordinary Petri net N = (P, T, pre, post, M 0 ).

3 Persistent sets and step graphs

Strong-persistent sets

Let M be a marking. Informally, a persistent set of M is a subset µ of enabled transitions such that no transition of µ can be disabled, as long as no transition of µ is fired [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem[END_REF][START_REF] Ribet | On combining the persistent sets method with the covering steps graph method[END_REF]. A persistent graph is obtained by recursively firing from each marking a persistent set. Persistent graphs preserve deadlocks of Petri nets [START_REF] Ribet | On combining the persistent sets method with the covering steps graph method[END_REF]. However, this strong definition of persistent sets can be weakened while preserving deadlocks of Petri nets. The idea comes from the stubborn sets [START_REF] Valmari | Can stubborn sets be optimal?[END_REF]. But unlike the stubborn sets, all the transitions inside a persistent set are enabled. To distinguish between the two definitions of persistent sets, the persistent sets of [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem[END_REF][START_REF] Ribet | On combining the persistent sets method with the covering steps graph method[END_REF] are referred as strong-persistent sets. The others are referred as weak-persistent sets.

Definition 1 Let M be a marking and µ ⊆ En(M ) a subset of enabled transitions. Formally, the subset µ is a strong-persistent set of M , if all the following conditions are satisfied:

-D0 : En(M ) = ∅ ⇔ µ = ∅. -D1 : ∀t ∈ µ, ∀ω ∈ Ω(T -µ), M [ω ⇒ M [ωt . -D2 : ∀t ∈ µ, ∀ω ∈ Ω(T -µ), M [ωt ⇒ M [tω .
The subset µ is a weak-persistent set of M , if it satisfies all the following conditions:

-D0: En(M ) = ∅ ⇔ µ = ∅. -D1w: ∃t ∈ µ, ∀ω ∈ Ω(T -µ), M [ω ⇒ M [ωt . -D2: ∀t ∈ µ, ∀ω ∈ Ω(T -µ), M [ωt ⇒ M [tω .
Intuitively, Condition D0 ensures that a strong/weak-persistent set of M is empty only if M is a deadlock. Conditions D1w means that there is at least a transition inside µ that is maintained enabled as long as no transition of µ is fired. Conditions D1 states that all transitions of µ are maintained enabled as long as no transition of µ is fired. Condition D2 means that if some sequence ω with no transition from µ is firable before any transition t of µ, then it is also firable after t.

The transitions of µ that satisfy D1w are called the key-transitions of µ [START_REF] Valmari | Can stubborn sets be optimal?[END_REF]. Note that the strong-persistent sets contains only key-transitions. A strong/weak-persistent selective search from M 04 preserves all deadlock markings of Petri nets [START_REF] Valmari | Stubborn set intuition explained[END_REF] (written, abusively, the strong/weak-persistent sets preserve deadlocks).

In the following, we investigate the combination of the strong/weak-persistent sets with the step graphs.

Step graphs

The aim of the step graph methods is to represent by a single path a largest possible set of equivalent maximal firing sequences of the model, by choosing appropriately, from each marking, the transitions to be fired together in steps. All transitions of the equivalent sequences are represented in the path but the concurrent ones are grouped together in steps.

Step graphs allow to reduce the path depths of the marking graph. However, in case there are several sets of transitions that are independent from each other, the number of steps and their lengths may be very large. For example, consider the model PN1 at Fig. 1. Its marking graph consists of 27 nodes and 54 arcs. Its initial marking M 0 has 3 strong-persistent sets that are independent from each other: {t 1 , t 2 }, {t 3 , t 4 } and {t 5 , t 6 }. A strong-persistent graph of PN1 is shown in Fig. 3. Note that there are different strong-persistent graphs but they have all the same size (2 4 -1 = 15 nodes and 15 -1 = 14 arcs). Using the 3 independent strongpersistent sets of M 0 , steps can be built by picking a transition from each strongpersistent set. Its step graph is shown in Fig. 2 and consists of 9 = 2 3 +1 nodes, 8 = 2 3 arcs and 2 3 maximal steps. It is a covering-steps graph, as the set of steps selected from each marking covers all its enabled transitions. But, the number of successors of the initial marking exceeds the number of enabled transitions and is exponential with the number of independent strong-persistent sets. Even if the covering-steps graph is smaller than the persistent graph, the number of maximal steps and their lengths may be very large, which limits the usefulness of the step graph method.

To take advantage of the strengths of each method, the persistent sets and step graphs are combined in [START_REF] Ribet | On combining the persistent sets method with the covering steps graph method[END_REF]. The idea is to compute a strong-persistent set and then determine the transitions within this set to be fired together in steps. As an example, for the strong-persistent set {t 1 , t 2 , t 3 , t 4 } of the initial marking M 0 , we can build 4 steps: {t 1 , t 3 }, {t 1 , t 4 }, {t 2 , t 3 } and {t 2 , t 4 }. The resulting reduced graph is reported in Fig. 4 and consists of 13 nodes and 12 arcs. This combination allows to control the number and the length of the steps to be considered from each marking, while yielding a graph that is larger than the step graph but smaller than the persistent graph.

Persistent step sets

We first define the notion of persistent step sets. Then, we show that the resulting graphs preserve deadlock markings of Petri nets.

Definition 2 Let M be a marking and µ i ⊆ T , for some n > 0 and i ∈ [1, n], n subsets of enabled transitions pairwise disjunct, i.e.,

µ i ∩ µ j = ∅ for i = j ∈ [1, n]. Let µ = i∈[1,n] µ i and SS = (⊗µ 1 ) ⊗ ... ⊗ µ n .
The set SS is a strong-persistent step set if it satisfies all the following conditions:

-DS0: En(M ) = ∅ ⇔ µ = ∅. -DS1: ∀i ∈ [1, n], ∀t ∈ µ i , ∀ω ∈ Ω(T -µ i ), M [ω ⇒ M [ωt . -DS2: ∀i ∈ [1, n], ∀t ∈ µ i , ∀ω ∈ Ω(T -µ i ), M [ωt ⇒ M [tω .
Similarly, the set SS is a weak-persistent step set if it satisfies all the following conditions:

-DS0: En(M ) = ∅ ⇔ µ = ∅. -DSw1: ∀i ∈ [1, n], ∃t ∈ µ i , ∀ω ∈ Ω(T -µ i ), M [ω ⇒ M [ωt . -DS2: ∀i ∈ [1, n], ∀t ∈ µ i , ∀ω ∈ Ω(T -µ i ), M [ωt ⇒ M [tω .
In other words, SS is a sort of cartesian product of pairwise disjunct strong/weakpersistent sets. Note that if SS = ⊗{t 1 , ..., t n } = {{t 1 }, ..., {t n }} is a strong/weakpersistent step set then µ = {t 1 , ..., t n } is a strong/weak-persistent set.

Example 1 Consider the model PN1 at Fig. 1. Proof As a strong-persistent set is a weak-persistent set, we provide the proof for weak-persistent sets.

-The set µ = {t 1 , t 2 , t 3 } is a weak-persistent
It is obvious that all deadlocks reachable by the weak-persistent step selective search from M 0 are also reachable in the Petri net. Let M be a marking reached in a weak-persistent step selective search from M ∈ SS then, by DSw1, D is not a deadlock marking as there is, at least, a transition from µ that is firable after t, which is in contradiction with the fact that D is a deadlock. Suppose that Theorem 1 holds for any marking M ′ (reachable in the weak-persistent step set selective search) and D is reachable from M ′ by a sequence ω ′ such that |ω ′ | < |ω|.

-If there is no step of SS (scattered or not) in ω (i.e., ω is free from all transitions of some µ i ), then, by DSw1, there is, at least, a missed transition of a step that is firable after ω. It means that D has, at least, a successor, which is in contradiction with the fact that D is a deadlock. -If there is, at least a step τ of SS, scattered or not, in ω, then, by DS2 the transitions of this step can be shifted to the front to constitute a step firable from M , as the sets µ i for i ∈ [1, n] are pairwise disjunct. Firing this step from M leads to some marking M ′ that is reachable by the weak-persistent step selective search. Moreover, D is reachable from M ′ , in the Petri net, by some sequence ω ′ s.t. |ω ′ | < |ω|. Therefore, D is reachable by the weak-persistent step selective search from M 0 . ⊓ ⊔

Parametric combination of persistent sets with step graphs

We propose, in the following, two parametric selection algorithms of persistent step sets, based on strong-persistent sets and weak-persistent sets, respectively. For a given marking M and a subset S of transitions enabled in M (S ⊆ En(M )), the idea is to compute a persistent step set that covers, at least, the transitions of S. Unlike, the approach proposed in [START_REF] Ribet | On combining the persistent sets method with the covering steps graph method[END_REF], the set S is not necessarily a strong-persistent set. As we will show, according to the parameter S, the provided persistent step set is either a strong/weak-persistent set, a covering-step set or a set of steps that covers partially the enabled transitions in M . We suppose available two procedures SP S and W P S that compute a strong-persistent set and a weak-persistent set, respectively, tor a given marking M and a transition t enabled in M .

Computing strong-persistent step sets

A computation procedure of strong-persistent step sets is provided in Algorithm 1. For a given marking M and a set of enabled transitions S ⊆ En(M ), Algorithm 1 returns a set of steps firable from M . The parameter S allows to specify the set of enabled transitions that must be, at least, covered by the set of steps.

The computed set of steps is a sort of product of some disjoint strong-persistent sets. The first term of the product is R = SP S(t, M ), where t is chosen randomly in S ′ (a copy of S). Afterwards, the transitions of R are deleted from S ′ to ensure that the next terms are disjoints from those computed so far. If the resulting set S ′ is not empty, then the same process is repeated to compute the next term of the product, and so on. Theorem 2 establishes that the returned set of steps is a strong-persistent step set. Choose t ∈ S ′ ; 6:

R := SP S(t, M ); 7:

S ′ := S ′ -R; 8:

SS := SS ⊗ R; 9: end while 10: return SS;

11: [For X ∈ 2 T and Y ⊆ T , X ⊗ Y = {x ∪ {y} | x ∈ X ∧ y ∈ Y } and ∅ ⊗ Y = {{y} |y ∈ Y }]
Example 2 Consider the initial marking M 0 of the model PN1 at Fig. 1.

-For S = {t 1 , t 2 , t 3 }, Algorithm 1 computes SS as follows. It starts by setting SS and S ′ to ∅ and {t 1 , t 2 , t 3 }, respectively. If t 1 of S ′ is the first transition selected in the loop while, then R = SP S(t

1 , M 0 ) = {t 1 , t 2 }, S ′ = S ′ -R = {t 3 } and SS = ∅ ⊗ R = {{t 1 }, {t 2 }}.
For the second iteration, t 3 is selected then

R = SP S(t 3 , M 0 ) = {t 3 , t 4 }, S ′ = S ′ -R = ∅ and SS = SS ⊗ {t 3 , t 4 } = {{t 1 , t 3 },
) = SP S(t 2 , M 0 ) = S). If t 1 (or t 2 ) is selected first then R = SP S(t 1 , M 0 ) = {t 1 , t 2 }, S ′ = S ′ -R = ∅ and SS = {{t 1 }, {t 2 }}.
Theorem 2 Algorithm 1 returns a set of steps that satisfies both DS1 and DS2 of the strong-persistent step sets.

Proof Suppose that n (n > 0) iterations are needed to complete the loop while of Algorithm 1. During the i th iteration (for i ∈ [1, n]), a transition t (i) is selected from S ′(i) and R (i) = SP S(t (i) , M ). The set R (i) is a strong-persistent set, which means that all its transitions are keys. Therefore, it holds that:

∀i ∈ [1, n], ∀t (i) ∈ R (i) , ∀ω ∈ Ω(T -R (i) ), M [ω ⇒ M [ωt (i) ∧ M [t (i) ω . Consequently, SS satisfies DS1 and DS2. ⊓ ⊔

Computing weak-persistent step sets

To achieve further reductions, Algorithm 2 computes, in SS, a product of some pairwise disjunct weak-persistent sets, instead of strong-persistent sets. Unlike disjunct strong-persistent sets, the product of disjunct weak-persistent sets may contain some non enabled steps. These steps are deleted from SS to keep only the enabled ones. According to Theorem 3, SS is a weak-persistent step set.

Algorithm 2 Weak-persistent-step set of a marking M covering the transitions of S Example 3 Consider the model PN2 at Fig. 5 and its initial marking M 0 . For S = {t 0 , t 1 , t 2 , t 3 }, Algorithm 2 first sets SS, S ′ and R ′ to ∅, {t 0 , t 1 , t 2 , t 3 } and ∅, respectively. Then, if t 0 of S ′ is the first transition selected in the loop while on S ′ , then R = W P S(t 0 , M 0 ) = {t 0 , t 1 },

S ′ := S ′ -R; 8: R ′ := R ′ ∪ R; 9: SS := SS ⊗ R; 10: end while 11: return SS ∩ EnS(M ); 12: [For X ∈ 2 T and Y ⊆ T , X ⊗ Y = {x ∪ {y} | x ∈ X ∧ y ∈ Y } and ∅ ⊗ Y = {{y} |y ∈ Y }]
M0 M5 M1 M2 M3 M4 M10 M11 M18 M15 M6 M7 M8 M9 M5 M6 M8 M14 M19 M12 M12 M13 M12 M13 M12 M13 M12 M12 M13 M12 M12 M17 M16 t3 t2
S ′ = S ′ -R = {t 2 , t 3 }, SS = ∅ ⊗ R = {{t 0 }, {t 1 }} and R ′ = R ′ ∪ {t 0 , t 1 }.
For the second iteration, t 3 is selected, as:

W P S(t 2 , M 0 ) ∩ R ′ = {t 1 } and W P S(t 3 , M 0 ) ∩ R ′ = ∅. Therefore, R = W P S(t 3 , M 0 ) = {t 2 , t 3 }, S ′ = S ′ -R = ∅ and SS = SS ⊗ {t 2 , t 3 } = {{t 0 , t 2 }, {t 0 , t 3 }, {t 1 , t 2 }, {t 1 , t 3 }}.
Finally, Algorithm 2 returns SS ∩ EnS(M 0 ), i.e., {{t 0 , t 2 }, {t 0 , t 3 }, {t 1 , t 3 }}. The step {t 1 , t 2 } is eliminated as it is not enabled in M 0 .

Theorem 3 Algorithm 2 returns a set of steps that satisfies conditions DSw1 and DS2 of the weak-persistent sets.

Proof SS is a product of some pairwise disjunct persistent sets.

Suppose that SS = R (1) ⊗ R (2) .... ⊗ R (n) with (n > 0). Example 4 For the model PN2 at Fig. 5, the graphs depicted at Fig. 6 and Fig. 7 are obtained using the step selection Algorithm 2 and the tool TINA, respectively for the case where all the enabled transitions are covered from each marking. The graph at Fig. 6 is a covering-steps graph obtained by recursively applying Algorithm 2 to the initial marking and each new computed marking. The step selective algorithms are always invoked for a marking M and S = En(M ).

Then, (i) ∀i ∈ [1, n], ∃t (i) ∈ R (i) , ∀ω ∈ Ω(T -R (i) ), M [ω ⇒ M [ωt (i) and (ii) ∀i ∈ [1, n], ∀t (i) ∈ R (i) , ∀ω ∈ Ω(T -R (i) ), M [ωt (i) ⇒ M [t (i) ω . Condition (i) is
Let us apply, Algorithm 1 to the initial marking M 0 for S = En(M 0 ). It starts by SS = ∅, S ′ = S = {t 0 , t 1 , t 2 , t 3 }. If t 0 of S ′ is the first transition selected in the loop while on S ′ , then R is set to SP S(t 0 , M 0 ) = {t 0 , t 1 , t 2 , t 3 } and S ′ to ∅. Then, Algorithm 1 returns SS = ∅ ⊗ R = {{t 0 }, {t 1 }, {t 2 }, {t 3 }}.

Note that for M 0 and S = En(M 0 ), Algorithm 2 returns the covering-step set SS = {{t 0 , t 2 }, {t 0 , t 3 }, {t 1 , t 3 }} (see Example 3).

In this section, two parametric algorithms are presented for computing strong/weakpersistent step sets. They allow to specify, for each marking M , the subset S of enabled transitions to be covered by the set of steps. For S = En(M ), all the enabled transitions are covered by the provided steps, as for the covering-steps graphs. For S = SP S(t, M ), the realised combination corresponds to the one proposed in [START_REF] Ribet | On combining the persistent sets method with the covering steps graph method[END_REF] for building persistent step graphs. In case the parameter S is a singleton then Algorithm 1 (resp. Algorithm 2) provides a set of singletons whose union is a strong (resp. weak) persistent set. Therefore, these algorithms allows to compute not only persistent step sets but also strong/weak-persistent sets.

Another feature of these algorithms is the possibility to control the number of steps by fixing the dimension of the cartesian product of the strong/weak-persistent sets. Indeed, the loops while in algorithms 1 and 2 can be, in addition, constrained by a given number of iterations or an appropriate number of steps. It is also possible to restrict the Cartesian product of strong/weak-persistent sets to singletons, except for one of them. More precisely, Line 9 of Algorithm 2 (Line 8 of Algorithm 1) is replaced with: if(SS = ∅∨|R| = 1) then SS := SS ⊗R. This modification allows to limit the number of steps and, at the same time, the redundancy of transitions between steps. These variants of algorithms 1 and 2 provide persistent step sets.

Experimental results

We have implemented and tested algorithms 1 and 2 on several ordinary Petri Nets and models derived from Petri nets at Fig. 5, Fig. 8 and Fig. 9.

The model n P N 2 is a simple parallel composition of n instances of the model P N 2 at Fig. 5. The model n P N 3(k) is a parallel composition of n instances of P N 3(k) at Fig. 8, where the place p 2 of the i th instance of P N 3(k) is merged with the place p 1 of the (i+1) th instance, for i ∈ [1, n-1]. Finally, the model n P N 4(k) is a parallel composition of n instances of P N 4(k) at Fig. 9, where the place p 31 of the i th instance of P N 4 is merged with the place p 11 of the (i + 1) th instance, for i ∈ [1, n -1]. The last two models are Petri net representations of two flexible manufacturing systems. The first one is either free from deadlocks or not, depending on parameter k. The second one is free from deadlocks.

For these tests, the strong-persistent is computed using algorithms 3. This algorithm is based on the stubborn sets method [START_REF] Valmari | Stubborn set intuition explained[END_REF]. Given a marking M and an enabled transition t, it starts by setting S to the singleton {t}. For each enabled transition t ′ within S, it adds to S the transitions in structural conflict with t ′ . For each non enabled transition t ′ within S, Algorithm 3 adds to S the input transitions of all the non marked input places of t ′ . This step ensures that, at the end of the process, for each non enabled transition t ′ in S, there is in S at least an enabled transition that must be fired before t ′ . This process is repeated until reaching a fixed point. Finally, the non enabled transitions are eliminated to obtain a strong-persistent set that satisfies conditions D0, D1 and D2 [START_REF] Valmari | Stubborn set intuition explained[END_REF].

Table 1 is devoted to the comparison of the covering-steps and persistent set methods. It reports the sizes of the marking graph (MG), the covering-steps graphs (CSG, SCSG), the persistent graphs (PG, SPG) and the persistent step graph (PSG) for the three models described above. The CSG is the covering-steps graph provided by the tool TINA. The SCSG is the covering-steps graph computed using algorithms 1 and 3 6 , for the case where all the enabled transitions are covered from each marking (i.e., S = En(M )). The PG is the persistent graph provided by the tool TINA. The SPG is the persistent graph computed using algorithms 1 and 3 for the case where S is a Algorithm 3 SP S(t, M ) : A strong-persistent set of the marking M containing, at least, the transition t 1: Input : A marking M and a transition t enabled in M ; 2: Output : A strong-persistent set S of M for t; 3: S = {t}; 4: repeat 5:

S ′ := S; 6:

for (t ′ ∈ S) do 7: if (t ′ / ∈ En(M )) then 8: S := S ∪ {p ∈ • t ′ | p ∈ • t ′ ∧ M (p) = 0}; 9:
else 10:

S := S ∪ CF S(t ′ ); 11:

end if 12:

end for 13: until (S = S ′ ) 14: S := S ∩ En(M ); 15: return S; singleton. The PSG combines the persistent sets with the step graph methods and is provided by the tool TINA. The last column reports the number of deadlock markings. For all tested models, the SCSG and SPG provide better results than the CSG, PG and PSG generated by the tool TINA. This improvement increases with the size of the models. Furthermore, the persistent sets methods outperform the coveringsteps methods for the tested models. However, their combination outperforms the both methods. To achieve further reductions, the next section presents an algorithm for computing the weak-persistent sets to be used by Algorithm 2.

Towards weaker persistent sets

To our knowledge, in almost all partial order approaches, if an enabled transition is selected then all the enabled transitions in weak-conflict are selected too. In the following, we show how to weaken the selection procedure to handle, in a better way, the weak-conflicts for a subclass of ordinary Petri nets. This subclass excludes all impure ordinary Petri nets 7 . It is known that each impure Petri net can be transformed into a pure Petri net with the same behaviour, by adding appropriate dummy places and transitions [START_REF] David | Du grafcet aux réseaux de Petri[END_REF]. Another restriction is to keep only pure ordinary Petri nets such that if a transition is enabled in some marking then, at most, one instance of each transition contributes to this enabledness. A structural sufficient condition for this property can be stated as: two or more input places (p 1 , p 2 , ...) of the same transition t cannot be reached from two or more output transitions (t 1 , t 2 , ...) of the same place p. If this property is not satisfied for some transition t and place p then all tokens that reach p could be transferred to the same input place of t leading to a dead transition or an unbounded place. Petri nets that do not satisfy this property are considered as not well-handled8 in [START_REF] Van Der Aalst | Finding errors in the design of a workflow process : a petri-net-based approach[END_REF]. In this paper, we call the subclass of Petri nets that satisfy this property as well-handled Petri nets. Given a marking M and an enabled transition t in M , in Algorithm 3, t is first selected and if an enabled transition t ′ is selected then all the enabled transitions in weak-conflict with t ′ are selected too. We propose in Algorithm 4 to limit this selection to transitions in conflict t ′ that are not enabled in M or their firing may disable t ′ and enable it again later. Theorem 4 shows with this restrictive selection the returned set S satisfies both conditions Dw1 and D2 of the weak-persistent sets. To preserve all deadlocks of Petri nets, it suffices to ensure that Condition D0 is also satisfied. Condition D0 is satisfied if Algorithm 4 is called for each non deadlock marking reachable from the initial marking M 0 , by the persistent set selective search.

For example, for the model P N 4 at Fig. 9 and its initial marking M 0 , no matter which transition is selected first, Algorithm 3 will select all the enabled transitions in M 0 . For M 0 and transition t 11 , Algorithm 4 will select the transitions t 11 and t 21 . Indeed, at Line 3, S is set to CF S(t 11 ) = {t 11 , t 21 }. For t 11 , the loop f or will not add any transition to S, as all transitions of CF S(t 11 ) are already in S and enabled. For t 21 , the transition t 24 is the only transition, outside S, in structural conflict with t 21 . This transition is enabled in M 0 and connected to t 21 by a path but its firing does not disable t 21 . Thus, it is not selected. Suppose that t 21 is disabled later by another occurrence of t 24 and enabled again after some non-empty firing sequence (as the model is a pure Petri net). The transitions that contribute to its new enabledness constitute an elementary sequence ω (as the model is a well-handled Petri net). Therefore, at most one instance of t 24 contributes to the new enabledness of t 21 . The sequence t 24 ω can be fired before other instances of t 24 to prevent the disabledness of t 21 . This results in an equivalent sequence that maintains t 21 enabled until its firing. This is the intuitive idea behind Algorithm 3. The resulting persistent graph is shown in Fig. 10 Theorem 4 Algorithm 4 returns a set that satisfies both conditions D1w and D2 of the weak-persistent sets for the well-handled Petri nets. Proof According to Line 3, the set S returned by Algorithm 4 contains CF S(t) ∩ En(M ). Lines 7 -8 inside the two loops (repeat and f or) ensure that S includes all transitions of En(M ) that could enable directly or indirectly any transition of CF S(t) -En(M ). Therefore, S satisfies conditions D1w and D2 of the weak-persistent sets for t. Indeed, the transitions outside S cannot enable any transition in conflict with t as long as no transition from S is fired. Let us show that S satisfies D2, i.e., ∀t

S := S ∪ { • p | p ∈ • t ′ ∧ M (p) = 0}; 9: else 10: for (u ∈ CF S(t ′ )) do 11: if (u / ∈ En(M ) ∨ (π(u, t ′ ) ∧ ∃p ∈ • t ′ ∩ • u, v∈p • ∩En(M ) pre(v)(p) > M (p)))
′ ∈ S, ∀ω ∈ Ω(T -S), M [ωt ′ ⇒ M [t ′ ω . 1-If t ′ is not disabled during the firing of ω then M [ωt ′ ⇒ M [t ′ ω .
2-Otherwise, t ′ is disabled by some transition u and enabled again later. Let ω 1 uω 2 t ′ ω 3 ≡ ω be a sequence equivalent to ω such that only the transitions which have a role in the disabledness or in the enabledness of t ′ are kept in ω 1 uω 2 . If u ∈ CF S(t ′ ) -En(M ) then Algorithm 4 ensures to keep in S all the enabled transitions that could enable any transition in conflict with t ′ . It means that there is in ω 1 at least a transition from S, which is in contradiction with ω 1 ∈ Ω(T -S). Consequently, all transitions in ω in conflict with t ′ are enabled in M . Let us now consider two cases: 2.1-If each transition of (CF S(t ′ ) ∩ En(M )) -S appears at most one time in the sequence ω 1 u then by Algorithm 4, u cannot disable t ′ . Indeed, Algorithm 4 ensures that firing one instance of each enabled transition in conflict with t ′ before t ′ will not disable t ′ . 2.2-If there is in the sequence ω 1 u at least a transition v from CF S(t ′ ) ∩ En(M ) that appears two or more times then the other instances of v in ω 1 are not needed to enable again t ′ but needed to empty some input places of t ′ . Indeed, for the subclass of Petri nets considered in this section, at most one instance of each transition is needed to be fired before the enabledness of a transition. In the worst case, at most one instance of each transition in ω 1 u contributes with those of ω 2 to enable t ′ . Thus these extra instances can be shifted to be fired after t ′ . In the resulting sequence ω ′ 1 uω 2 t ′ ω ′ 3 , the sequence ω 2 does not disable t ′ if t ′ is not disabled by ω ′ 1 u. This is the case because, each transition of CF S(t ′ ) ∩ En(M ) appears at most one time in the sequence ω ′ 1 u and by 2.1, firing all transitions of CF S(t ′ ) ∩ En(M ) will not disable t ′ . Therefore, S satisfies D2. To sum up S satisfies D1w and D2 for the well-handled Petri nets.

⊓ ⊔

The comparison results of algorithms 3, 4 and the persistent graph of the tool TINA are reported in Table 2. As expected, for models with weak-conflicts, Algorithm 4 outperforms the others. For the model n P N 4(5), the weak-persistent graph generated by Algorithm 4 has the same very small size, independently of the number of instances n of P N 4(5). Thus, it is not exaggerated to say that the weak-persistent sets methods are very promising to fight the state explosion and to address the verification of very large asynchronous concurrent systems, where the interplay between concurrency and weak-conflict is expanded. Table 3 shows the comparison results of the PSG of the tool TINA with the one provided using algorithms 2 and 4. The column V W P SG is a variant of the W P SG for the case where Line 9 of Algorithm 2 is replaced with: if(SS = ∅ ∨ |R| = 1) then SS := SS ⊗ R. The obtained results show that the possibility to control the size and number of steps may be very useful to achieve further reductions.

Conclusion

In this work, we have proposed a new parametric combination of the persistent sets with step graphs, based on a better understanding of the intricacy of the relations between concurrency and conflict, revealing local persistency and leading to a significant reduction. We have also shown how to weaken the sufficient conditions used to build persistent sets. The proposed approach takes into account, in a finer way, the structure of the net, while preserving deadlocks of Petri Nets. Indeed, unlike the method in [START_REF] Franc ¸ois Vernadat | Covering step graph[END_REF], persistent steps may contain some transitions that are in weak-Finally, the performed tests show the effectiveness of the proposed approach in terms of state space reduction, relatively to the covering-steps and strong-persistent sets methods or their combination implemented in the tool TINA. They also suggest that combining appropriately step graphs with any partial order technique is of very great interest for model-checking.

Fig. 2 A

 2 Fig. 1 Model PN1

Fig. 3 AFig. 4 A

 34 Fig. 3 A persistent set graph of PN1

  0 5 and D a deadlock marking reachable from M in the Petri net. Let us show that D is also reached by the weak-persistent step selective search from M 0 . The marking M is reachable in the Petri net. Let ω be a firing sequence leading to the marking D from M in the Petri net. The proof is by induction on the length of ω. a) If ω = ǫ then M = D. b) If ω = t and {t} ∈ SS then D is reached by the persistent step selective search. c) If ω = t and {t} /

Algorithm 1

 1 Strong-persistent step set of a marking M covering the transitions of S 1: Input : A marking M and a subset S of enabled transitions such that S = ∅; 2: Output : A strong-persistent step set SS of M w.r.t. S; 3: SS := ∅; S ′ := S; 4: while (S ′ = ∅) do 5:

Fig. 6

 6 Fig. 5 Model PN2

Fig. 7

 7 Fig. 7 SCSG: Covering-steps graph of PN2 (using the tool TINA)

Fig. 8

 8 Fig.8Model PN3(k): A flexible manufacturing system (with deadlocks) taken from[START_REF] Chen | Optimal Supervisory Control of Flexible Manufacturing Systems[END_REF]

Fig. 9

 9 Fig. 9 Model P N 4(k): A flexible manufacturing system (free from deadlocks)

Fig. 10 A

 10 Fig.10A weak-persistent graph of P N 4[START_REF] David | Du grafcet aux réseaux de Petri[END_REF]

  2 , t 3 } represents the following six sequences: t 1 t 2 t 3 , t 1 t 3 t 2 , t 2 t 1 t 3 , t 2 t 3 t 1 , t 3 t 1 t 2 and t 3 t 2 t 1 . The intermediate markings are abstracted to keep only the markings before and after the firing step. Let M ∈ P MS be a marking and τ ⊆ T a firing step of N . The firing step τ is enabled in M , denoted by M [τ iff M ≥ The notation M [τ M ′ means that τ is enabled at M and M ′ is the marking reached from M by τ . We denote by EnS(M ) the set of all enabled steps in M , i.e., EnS(M ) = {τ ⊆ T | M ≥

	pre(t), which means that there are enough tokens to fire concurrently all
	t∈τ
	the transitions within the step. If τ is enabled in M , its firing leads to the marking
	M ′ = M +	t∈τ	(post(t) -pre(t)). t∈τ	pre(t)}. The firing step τ
	is maximal in M iff it is maximal for the inclusion in EnS(M ), i.e., M ≥	pre(t)
				t∈τ

  set but not a strong-persistent set of the initial marking M 0 = p 1 + p 2 + p 3 , as it satisfies D0, D1w and D2 but it does not satisfy D1. There are two key-transitions in µ: t 1 and t 2 . -The step set SS = (⊗{t 1 , t 2 }) ⊗ {t 3 } = {{t 1 , t 3 }, {t 2 , t 3 }} is not a persistent step set of M 0 , as it does not satisfy Condition DS1 for {t 3 }. Indeed, t 4 ∈ Ω(T -{t 3 }), we have M 0 [t 4 t 1 and ¬M 0 [t 4 t 1 t 3 } .

Theorem 1 Strong/weak persistent step sets preserve deadlocks of the Petri net.

  {t 1 , t 4 }, {t 2 , t 3 }, {t 2 , t 4 }}. Algorithm 1 returns SS. -For M 0 and S = En(M 0 ), Algorithm 1 returns the set: SS = ({{t 1 }, {t 2 }} ⊗ {{t 3 , t 4 }}) ⊗ {{t 5 , t 6 }}. Indeed, initially, we have S ′ = S = En(M 0 ). The loop while will perform successively the following updates of R, S ′ and SS, for the case where the selected transitions are successively t 1 , t 3 and t 5 : For t 1 : R = {t 1 , t 2 }, S ′ = {t 3 , t 4 , t 5 , t 6 } and SS = {{t 1 }, {t 2 }}. For t 3 : R = {t 3 , t 4 }, S ′ = {t 5 , t 6 } and SS = SS × R. For t 5 : R = {t 5 , t 6 }, S ′ = ∅ and then Then, SS = ({{t 1 }, {t 2 }} ⊗ {t 3 , t 4 }) ⊗ {t 5 , t 6 }. Note that in this case, SS is a covering-step set. -For M 0 and S ′ = S = {t 1 , t 2 }, Algorithm 1 returns SS = {{t 1 }, {t 2 }}, as the transitions of S are all key-transitions (i.e., SP S(t 1 , M 0

Table 1

 1 Experimental results for Algorithm 1 vs TINA

		MG	CSG	SCSG	PG	SPG	PSG	Dead
			TINA	Alg.1&3	TINA	Alg.3	TINA
				S = En(M )		(Alg.1&3
						|S| = 1)
	4 PN2
	Markings	160000	23138	1569	6905	226	6737	16
	Edges	1024000	71801	2848	11048	285	10880
	CPU (s)	2	0.5	0	0	0	0
	5 PN2
	Markings		265640	8833	48361	466	47681	32
	Edges	> 3000000	952997	16576	80488	589	79808
	CPU (s)		3	0	0.3	0	0.3
	6 PN2
	Markings			50817	333417	946	330689	64
	Edges	> 3000000	> 3000000	97408	570792	1197	568064
	CPU (s)			0.4	2.5	0	3.2
	2 PN3 (5 )
	Markings		403998	89714	50196	7853	54709	31
	Edges	> 3000000	2579317	635090	114242	13580	138382
	CPU (s)		12.2	5.5	0.4	0	0.6
	3 PN3 (2 )
	Markings	368905	359824	119605	101486	25775	101482	9
	Edges	2623520	2221255	672509	263007	50509	266696
	CPU (s)	7	9.5	9.3	1	0.3	1.2
	3 PN3 (3 )
	Markings				1051463	115391	1068339	16
	Edges	> 3000000	> 3000000	> 3000000	2676615	220535	2868287
	CPU (s)				13.2	3.2	18
	1 PN4 (5 )
	Markings	1251	1063	76	83	51	83	0
	Edges	6526	3795	272	156	84	156
	CPU (s)	0	0	0	0	0	0
	2 PN4 (5 )
	Markings			5109	3909	837	3909	0
	Edges	> 3000000	> 3000000	32836	8568	1512	8568
	CPU (s)			0	0	0	0
	3 PN4 (5 )
	Markings				143959	10935	143959	0
	Edges	> 3000000	> 3000000	> 3000000	331668	20412	331668
	CPU (s)				1.7	0.4	2.3

  . Note that firing t 11 or t 21 from M 0 will disable neither t 24 nor t 31 . These transitions are maintained enabled as long as the fired transitions are enabled directly/indirectly by t 11 or t 21 . Their firings are postponed indefinitely in favour of t 11 , t 21 and the transitions they will enable directly/indirectly.

	Algorithm 4 W P S(t, M ) : A weak-persistent set of the marking M where t is a
	key-transition
	1: Input : A marking M and a transition t enabled in M ;
	2: Output : A weak-persistent set S of M for t;
	3: S := CF S(t);
	4: repeat
	5:	S ′ := S;
	6:	for (t ′ ∈ S) do
	7:	if (t ′ / ∈ En(M )) then
	8:

  ′ ) is true iff there is a path in the Petri net connecting u to t ′ .]

		then
	12:	S := S ∪ {u};
	13:	end if
	14:	end for
	15:	end if
	16:	end for
	17: until (S = S ′ )
	18: S := S ∩ En(M );
	19: return S;
	20: [π(u, t

Table 2

 2 Experimental results for persistent graphs

		PG	SPG	WPG	Dead
		TINA	Alg.3	Alg.4
			(Alg.1&3	(Alg.2&4
			|S| = 1)	|S| = 1)
	4 PN2
	Markings	6905	226	136	16
	Edges	11048	285	150
	CPU (s)	0	0	0
	5 PN2
	Markings	48361	466	280	32
	Edges	80488	589	310
	CPU (s)	0.3	0	0
	6 PN2
	Markings	333417	946	568	64
	Edges	570792	1197	630
	CPU (s)	2.5	0	0
	2 PN3 (5 )
	Markings	50196	7853	1514	31
	Edges	114242	13580	2353
	CPU (s)	0.4	0	0
	3 PN3 (2 )
	Markings	101486	25775	23409	9
	Edges	263007	50509	42423
	CPU (s)	1	0.3	0.2
	3 PN3 (3 )
	Markings	1051463	115391	95356	16
	Edges	2676615	220535	165027
	CPU (s)	13.2	3.2	0.7
	1 PN4 (5 )
	Markings	83	51	10	0
	Edges	156	84	14
	CPU (s)	0	0	0
	2 PN4 (5 )
	Markings	3909	837	10	0
	Edges	8568	1512	14
	CPU (s)	0	0	0
	3 PN4 (5 )
	Markings	143959	10935	10	0
	Edges	331668	20412	14
	CPU (s)	1.7	0.4	0

Two firing sequences are equivalent w.r.t. some property, if they cannot be distinguished by the property.

The (structural) weak-conflict relation is the transitive closure of the (structural) conflict relation.

http://projects.laas.fr/tina//home.php.

A strong/weak-persistent selective search of the Petri net is a procedure that recursively computes a strong/weak-persistent set and the successor markings reachable by the transitions of this set, for the initial marking and each new computed marking.

A persistent step selective search from M 0 is a procedure that recursively computes a persistent step set and the successor markings reachable by these steps, for the initial marking and each new computed marking.

Algorithm 3 is used for SP S(t, M ).

An impure Petri net is a Petri net with one or more self-loops (i.e., place in the net, which is both an input and output place of the same transition).

A Petri net is well-handled iff, for any pair of nodes x and y such that one of the nodes is a place and the other a transition and for any pair of elementary paths C1 and C2 leading from x to y, nodes(C1) ∩ nodes(C2) = {x, y} ⇒ C1 = C2, where nodes(C) is the set of nodes in the path C[START_REF] Van Der Aalst | Finding errors in the design of a workflow process : a petri-net-based approach[END_REF].

conflict. Moreover, it allows choosing the transitions to be covered while controlling the length and the number of steps to be selected from each marking. It can thus compute persistent graphs, covering steps graphs and graphs generated from different kinds of their combination.