Alain Finkel
email: finkel@lsv.fr

Serge Haddad
email: haddad@lsv.fr

Igor Khmelnitsky
email: khmelnitsky@lsv.fr

Commodification of Accelerations for the Karp and Miller Construction

Keywords: Petri nets, Coverability, Verification tool

Karp and Miller's algorithm is based on an exploration of the reachability tree of a Petri net where, the sequences of transitions with positive incidence are accelerated. The tree nodes of Karp and Miller are labeled with ω-markings representing (potentially infinite) coverability sets. This set of ω-markings allows us to decide several properties of the Petri net, such as whether a marking is coverable or whether the reachability set is finite. The edges of the Karp and Miller tree are labeled by transitions but the associated semantic is unclear which yields to a complex proof of the algorithm correctness. In this work we introduce three concepts: abstraction, acceleration and exploration sequence. In particular, we generalize the definition of transitions to ω-transitions in order to represent accelerations by such transitions. The notion of abstraction makes it possible to greatly simplify the proof of the correctness. On the other hand, for an additional cost in memory, which we theoretically evaluated, we propose an "accelerated" variant of the Karp and Miller algorithm with an expected gain in execution time. Based on a similar idea we have accelerated (and made complete) the minimal coverability graph construction, implemented it in a tool and performed numerous promising benchmarks issued from realistic case studies and from a random generator of Petri nets.

Introduction

Coverability and Karp and Miller's algorithm. The coverability set (also denoted as Cover ) of a Petri net with an initial marking is the downward closure (for the usual order on integer vectors) of the set of reachable markings. An effective finite representation of the cover makes it possible to decide several problems such as: Can a given marking be covered by an reachable marking (the coverability problem)? Is the set of reachable markings finite? Which places are unbounded?

In 1969, Karp and Miller showed that a finite representation of the coverability set of Petri nets and vector addition systems is computable by an algorithm constructing a finite tree (KMT) [START_REF] Karp | Parallel program schemata[END_REF] whose finite set of vertex labels (ω-markings) C represents the cover. Specifically, the downward closure (in N P ) of C, denoted ↓C, coincides with the cover. The set C is not unique because it depends on the order chosen for the exploration of the successors of the tree nodes. Moreover, it is not minimal in the number of elements because it may can contain comparable ω-markings and thus contain redundant items.

The original proof of Karp and Miller's algorithm is incomplete as Hack had already noted in 1974 [START_REF] Hack | Decidability questions for Petri Nets[END_REF]. Moreover the proofs of variants of the Karp and Miller algorithm (see below) are difficult and do not reuse the original proof of Karp and Miller. Motivated by the lack of complete and certified proof, Yamamoto et al wrote a formal COQ proof of the correctness of Karp and Miller's algorithm [START_REF] Yamamoto | Formalization of karp-miller tree construction on petri nets[END_REF].

Clover, the canonical representation of the cover. It is possible to associate with any marked Petri net a finite and canonical representation of the cover. Indeed, any downward closed set in N P is equal to the downward closed set (in N P ) consisting of a finite subset of incomparable ω-markings in N P ω . Thus one can associate with any marked Petri net a unique finite representation of its cover [START_REF] Finkel | The minimal coverability graph for Petri nets[END_REF]. This approach is generalized to monotonic transition systems with a well quasi order (i.e. well-structured systems) [START_REF] Finkel | Reduction and covering of infinite reachability trees[END_REF] and even to monotonic transition systems with an order without infinite antichains [START_REF] Blondin | Well behaved transition systems[END_REF]. This finite representation is called Clover (for Closure of the Cover ) in [START_REF] Finkel | Forward analysis for WSTS, part II: Complete WSTS[END_REF]. This set is minimal, unique, and consists of maximal elements (these elements represent particular downward closed sets, called ideals). The Clover can be computed from C, by keeping only the maximal elements. Once the Clover is obtained, one can answer coverability questions without rerunning the coverability algorithm each time since one only needs to compare the desired marking to be covered with the markings in the Clover, which takes time which is proportional to the size of Clover and no longer necessarily doubly exponential. Clover also makes it possible to answer a wider variety of questions beyond coverability and finiteness problems. Let us illustrate this point with the following question on ω-coverability (which by itself represents an infinity number of coverability questions): Is the marking (n, 2, 5, n) coverable for all n ≥ 0? This property holds if and only if the ω-marking (ω, 2, 5, ω) is smaller than another ω-marking in the clover, which can be tested in time proportional to the size of Clover.

The Clover set thus allows to solve many problems without re-running an algorithm which is doubly exponential. The question which arises is whether one can find an efficient algorithms to compute the Clover of a marked Petri net.

Variants of the Karp and Miller algorithm. In [START_REF] Finkel | The minimal coverability graph for Petri nets[END_REF] the author develops an a modification to the Karp and Miller algorithm where at any time during the execution of the algorithm, the current set of labeled vertices form an antichain (a set of incomparable elements). The algorithm consists of accelerating, like the original algorithm, the current node and then removing all the sub-trees whose marked root is strictly covered by the marking of the current node. Conversely, if the marking of the current node is covered by the marking of an existing node then the exploration from the current node is stopped and it is removed from the tree. Unfortunately this algorithm contains a bug, identified in 2005, and for some executions calculates a strict sub-approximation of Clover [START_REF] Finkel | A counterexample the the minimal coverability tree algorithm[END_REF]. Since 2005, three main algorithms (with variants) have been proposed [START_REF] Geeraerts | On the efficient computation of the minimal coverability set of Petri nets[END_REF][START_REF] Reynier | Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning[END_REF][START_REF] Valmari | Old and new algorithms for minimal coverability sets[END_REF][START_REF] Piipponen | Constructing minimal coverability sets[END_REF] to calculate Clover without completely building the Karp and Miller tree. An empirical evaluation of these three algorithms gave rather good performances on most of the commonly analyzed case studies but no theoretical limit of the additional cost in memory of these algorithms compared to the algorithm developed in [START_REF] Finkel | The minimal coverability graph for Petri nets[END_REF] is known.

Our contribution. First we give a simple and elegant proof of the Karp and Miller algorithm based on three new concepts: abstraction, acceleration and sequence of exploration. In particular we transform the accelerations of the Karp and Miller algorithm to first-class citizens (i.e. commodification of the accelerations) instead of using them implicitly. Then we propose two "accelerated" variants of the Karp and Miller algorithm with an expected gain in execution time. Based on a similar idea we have accelerated (and made complete) the minimal coverability graph construction of Alain Finkel [START_REF] Finkel | The minimal coverability graph for Petri nets[END_REF], implemented it in a tool and performed numerous promising benchmarks issued from realistic case studies and from a random generator of Petri nets.

-An abstraction is an ω-transition (i.e. a generalized transition), where (1) its backward incidence and incidence with respect to a place can be equal to ω (i.e. belonging to N ω ) and ( 2) which has an infinite family of transition sequences "justifying" the introduction of the ω's. We show that their firing from a ωmarking whose associated ideal is included in Cover leads to a ω-marking whose associated ideal is also included in Cover. We then prove that the concatenation of abstractions is still an abstraction. An acceleration is an abstraction whose incidence with respect to each place is either zero or ω. We establish that any abstraction can be transformed into an acceleration by substituting the strictly positive components of the incidence by ω and requiring ω tokens for the strictly negative components of the incidence. -The proof of the Karp and Miller algorithm becomes rather simple, with the addition of ghost variables (i.e. variables without effect on the execution of the algorithm). The proof of the termination is based on the well order of N P ω . The proof of consistency is an almost immediate consequence of the properties of abstractions and accelerations. The proof of completeness is based on the notion of exploration sequences detailed below.

-We then deepen our study of accelerations. The set of accelerations provided with a natural order is a well order, i.e. it can be represented by its finite base of minimal elements. We show that the integer coefficients of the minimum accelerations are bounded by B(e, d), which is polynomial in the size of the incidence matrices e and doubly exponential in the number of places d. We also show how to transform (truncate) any acceleration into an acceleration whose integer coefficients are bounded by B(e, d). We then propose an accelerated version of the algorithm of Karp and Miller with an expected gains in the execution time. The general principle is as follows: when you discover an acceleration, you truncate it and memorize it. Then at each step of the algorithm, the marking of the current node is increased by firing the accelerations that can be fired. Due to the truncation of the accelerations, our accelerated version of the algorithm of Karp and Miller requires a minimal additional cost in memory, compared to the general cost memory of the algorithm of Karp and Miller which is non-primitive recursive. In addition, the proof of the correctness of our accelerated variant is immediately deduced from our original proof. -A second version consists to memorize accelerations and reuse it along the incomplete algorithm of [START_REF] Finkel | The minimal coverability graph for Petri nets[END_REF]. We proved that this version recovers completeness in [START_REF] Finkel | Minimal Coverability Tree Construction Made Complete and Efficient[END_REF]. Here we perform a large empirical study of the efficiency of this approach that we have integrated in our tool MinCov.

Organization. In Section 2 we introduce and study abstractions and accelerations of a Petri net. We then establish the proof of the Karp and Miller algorithm in Section 3. In Section 4 we describe our version of the Karp and Miller algorithm.

In Section 5 we describe and evaluate our accelerated version of the algorithm of [START_REF] Finkel | The minimal coverability graph for Petri nets[END_REF]. Finally we conclude and offer perspectives to our work in Section 6.

2 Covering and Abstractions

Petri nets: reachability and coverability

We define the Petri nets here in a different but equivalent way compared to the usual definition, namely using the backward incidence matrix Pre and the incidence matrix C. The forward incidence matrix is implicitly defined by C + Pre. This choice is justified by the introduction of abstractions in Subsection 2.2.

Definition 1 A Petri net (PN) is a tuple N = P, T, Pre, C where:

-P is a finite set of places; -T is a finite set of transitions with P ∩ T = ∅; -Pre ∈ N P ×T is the backward incidence matrix ; -C ∈ Z P ×T is the incidence matrix for which the following holds: For all p ∈ P and t ∈ T , C(p, t) + Pre(p, t) ≥ 0.

A marked PN (N , m 0 ) is a PN N initialized with a marking m 0 ∈ N P .

The column vector of the matrix Pre (resp. C) indexed by t ∈ T is denoted by Pre(t) (resp. C(t)). A transition t ∈ T is fireable from a marking m ∈ N P if m ≥ Pre(t). When t is fired from a marking m, its firing leads to a marking m def = m + C(t), which is denoted by m t -→ m . We extend the firing rule to a sequence of firings σ ∈ T * recursively according to its length, as follows: The empty sequence ε is always fireable and does not change the marking. The sequence σ = tσ , with t ∈ T and σ ∈ T * is fireable from m if m t -→ m and σ is fireable from m . The firing of σ from m leads to a marking m reached by σ from m . We denote this firing by m σ -→ m .

Definition 2 Let (N , m 0 ) be a marked PN. The reachability set Reach(N , m 0 ) is defined by:

Reach(N , m 0 ) = {m | ∃σ ∈ T * m 0 σ -→ m}
Before introducing the coverability set of a marked PN, we recall some facts and definitions related to ordered sets. Let (X, ≤) be an ordered set, we will just call X an ordered set when the order is implicit. The downward (resp. upward) closure of a set E ⊆ X denoted by ↓ E (resp. ↑ E) is defined by:

↓ E = {x ∈ X | ∃y ∈ E y ≥ x} (resp. ↑ E = {x ∈ X | ∃y ∈ E y ≤ x}) A set E ⊆ X is said to be downward closed (resp. upward closed ) if E =↓ E (resp. E =↑ E).
An antichain E is a set for which : ∀x = y ∈ E ¬(x ≤ y ∨ y ≤ x). X is FAC if all of its antichains are finite. A set E ⊂ X is directed if E is nonempty and for all x, y ∈ E there exists z ∈ E such that x ≤ z and y ≤ z. An ideal is a directed downward closed set. A well known characterization of FAC sets is: a set is FAC if and only if it is equal to a finite union of ideals (one can find a proof of this result in [START_REF] Blondin | Well behaved transition systems[END_REF]). Given a set E ⊆ X, there may exist several finite families of ideals whose union is equal to E. Among all these finite families, one can choose the unique set of maximal ideals (by inclusion): this set is therefore canonically associated with E.

Recall that an ordered set (X, ≤) is well founded if all strictly decreasing sequences are finite and (X, ≤) is well ordered if it is well founded and FAC. Another characterization of well ordered sets is: a set (X, ≤) is well ordered if and only if for all sequences (x n ) n∈N of elements of X, there exists an infinite non decreasing subsequence. Finally recall that (N, ≤) and (N P , ≤) are well ordered.

We are now able to introduce the cover (also called the coverability set) of a net and to study some of its properties.

Definition 3 Let (N , m 0 ) be a marked PN. The coverability set Cover(N , m 0 ) is defined by: Cover(N , m 0 ) =↓ Reach(N , m 0 )
Since the coverability set is downward closed and N P is FAC, it can be expressed as a finite union of ideals. The ideals of N P can be elegantly defined as follows. We first extend the natural numbers and integers: N ω = N ∪ {ω} and Z ω = Z ∪ {ω}.

Then we extend the order relation and the addition operation to Z ω : For all n ∈ Z, ω > n and for all n ∈ Z ω , n + ω = ω + n = ω. N P ω with this extended order is still well ordered and its elements are called ω-markings. There is a one to one correspondence between ideals of N P and ω-markings. Let m ∈ N P ω . Denote by JmK the set:

JmK = {m ∈ N P | m ≤ m}
JmK is an ideal of N P (and any ideal can be represented as such). By the definitions and properties stated above, we are able to formally define the Clover of a Petri net.

Definition 4 Let (N , m 0 ) be a marked PN. Then Clover(N , m 0 ) ⊆ N P ω is the set of maximal ideals such that :

Cover(N , m 0 ) = m∈Clover(N ,m 0 )

JmK

Remark: We can show that the Clover(N , m 0 ) is thus well defined in a unique way and that it is the smallest (in number of elements) finite set among all the

p i p l p bk p m p ba p c t 1 t 2 t 3 t 4 t 5 t 6
Fig. 1 An unbounded Petri net finite sets of ideals whose union is equal to the Cover(N , m 0 ).

In [START_REF] Blondin | Well behaved transition systems[END_REF] one can find a more general definition of a Clover for well structured transition systems. One of the goals of the Karp and Miller algorithm is the computation of Clover(N , m 0 ).

Example 1

The PN in Figure 1 is unbounded. Its Clover is a set of four elements:

{p i , p bk + p m , p l + p m + ωp ba , p l + p bk + ωp ba + ωp c }
For example, the marking p l + p bk + αp ba + βp c is reachable by the sequence t 1 t α+β 5 t β 6 and therefore covered.

Abstractions and Accelerations

In order to introduce abstractions and accelerations, we generalize the transitions to take into account place markings with ω tokens. In order to define abstractions, we define the incidence of a sequence of ωtransitions σ by recurrence over its length. Like previously, we introduce Pre(p, σ)

def = Pre(σ)(p) and C(p, σ) def = C(σ)(p).
The base case corresponds to the definition of an ω-transition. Let σ = tσ , with t an ω-transition and σ a sequence of ωtransitions, then:

-C(σ) = C(t) + C(σ ); -For all p ∈ P -if C(p, t) = ω then Pre(p, σ) = Pre(p, t); -else Pre(p, σ) = max(Pre(p, t), Pre(p, σ ) -C(p, t)).
The sequence σ is fireable from m if and only if m ≥ Pre(σ). In this case,

m σ -→ m + C(σ).
An abstraction of a PN is an ω-transition which concisely reflects the behavior of the net from the point of view of coverability (see Proposition 1). We note that a transition t of a PN is by construction (with σ n = t) an abstraction. Definition 6 Let N = P, T, Pre, C be a PN and a be an ω-transition. a is an abstraction if for all n ≥ 0, there exists σ n ∈ T * such that for all p ∈ P with Pre(p, a) ∈ N:

1. Pre(p, σ n ) ≤ Pre(p, a); 2. if C(p, a) ∈ Z then C(p, σ n ) ≥ C(p, a); 3. if C(p, a) = ω then C(p, σ n ) ≥ n.
The following proposition justifies the interest of abstractions.

Proposition 1 Let (N , m 0 ) be a marked PN, a be an abstraction and m be an ω-marking such that:

JmK ⊆ Cover(N , m 0 ) and m a -→ m . Then Jm K ⊆ Cover(N , m 0 ). Proof Let m * ∈ Jm K. Denote n = max(m * (p) | m (p) = ω) and = max(Pre(p, σ n ), n -C(p, σ n ) | m(p) = ω). Define m ∈ JmK by: -If m(p) < ω then m (p) = m(p); -Otherwise m (p) = .
Let us check that σ n is fireable from m . For any p ∈ P ,

-If m(p) < ω then m (p) = m(p) ≥ Pre(p, a) ≥ Pre(p, σ n ); -Otherwise m (p) = ≥ Pre(p, σ n ). Let us check that m + C(σ n ) ≥ m * . For any p ∈ P , -If m(p) < ω and C(p, a) < ω then m (p) + C(p, σ n ) ≥ m(p) + C(p, a) = m (p) ≥ m * (p); -If m(p) < ω and C(p, a) = ω then m (p) + C(p, σ n ) ≥ C(p, σ n ) ≥ n ≥ m * (p); -If m(p) = ω then m (p) + C(p, σ n ) ≥ n -C(p, σ n ) + C(p, σ n ) = n ≥ m * (p).
A simple way to build new abstractions consists in concatenating them.

Moreover Pre(p, σ ,b ) + C(p, σ ,b ) ≥ C(p, σ ,b ) ≥ ≥ Pre(p, σ n ). Finally C(p, σ ,b ) + C(p, σ n ) ≥ + C(p, σ n ) ≥ n -C(p, σ n ) + C(p, σ n ) ≥ n. • Case Pre(p, b) < ω, C(p
Pre(p, σ ,b σ n ) = max(Pre(p, σ ,b ), Pre(p, σ n ) -C(p, σ ,b )) ≤ max(Pre(p, b), Pre(p, σ ) -C(p, b)) = Pre(p, a)
There are now two sub-cases to be considered.

• C(p, σ ) < ω. So, C(p, a) = C(p, b) + C(p, σ ) and C(p, σ ,b σ n ) = C(p, σ ,b ) + C(p, σ n ) ≥ C(p, b) + C(p, σ ) = C(p, a). • C(p, σ ) = ω. So, C(p, a) = ω and C(p, σ ,b σ n ) = C(p, σ ,b ) + C(p, σ n ) ≥ C(p, b) + n -C(p, b) = n.
Therefore a is an abstraction.

We now introduce the concept underlying the construction of Karp and Miller.

Definition 7 Let N = P, T, Pre, C be a PN. We say that a is an acceleration if a is an abstraction such that C(a) ∈ {0, ω} P .

The following proposition provides a way of obtaining acceleration from any abstraction.

Karp and Miller's algorithm

Algorithm 1 is the Karp-Miller algorithm enlarged with 'ghost' variables (i.e. having no influence on the behavior of the algorithm) Acc and δ which will simplify the proof. Let us briefly describe this algorithm. It maintains a directed tree T r = (V, E, λ, δ) whose vertices (V ) are labeled by an ω-marking (function λ) and the arcs are labeled by a sequence of ω-transitions belonging to T Acc * , the function δ. We extend δ to a mapping from E * → (T Acc * ) * in the usual way. It maintains a subset of the vertices (Front) which are still to be explored. In order to shorten the description of the algorithm, we introduced Anc(u) the set of ancestors of u (excluding u).

As long as Front is not empty, the algorithm chooses a vertex u ∈ Front. Then there are three cases:

-The marking of u is less then or equal to that of an ancestor u : then u is removed from Front and V and the edge entering u is removed. -The marking of u is greater than that of an ancestor u and for at least one place p, λ(u )(p) < λ(u)(p) < ω. For all such places p, we substitute to its marking the value ω. In our version, we also define an ω-transition a by (1) defining it as the sequence of ω-transitions which labels the path from u to u, (2) applying the transformation of Proposition 3, and (3) concatenating it with the sequence labeling the incoming arc of u. -Otherwise the algorithm determine the fireable transitions and fire them to create the children of u which are inserted in Front. The vertex u is removed from Front. In our version, the incoming arc of a new vertex is labeled by the transition that has been fired.

When Front is empty, the algorithm ends. The set Clover(N , m 0 ) corresponds to the maximal ω-markings associated with the vertices V .

Example 2

The Figure 2 illustrates the tree of Karp and Miller corresponding to the PN in Figure 1. Let us describe its construction during the development of the leftmost branch. From the initial marking, one fires t 1 which leads to p l + p bk , incomparable with m 0 . The exploration continues from this marking. The only fireable transition is t 5 whose firing leads to the marking p l + p bk + p ba . An acceleration a 1 is discovered with Pre(a 1 ) = p l and C(a 1 ) = ωp ba . The current marking is then modified accordingly to the firing of a 1 . This vertex is examined again during a subsequent iteration. There is no more acceleration possible. Consequently one continues the exploration: t 5 and t 6 are fireable. The vertex associated with the firing of t 5 has an identical marking: it will therefore be removed. The vertex associated with firing of t 6 gives rise to a new acceleration: a 2 with Pre(a 2 ) = p bk + ωp ba and C(a 2 ) = ωp c + ωp ba . Since from the last marking only t 5 and t 6 are fireable and lead to the same marking, the exploration of the branch is stopped. Note that a 1 is re-discovered twice during the construction. The Cover computed here is represented by a set of 11 nodes and therefore 11 ω-markings. This set of 11 ω-markings is redundant but one can recover Clover by only keeping the 4 maximum elements: {p i , p l + p bk + ωp ba + ωp c , p bk + p m , p l + p m + ωp ba }.

We will now show the correctness of the Karp and Miller algorithm, namely:

-It terminates; -It is consistent: v∈V Jλ(v)K ⊆ Cover(N , m 0 ); -It is complete: Cover(N , m 0 ) ⊆ v∈V Jλ(v)K.
The termination is based on the fact that N P ω is well ordered.

Proposition 4 (termination)

The Algorithm 1 terminates.

Proof By contradiction, suppose the algorithm does not finish. A vertex of the tree can only be chosen in the loop at most |P | + 1 times. In fact, it remains in Front only if it has been accelerated, which implies that the associated marking has, at least, one more component which is equal to ω. Consequently, the algorithm builds a tree whose number of vertices is infinite.

Each vertex has at most |T | children. By application of König's lemma, this tree has an infinite branch. Let m 0 , m 1 , . . . be the markings associated with the vertices of this branch. N P ω is well ordered. We can therefore extract an increasing infinite subsequence m α(0) ≤ m α(1) ≤ • • • . There cannot be an equality between two consecutive vertices because then the second vertex would have been removed. We therefore deduce that an acceleration has been detected between any two consecutive vertices. Thus each marking has, at least, one more component which is equal to ω then its predecessor. Therefore this sequence contains at most |P | + 1 elements which contradicts the hypothesis.

The following lemma illustrates the advantage of the introduction of ghost variables.

Lemma 1 For every edge (u, v) ∈ E, we have λ(u)

δ(u,v) -→ λ(v).

Algorithm 1: The Karp and Miller algorithm

KarpMiller(N , m 0 ) Input: A marked PN (N , m 0 ) Data: V a set of vertices; E ⊆ V × V ; Front ⊆ V ; λ : V → N p ω ; δ : E → T Acc * ; T r = (V, E, λ, δ) a labeled tree; Acc a set of ω-transitions; u, u , u vertices; a an ω-transition with non negative incidence; Output: A labeled tree T r = (V, E, λ, δ)

1 V ← {r}; E ← ∅; Front ← {r}; λ(r) ← m 0 ; Acc ← ∅; 2 while Front = ∅ do 3 Choose u ∈ Front 4 if ∃u ∈ Anc(u) s.t. λ(u ) ≥ λ(u) then 5 Front ← Front \ {u} ; V ← V \ {u} ; E ← E \ V × {u} // λ(u) is covered 6 else if ∃u ∈ Anc(u) s.t. λ(u ) < λ(u) ∧ ∃p λ(u )(p) < λ(u)(p) < ω then
// An acceleration is found between u and its ancestors u Front ← Front \ {u}

19 foreach t ∈ T s.t. λ(u) ≥ Pre(t) do // Adding the children of u 20 u ← NewNode(); V ← V ∪ {u }; Front ← Front ∪ {u }; E ← E ∪ {(u, u )} 21 λ(u ) ← λ(u) + C(t); δ((u, u )) ← t 22 end 23 end 24 end 25 return T r
Proof There are two cases to be considered: • The creation of (u, v). This happens during the construction of the successors of u. Consequently, there exists a transition t ∈ T such that λ(u) t -→ λ(v) and this transition labels the edge (u, v) .

• The modification of λ(v). This happens when the algorithm discovers an acceleration a between an ancestor u of v and v. We denote by m -the marking associated with v before its update and m + the marking associated with v after its update. By induction, the sequence of ω-transitions along the path from u to v is fireable from λ(u ), hence also from m -. This sequence has the same precondition that a has, except possibly on places p where m -(p) = ω. So a is fireable from m -and by construction m -a -→ m + .

The following lemma is based on the preservation of abstractions by concatenation and the construction of accelerations from abstractions.

Lemma 2 Every ω-transition a ∈ Acc is an acceleration.

Proof The proof is done by induction according to the order of insertion in Acc. Let a ∈ Acc be a ω-transition. Let us denote by σ the sequence corresponding to the path in the tree which led to the creation of a. σ is a sequence of abstractions (by the induction hypothesis). From Proposition 2, this is an abstraction. The construction of a from σ corresponds to Proposition 3. a is therefore an acceleration.

The consistency of the algorithm is now a consequence of the previous lemmas.

Proposition 5 (consistency) For all v ∈ V , Jλ(v)K ⊆ Cover(N , m 0 ).
Proof The proof is done by induction on the length of the path from r to u. The marking associated with r is m 0 . Hence Jm 0 K ⊆ Cover(N , m 0 ). Denote by u the parent of v. By the induction hypothesis Jλ(u)K ⊆ Cover(N , m 0 ). By Lemma 1,

λ(u) δ(u,v) -→ λ(v). By Lemma 2, δ(u, v) is a sequence of abstractions. By Proposi- tion 2, δ(u, v) is an abstraction. By Proposition 1, Jλ(v)K ⊆ Cover(N , m 0 ).
In order to ease the proof of completeness, we introduce the notion of sequence of exploration, related to the coverability tree and its construction.

Definition 8 A sequence of transitions m σ

-→ m is a sequence of exploration of T r if there exists v ∈ Front with λ(v) = m and for all markings m visited by the sequence and all v ∈ V \ Front, we have : m ≤ λ(v).

Lemma 3 For all m ∈ Cover(N , m 0 ) at the start of each iteration of the main loop, the following holds:

1. Either there exists v ∈ V \ Front such that m ∈ Jλ(v)K; 2. Or there exists a sequence of exploration m 1 σ -→ m 2 ≥ m.
Proof We establish this result by induction on the number of iterations already performed.

• For all m ∈ Cover(N , m 0 ), there exists a sequence m 0 σ -→ m 2 ≥ m. Initializing V = Front = {r} and λ(r) = m 0 . We get that Assertion 2 holds for the base case. • ∃u ∈ Anc(u) such that λ(u ) ≥ λ(u). This implies that u = w and the sequence of exploration stays valid.

• λ(u) is accelerated. If u = w, the sequence of exploration is still valid. If u = w then, since λ(u) has been increased, σ is fireable from λ(u). Each marking visited is greater than or equal to the corresponding marking of the exploration sequence. So this new sequence is a sequence of exploration that covers m.

• u is removed from Front and its children are computed. There are now two subcases to be considered.

-If for all marking m visited by σ, m ≤ λ(u), the sequence of exploration is still valid.

-Otherwise, consider m the last marking visited such that m ≤ λ(u) and the suffix of the sequence m

σ -→ m 2 . If σ = ε then m ≤ m 2 = m ≤ λ(u). Therefore Assertion 1 holds for m. Otherwise m t -→ m σ -→ m 2 . Since m ≤ λ(u), u has a child v ∈ Front such that λ(u) t -→ λ(v) ≥ m . Therefore, λ(v) σ -→ m * ≥ m
for some m * and considering the choice of m this sequence is a sequence of exploration.

Proposition 6 (completeness) Upon termination of Algorithm 1, Cover(N , m 0 ) ⊆ v∈V Jλ(v)K.

Proof When Algorithm 1 terminates, Front is empty. The completeness is a consequence of Lemma 3.

An improvement of the algorithm

In order to present an improvement of the algorithm, we deepen the study of accelerations. First, we equip the ω-transitions with an order related to their precondition and incidence.

Definition 9 Let P be a set of places and a and a be ω-transitions.

a ≤ a if and only if Pre(a) ≤ Pre(a ) ∧ C(a) ≥ C(a )
In other words , a ≤ a if a is fireable from an ω-marking m, then a is also firable and firing it leads to an ω-marking greater than or equal to the one reached by a .

Proposition 7 Let N be a PN. Then the set of abstractions of N is upward closed. Similarly, the set of accelerations is upward closed in the set of ω-transitions with incidence in {0, ω} P . Proof Let a be an abstraction and a ≥ a be an ω-transition. Let {σ n } n∈N be the family of sequences associated with a. Let n 0 = max(C(p, a ) | C(p, a ) ∈ N) where, by convention, max(∅) = 0. We will show that the family {σ max(n,n 0 ) } n∈N can be associated with a . Pick p such that Pre(p, a ) ∈ N, which implies that Pre(p, a) ∈ N. We get:

-Pre(p, σ max(n,n 0 ) ) ≤ Pre(p, a) ≤ Pre(p, a ) ; -If C(p, a ) ∈ Z and C(p, a) ∈ Z then C(p, σ max(n,n 0 ) ) ≥ C(p, a) ≥ C(p, a ) ; -If C(p, a ) ∈ Z and C(p, a) = ω then C(p, σ max(n,n 0 ) ) ≥ n 0 ≥ C(p, a ) ; -If C(p, a ) = ω then C(p, a) = ω and C(p, σ max(n,n 0 ) ) ≥ n.
The above also applies to accelerations.

Proposition 8 Let N be a PN. Then the set of accelerations of N is well ordered.

Proof The set of accelerations is a subset of N P × {0, ω} P with the order obtained by the Cartesian product of (N, ≤) and ({0, ω}, ≥). These sets are well ordered and since the Cartesian product preserves this property, the proposition follows.

Let us observe that the set of accelerations is not empty since it contains the acceleration a defined by Pre(a) = C(a) = 0 whose associated family {σ n } is defined by: for all n, σ n = ε. Since the set of accelerations is well ordered and upward closed, it is equal to the upper closure of the finite set of minimal accelerations. We now study the maximal size of these minimal accelerations. Given a net, we denote by d = |P | and e = max p,t (max(Pre(p, t), Pre(p, t) + C(p, t)).

We will use the following result by Jérôme Leroux (published on HAL in June 2019) which gives a bound to the length of the shortest transition sequences which connects two mutually reachable markings m 1 and m 2 .

Theorem 1 (Theorem 2, [START_REF] Leroux | Distance between mutually reachable petri net configurations[END_REF]) Let N be a PN, m 1 , m 2 be markings, and σ 1 , σ 2 be sequences such that m 1

σ 1 -→ m 2 σ 2 -→ m 1 . Then there exist σ 1 , σ 2 such that m 1 σ 1 -→ m 2 σ 2
-→ m 1 where:

|σ 1 σ 2 | ≤ ||m 1 -m 2 || ∞ (3de) (d+1) 2d+4
We deduce an upper bound on the size of minimal accelerations. Let v ∈ N P ω . We denote by . Hence a ≤ trunc(a). Since the set of accelerations is upward closed, we deduce that trunc(a) is an acceleration. We are now able to describe the improvement made to the construction of Karp and Miller (see Algorithm 2). First when one discovers an acceleration, one truncates it before inserting it into Acc (line 17). Then, when a vertex of the Front is selected, one first tries to apply the accelerations of Acc to increase its marking (lines 4-6). Example 3 Figure 3 shows the accelerated Karp and Miller tree corresponding to the net of Figure 1. When the vertex obtained by firing t 2 from the initial marking is examined, the algorithm evaluates whether firing a 1 or a 2 (both discovered in the left branch) is possible. The acceleration a 1 is fireable and therefore fired.

||v|| ∞ = max(v(p) | v(p) ∈ N).
if ∃u ∈ Anc(u) s.t. λ(u ) ≥ λ(u) then 8 Front ← Front \ {u} ; V ← V \ {u} ; E ← E \ V × {u} // λ(u) is covered 9 else if ∃u ∈ Anc(u) s.t. λ(u ) < λ(u) ∧ ∃p λ(u )(p) < λ(u)(p) < ω then //
The proof of termination is unchanged while the proofs of consistency and completeness require only very minor modifications to integrate the case of the application of accelerations. The the proof of consistency remains valid since the ω-transition a which is truncated before being added to Acc is still an acceleration due to Proposition 10. For completeness one needs to include in the induction step of the proof of Lemma 3, the case of the algorithm using a previously discovered acceleration.

In practice applying the memorized accelerations decreases the size of tree. Furthermore the cost of memorizing accelerations is largely compensated by this decrease.

From a theoretical point of view, there is at most a doubly exponential number of accelerations each of exponential size: that is to say an additional doubly exponential memory complexity. Recall, that the size of a cover tree is in the worst case non-primitive recursive. Therefore even without decrease of the size of the tree, the increase of memory size is negligible. Moreover if the memory space is a strong constraint then it is enough to keep a subset of the accelerations since the proof of the modified algorithm is valid for any set of accelerations.

An efficient tool for the clover construction

Based on the improvements discussed in the previous section and the algorithm (from now on denoted by AF) from [START_REF] Finkel | The minimal coverability graph for Petri nets[END_REF], we have designed an algorithm for computing the minimal coverability set. The main idea of this improvement consists in avoiding the redundancy between ω-markings created by the Karp and Miller algorithm. Hence the new algorithm refines algorithm 2 by adding the following steps to the main loop after using previous discovered accelerations (Line 6):

1. Cleaning: If there exists a vertex with an ω-marking greater than the one of the current processed vertex, then the current vertex is redundant, the algorithm deletes it and starts an new iteration of the main loop.

2. Pruning: Before computing the successors of the current vertex, the algorithm prunes all the subtrees whose roots have ω-markings smaller than the one of the currently processed vertex.

Observe that the main difference between this algorithm and AF is the reuse of previously discovered acceleration which transforms an incomplete algorithm (see [START_REF] Finkel | A counterexample the the minimal coverability tree algorithm[END_REF]) into a complete one. For further details and the whole proof of the correctness, we refer the reader to [START_REF] Finkel | Minimal Coverability Tree Construction Made Complete and Efficient[END_REF]. This algorithm is implemented in the tool MinCov, a tool designed to efficiently solve the coverability and minimal coverability set problems. MinCov is implemented in Python 3.7 using the Numpy and the Z3-solver libraries, and it is around 2000 lines of code. MinCov imports Petri net in .spec format from Mist1 . MinCov and the benchmarks discussed below can be found here: https: //github.com/IgorKhm/MinCov.

Benchmarks. We split the benchmarks into two sets, a set of benchmarks from the literature, and a set of randomly generated Petri nets. The literature ones were taken from [START_REF] Blondin | The logical view on continuous Petri nets[END_REF][START_REF] Esparza | An smt-based approach to coverability analysis[END_REF] which in turn were gathered from five sources:

• MIST 1 : containing both real and artificial systems (mutual exclusion protocols, communication protocols, . . . ); • BFC2 [START_REF] Kaiser | A widening approach to multithreaded program verification[END_REF]: systems originated from analysis of concurrent C programs; • SOTER3 [START_REF] Emanuele | Automatic verification of Erlang-style concurrency[END_REF]: systems originating from the analysis of Erlang programs in order to test the tool SOTER; • Medical [START_REF] Kloos | Incremental, inductive coverability[END_REF]: systems originating from the analysis of a simple medical messaging system of Vanderbilt University Medical Center; • Bug tracking [START_REF] Kloos | Incremental, inductive coverability[END_REF]: systems originating from the analysis of messages of a bug-tracking system.

The random Petri nets were generated by MinCov with the following properties:

(1) 50 < |P |, |T | < 100, (2) the number of places connected to each transition is bounded by 10, and (3) they are not structurally bounded. We compare MinCov with the tool MP [START_REF] Reynier | Minimal coverability set for Petri nets: Karp and Miller algorithm with pruning[END_REF], the tool VH [START_REF] Valmari | Old and new algorithms for minimal coverability sets[END_REF] and the tool CovProc [START_REF] Geeraerts | On the efficient computation of the minimal coverability set of Petri nets[END_REF]. We have also implemented the (incomplete) minimal coverability tree algorithm AF, in order to measure the additional memory needed for the (complete) tools. Both MP and VH tools were sent to us by the courtesy of the authors. The tool MP has two implementations one in Python and the other in C ++ , for this comparison we took the Python one, in order to compare both tools implemented in the same language. The tool CovProc participates only in the benchmark from the literature, since it is extremely slow, and could not achieve the analysis of most of randomly generated Petri nets in a reasonable time. All the benchmarks were performed on a single computer equipped with Intel i5-8250U CPU with 4 cores, 16 GB of memory and Ubuntu Linux 18.03.

The execution time of the tools was limited to 900 seconds for each Petri net, and the results are summarized in the tables below. Each of these tables contain the following information: The first column (T/O) shows the number of instances on which the tool timed out. The second column (Time) consists of the total time on instances that did not time out plus 900 seconds for any instance that led to a time out. The third column (#Nodes) consists of the sum of peak number of nodes in instances that did not time out on any of the tools (except CovProc which does not provide this number). For MinCov we consider the peak number of nodes plus the number of accelerations. In the benchmarks from the literature we observed that the instances that timed out from MinCov are included in those of AF and MP. However there were instances the timed out on VH but did not time out on MinCov and vice versa. W.r.t. memory requirements AF and MinCov have the least number of nodes. MinCov is the second fastest tool, and compared to VH it is 1.2 times slower on the examples from the literature. A possible explanation would be that VH is implemented in C ++ .

In the random benchmarks we observe the same behavior as in the one from the literature where MinCov is only second time-wise, it is 1.5 times slower then VH, but it is the most efficient memory-wise. Compared to AF the extra memory used by MinCov is negligible: 0.002 times additional nodes in average.

Conclusion

The study of the Karp and Miller algorithm led us to two results. First we have developed a simple and elegant proof of this algorithm based on the new notions of abstraction, acceleration and exploration sequence. Then we designed an accelerated version of this algorithm which memorizes all the accelerations already computed in order to re-apply them systematically.

We have also implemented an accelerated version of the minimal coverability graph construction. We have compared the performance of this algorithm with the main existing algorithms calculating Clover with promising results.

In the future, we will also study the possibility of effectively pre-calculating the set of minimal accelerations or some relevant subset. Finally it would be interesting to introduce and apply the concept of acceleration for the study of other well structured transition systems.

Definition 5

 5 Let P be a set of places. An ω-transition a is defined by: -Pre(a) ∈ N P ω its backward incidence; -C(a) ∈ Z P ω its incidence with Pre(a) + C(a) ≥ 0. For simplicity, we denote Pre(a)(p) (resp. C(a)(p)) by Pre(p, a) (resp. C(p, a)). An ω-transition a is fireable from an ω-marking m ∈ N P ω if m ≥ Pre(a). When a is fired from an ω-marking m, it leads to an ω-marking m def = m + C(a), which we denote m a -→ m . Note that if Pre(p, a) = ω then whatever the the value of C(p, a) is, one has m (p) = ω. So without loss of generality, we suppose that for all ω-transition a, Pre(p, a) = ω implies C(p, a) = ω.

Proposition 2

 2 Let N = P, T, Pre, C be a PN and σ a sequence of abstractions. Then the ω-transition a defined by Pre(a) = Pre(σ) and C(a) = C(σ) is an abstraction. Proof We show this result by recurrence on the length of σ. The base case is immediate. Let σ = bσ and (by the recursion hypothesis) let {σ n } n∈N a family of sequences of transitions associated with σ . Let {σ n,b } n∈N a family of sequences of transitions associated with b. Fix n ∈ N. Denote by n = max(n, max(n -C(p, b) | C(p, b) < ω = C(p, σ ))). Denote = max(Pre(p, σ n ), n -C(p, σ n ) | Pre(p, b) < ω = C(p, b)). Let us show that σ ,b σ n satisfies the conditions of Definition 6. Let p ∈ P , Pre(p, a) < ω if and only if (1) Pre(p, b) < ω and C(p, b) = ω or (2) Pre(p, b) < ω, C(p, b) < ω and Pre(p, σ ) < ω. • Case Pre(p, b) < ω and C(p, b) = ω. Therefore Pre(p, a) = Pre(p, b) and C(p, a) = ω. We thus have Pre(σ ,b ) ≤ Pre(p, b) = Pre(p, a).

  , b) < ω and Pre(p, σ ) < ω. Therefore Pre(p, a) = max(Pre(p, b), Pre(p, σ ) -C(p, b)) and:

Proposition 3

 3 Let N = P, T, Pre, C be a PN and a be an abstraction. Define a an ω-transition by for all p ∈ P -If C(p, a) < 0 then Pre(p, a ) = C(p, a ) = ω; -If C(p, a) = 0 then Pre(p, a ) = Pre(p, a) and C(p, a ) = 0; -If C(p, a) > 0 then Pre(p, a ) = Pre(p, a) and C(p, a ) = ω. Then a is an acceleration. Proof Consider {σ n } n∈N a family associated with the abstraction a. We now show that the family {σ n n } n∈N satisfies the conditions of Definition 6 for a . For all n ∈ N : -Let p ∈ P such that Pre(p, a ) < ω. This implies that C(p, a) ≥ 0 and that Pre(p, a ) = Pre(p, a). Since, C(p, σ n ) ≥ C(p, a) ≥ 0, one has Pre(p, σ n n ) = Pre(p, σ n ) ≤ Pre(p, a) = Pre(p, a ); -Let p ∈ P such that C(p, a ) = 0. We get that 0 = C(p, a) ≤ C(σ n ). Therefore, 0 ≤ nC(σ n ) = C(σ n n ); -Let p ∈ P such that Pre(p, a ) < ω and C(p, a ) = ω. This implies that C(p, a) > 0. So 1 ≤ C(p, a) ≤ C(σ n ). Therefore, n ≤ nC(σ n ) = C(σ n n ).

Fig. 2

 2 Fig. 2 Karp and Miller's tree

7 8 a ← NewAcceleration() 9 foreach p ∈ P do 10 if

 8910 Let γ ∈ E * be the path from u to u in T r λ(u)(p) < λ(u)(p) then λ(u)(p) ← ω 11 if C(p, δ(γ)) < 0 then Pre(p, a) ← ω; C(p, a) ← ω 12 if C(p, δ(γ)) = 0 then Pre(p,a) ← Pre(p, δ(γ)); C(p, a) ← 0 13 if C(p, δ(γ)) > 0 then Pre(p, a) ← Pre(p, δ(γ)); C(p, a) ← ω 14 end 15 Let (u , u) be the incoming arc of u in T r 16 δ((u , u)) ← δ((u , u)) • a; Acc ← Acc ∪ {a} 17 else 18

• 1 σ-→ m 2 ≥

 12 Consider the start of an iteration of the loop. Pick m ∈ Cover(N , m 0 ). If m satisfies Assertion 1, it satisfies it until the termination of the algorithm. Suppose that m satisfies Assertion 2. Let us denote the sequence of exploration m m with w ∈ Front where λ(w) = m 1 . Let us consider the different alternatives.

Proposition 9 1 σ 1 -→ m 2 . 2 σ 2 -→ m 1 . 1 -→ m 2 1 -→ m 2 ≥

 91122211212 Let N be a PN and a be a minimal acceleration. Then ||Pre(a)|| ∞ ≤ e(3de) (d+1) 2d+4 . Proof We consider the net N = P , T , Pre , C obtained from N by removing the set of places {p | Pre(p, a) = ω} and adding the set of transitions T 1 = {t p | p ∈ P } with Pre(t p ) = p and C(t p ) = -p. We denote P 1 = {p | Pre(p, a) < ω = C(p, a)}. Let m 1 the marking obtained by restricting Pre(a) to P and m 2 = m 1 + p∈P 1 p. Observe that d ≤ d and that e = e. Let {σ n } n∈N be the family of sequences associated with a. Consider n * = ||Pre(a)|| ∞ + 1. Then σ n * is fireable in N from m 1 and its firing reaches a marking that covers m 2 . By concatenating transitions of T 1 , we obtain a firing sequence in N such that m By the same process, we obtain a sequence m Applying Theorem 1, there exists a sequence σ 1 with m 1 σ and |σ 1 | ≤ (3de) (d+1) 2d+4 since ||m 1 -m 2 || ∞ = 1. By deleting transitions of T 1 in σ 1 , we obtain a sequence σ 1 ∈ T * with m 1 σ m 2 and |σ 1 | ≤ (3de) (d+1) 2d+4 . The ω-transition a , defined by: -Pre(p, a ) = Pre(p, σ 1 ) for all p ∈ P ; -Pre(p, a ) = ω for all p ∈ P \ P ; and C(a ) = C(a). is an acceleration with associated family {σ 1 n } n∈N . By definition of m 1 , a ≤ a. Since a is minimal, a = a. Since |σ 1 | ≤ (3de) (d+1) 2d+4 , ||Pre(a)|| ∞ = ||Pre(a )|| ∞ ≤ e(3de) (d+1) 2d+4 . Proposition 10 Let N be a PN and a be an acceleration. Then the ω-transition trunc(a) defined by: -C(trunc(a)) = C(a); for all p such that Pre(p, a) = ω, Pre(p, trunc(a)) = min(Pre(p, a), e(3de) (d+1) 2d+4 ); for all p such that Pre(p, a) = ω, Pre(p, trunc(a)) = ω. is an acceleration. Proof Let a ≤ a, be a minimal acceleration. For all p such that Pre(p, a) = ω, Pre(p, a ) ≤ e(3de) (d+1) 2d+4

Algorithm 2 :

 2 An acceleration of the Karp and Miller algorithmKarpMillerImproved(N , m 0 ) Input: A marked PN (N , m 0 ) Data: V set of vertices; E ⊆ V × V ; Front ⊆ V ; λ : V → N p ω ; δ : E → T Acc * ; T r = (V, E, λ,δ) a labeled tree; Acc a set of ω-transitions; u, u , u vertices; a an acceleration;Output: A labeled tree T r = (V, E, λ, δ) 1 V ← {r}; E ← ∅; Front ← {r}; λ(r) ← m 0 ; Acc ← ∅; 2 while F ront = ∅ do3 Choose u ∈ Front and let u be the predecessor of u 4 foreach a ∈ Acc s.t. λ(u) a -→ λ(u) + C(a) > λ(u) do 5 λ(u) ← λ(u) + C(a); δ((u , u)) ← δ((u , u))a 6 end 7

11 a ← NewAcceleration() 12 foreach p ∈ P do 13 if 17 a 20 Front←

 1112131720 An acceleration is found between u and an ancestors of u 10 Let γ ∈ E * The path from u to u in T r C(p, δ(γ)) < 0 then Pre(p, a) ← ω; C(p, a) ← ω 14 if C(p, δ(γ)) = 0 then Pre(p, a) ← Pre(p, δ(γ)); C(p, a) ← 0 15 if C(p, δ(γ)) > 0 then Pre(p, a) ← Pre(p, δ(γ)); C(p, a) ← ω; λ(u)(p) ← ω 16 end ← trunc(a) 18 δ((u , u)) ← δ((u , u)) • a; Acc ← Acc ∪ {a} 19 else Front \ {u} 21 foreach t ∈ T s.t. λ(u) ≥ Pre(t) do // Adding the children of u 22 u ← NewNode(); V ← V ∪ {u }; Front ← Front ∪ {u }; E ← E ∪ {(u, u )} 23 λ(u ) ← λ(u) + C(t); δ((u, u )) ← t 24 end 25 end 26 end 27 return T r

Fig. 3

 3 Fig. 3 An accelerated tree

  i p l + p bk p l + pm p bk + pm p l + pm + ωp ba p l + pc + ωp ba pc + p l p l + pc + ωp ba p l + p bk + ωp ba p l + p bk + ωp ba + ωpc

	t 5 a 1	t 1	t 3 p p bk + pc t 4	t 2	t 4	t 5 a 1
	t 6 a 2			t 5 a 1		t 4

  i p l + p b p l + pm + ωp ba p bk + pm p l + pc + ωp ba p l + p bk + ωp ba p l + p bk + ωp ba + ωpc

	t 5 a 1	t 1	t 3 p p bk + pc t 4	t 2 a 1	t 4
	t 6 a 2

Table 1

 1 Benchmarks for MinCov.

	123 benchmarks from the literature	1078 random benchmarks
		T/O	Time	#Nodes		T/O	Time	#Nodes
	MinCov	16	18127	48218	MinCov	146	159940	1291066
	VH	15	14873	75225	VH	111 110431	2454490
	MP	24	23904	478681	MP	231	260608	31354531
	CovProc 49	47081	N/A	CovProc N/A	N/A	N/A
	AF	19	19223	45660	AF	163	178322	1267076

https://github.com/pierreganty/mist/wiki.

http://www.cprover.org/bfc/.

http://mjolnir.cs.ox.ac.uk/soter/

Acknowledments. The authors would like to thank the reviewers for their careful reading of the article and their constructive comments that help us to improve the quality of our article.