Michael Blondin

Alain Finkel

Christoph Haase

Serge Haddad

Approaching the Coverability Problem Continuously

The coverability problem for Petri nets plays a central role in the verification of concurrent shared-memory programs. However, its high EXPSPACE-complete complexity poses a challenge when encountered in real-world instances. In this paper, we develop a new approach to this problem which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backwardcoverability framework. A cornerstone of our approach is the efficient encoding of a recently developed polynomial-time algorithm for reachability in continuous Petri nets into SMT. We demonstrate the effectiveness of our approach on standard benchmarks from the literature, which shows that our approach decides significantly more instances than any existing tool and is in addition often much faster, in particular on large instances.

Introduction

Counter machines and Petri nets are popular mathematical models for modeling and reasoning about distributed and concurrent systems. They provide a high level of abstraction that allows for employing them in a great variety of application domains, ranging, for instance, from modeling of biological, chemical and business processes to the formal verification of concurrent programs.

Many safety properties of real-world systems reduce to the coverability problem in Petri nets: Given an initial and a target configuration, does there exist a sequence of transitions leading from the initial configuration to a configuration larger than the target configuration? For instance, in an approach pioneered by German and Sistla [START_REF] German | Reasoning about systems with many processes[END_REF] multi-threaded non-recursive finite-state programs with shared variables, which naturally occur in predicate-abstraction-based verification frameworks, are modeled as Petri nets such that every program location corresponds to a place in a Petri net, and the number of tokens of a place indicates how many threads are currently at the corresponding program location. Coverability can then, for instance, be used in order to detect whether a mutual exclusion property could be violated when a potentially unbounded number of threads is executed in parallel. The coverability problem was one of the first decision problems for Petri nets that was shown decidable and EXPSPACEcomplete [START_REF] Karp | Parallel program schemata: A mathematical model for parallel computation[END_REF][START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report[END_REF][START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. Despite this huge worst-case complexity, over the course of the last twenty years, a plethora of tools has emerged that have shown to be able to cope with a large number of real-world instances of coverability problems in a satisfactory manner.

Our contribution. We present a new approach to the coverability problem and its implementation. When run on standard benchmarks that we obtained from the literature, our approach proves more than 91% of safe instances to be safe, most of the time much faster when compared to existing tools, and none of those tools can individually prove more than 84% of safe instances to be safe. We additionally demonstrate that our approach is also competitive when run on unsafe instances. In particular, it decides 142 out of 176 (80%) instances of our benchmark suite, while the best competitor only decides 122 (69%) instances.

Our approach is conceptually extremely simple and exploits recent advances in the theory of Petri nets as well as the power of modern SMT-solvers inside a backward-coverability framework. In [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF], Fraca and Haddad solved longstanding open problems about the complexity of decision problems for so-called continuous Petri nets. This class was introduced by David and Alla [START_REF] David | Continuous Petri nets[END_REF] and allows for transitions to be fired a non-negative real number of times-hence places may contain a non-negative real number of tokens. The contribution of [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF] was to present polynomial-time algorithms that decide all of coverability, reachability and boundedness in this class. A further benefit of [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF] is to show that continuous Petri nets over the reals are equivalent to continuous Petri nets over the rationals, and, moreover, to establish a set of simple sufficient and necessary conditions in order to decide reachability in continuous Petri nets. The first contribution of our paper is to show that these conditions can efficiently be encoded into a sentence of linear size in the existential theory of the non-negative rational numbers with addition and order (FO(Q + , +, >)). This encoding paves the way for deciding coverability in continuous Petri nets inside SMT-solvers and is particularly useful in order to efficiently answer multiple coverability queries on the same continuous Petri net due to caching strategies present in modern SMT-solvers. Moreover, we show that our encoding in effect strictly subsumes a recently introduced CEGAR-based approach to coverability described by Esparza et al. in [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF]; in particular we can completely avoid the potentially exponentially long CEGAR-loop, cf. the related work section below. The benefit of coverability in continuous Petri nets is that it provides a way to over-approximate coverability under the standard semantics: any configuration that is not coverable in a continuous Petri net is also not coverable under the standard semantics. This observation can be exploited inside a backward-coverability framework as follows. Starting at the target configuration to be covered, the classical backward-coverability algorithm [START_REF] Parosh | Algorithmic analysis of programs with well quasi-ordered domains[END_REF] repeatedly computes the set of all minimal predecessor configurations that by application of one transition cover the target or some earlier computed configuration until a fixed point is reached, which is guaranteed to happen due to Petri nets being well-structured transition systems [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. The crux to the performance of the algorithm lies in the size of the set of minimal elements that is computed during each iteration, which may grow exponentially. 4 This is where continuous coverability becomes beneficial. In our approach, if a minimal element is not continuously coverable, it can safely be discarded since none of its predecessors is going to be coverable either, which substantially shrinks the predecessor set. In effect, this heuristic yields a powerful pruning technique, enabling us to achieve the aforementioned advantages when compared to other approaches on standard benchmarks. Some proof details are only sketched in the main part of this paper; full details can be found in the appendix. Related Work. Our approach is primarily related to the work by Esparza et al. [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF], by Kaiser, Kroening and Wahl [START_REF] Kaiser | A widening approach to multithreaded program verification[END_REF], and by Delzanno, Raskin and van Begin [START_REF] Delzanno | Attacking symbolic state explosion[END_REF]. In [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF], Esparza et al. presented an implementation of a semi-decision procedure for disproving coverability which was originally proposed by Esparza and Melzer [START_REF] Esparza | Verification of safety properties using integer programming: Beyond the state equation[END_REF]. It is based on the Petri-net state equation and traps as sufficient criteria in order to witness non-coverability. As shown in [START_REF] Esparza | Verification of safety properties using integer programming: Beyond the state equation[END_REF], those conditions can be encoded into an equi-satisfiable system of linear inequalities called the trap inequation in [START_REF] Esparza | Verification of safety properties using integer programming: Beyond the state equation[END_REF]. This approach is, however, prone to numerical imprecision that become problematic even for instances of small size [START_REF] Esparza | Verification of safety properties using integer programming: Beyond the state equation[END_REF]Sec. 5.3]. For that reason, the authors of [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF] resort to a CEGAR-based variant of the approach described in [START_REF] Esparza | Verification of safety properties using integer programming: Beyond the state equation[END_REF] which has the drawback that in the worst case, the CEGAR loop has to be executed an exponential number of times leading to an exponential number of queries to the underlying SMT-solver. We will show in Section 4.3 that the conditions used in [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF] are strictly subsumed by a subset of the conditions required to witness coverability in continuous Petri nets: whenever the procedure described in [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF] returns uncoverable then coverability does not hold in the continuous setting either, but not vice versa. Thus, a single satisfiability check to our formula in existential FO(Q + , +, >) encoding continuous coverability that we develop in this paper completely subsumes the CEGARapproach presented in [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF]. Another difference to [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF] is that here we present a sound and complete decision procedure.

Regarding the relationship of our work to [START_REF] Kaiser | A widening approach to multithreaded program verification[END_REF], Kaiser et al. develop in their paper an approach to coverability in richer classes of well-structured transition systems that is also based on the classical backward-analysis algorithm. They also employ forward analysis in order to prune the set of minimal elements during the backward iteration, and in addition a widening heuristic in order to overapproximate the minimal basis. Our approach differs in that our minimal basis is always precise yet as small as possible modulo continuous coverability. Thus no backtracking as in [START_REF] Kaiser | A widening approach to multithreaded program verification[END_REF] is needed, which is required when the widened basis turns out to be too inaccurate. Another difference is that for the forward analysis, a Karp-Miller tree is incrementally built in the approach described in [START_REF] Kaiser | A widening approach to multithreaded program verification[END_REF], whereas we use the continuous coverability over-approximation of coverability.

The idea of using an over-approximation of the reachability set of a Petri net in order to prune minimal basis elements inside a backward coverability framework was first described by Delzanno et al. [START_REF] Delzanno | Attacking symbolic state explosion[END_REF], who use place invariants as a pruning criterion. However, computing such invariants and checking if a minimal basis element can be pruned potentially requires exponential time.

Finally, a number of further techniques and tools for deciding Petri net coverability or more general well-structured transition systems have been described in the literature. They are, for instance, based on efficient data structures [START_REF] Ganty | Algorithmes et structures de données efficaces pour la manipulation de contraintes sur les intervalles[END_REF][START_REF] Finkel | Monotonic extensions of Petri nets: Forward and backward search revisited[END_REF][START_REF] Delzanno | Covering sharing trees: a compact data structure for parameterized verification[END_REF][START_REF] Ganty | Symbolic data structure for sets of k-uples[END_REF] and generic algorithmic frameworks such as EEC [START_REF] Geeraerts | Expand, enlarge and check: New algorithms for the coverability problem of WSTS[END_REF] and IC3 [START_REF] Kloos | Incremental, inductive coverability[END_REF].

Preliminaries

We denote by Q, Z and N the set of rationals, integers, and natural numbers, respectively, and by Q + the set of non-negative rationals. Throughout the whole paper, numbers are encoded in binary, and rational numbers as pairs of integers encoded in binary. Let D ⊆ Q, D E denotes the set of vectors indexed by a finite set E. A vector u is denoted by u

= (u i ) i∈E . Given vectors u = (u i ) i∈E , v = (v i ) i∈E ∈ D E , addition u + v is defined component-wise, and u ≤ v whenever u i ≤ v i for all i ∈ E. Moreover, u < v whenever u ≤ v and u = v. Let E ′ ⊆ E and v ∈ D E , we sometimes write v[E ′ ] as an abbreviation for (v i ) i∈E ′ . The support of v is the set v def = {i ∈ E : v i = 0}.
Given finite sets of indices E and F , and D ⊆ Q, D E×F denotes the set of matrices over D with rows and columns indexed by elements from E and F , respectively. Let M ∈ D E×F , E ′ ⊆ E and F ′ ⊆ F , we denote by M E ′ ×F ′ the D E ′ ×F ′ sub-matrix obtained from M whose row and columns indices are restricted respectively to E ′ and F ′ .

Petri Nets.

In what follows, we introduce the syntax and semantics of Petri nets. While we provide a single syntax for nets, we introduce a discrete (i.e. in N) and a continuous (i.e. in Q + ) semantics. Definition 1. A Petri net is a tuple N = (P, T, Pre, Post), where P is a finite set of places; T is a finite set of transitions with P ∩ T = ∅; and Pre, Post ∈ N P ×T are the backward and forward incidence matrices, respectively. A (discrete) marking of N is a vector of N P . A Petri net system (PNS) is a pair S = (N , m 0 ), where N is a Petri net and m 0 ∈ N P is the initial marking. The incidence matrix C of N is the P × T integer matrix defined by

C def = Post -Pre. The reverse net of N is N -1 def
= (P, T, Post, Pre). Let p ∈ P and t ∈ T , the pre-sets of p and t are the sets

• p def = {t ′ ∈ T : Post(p, t ′ ) > 0} and • t def = {p ′ ∈ P : Pre(p ′ , t) > 0}, respectively. Likewise, the post-sets of p and t are p • def = {t ′ ∈ T : Pre(p, t ′ ) > 0} and t • = {p ′ ∈ P : Post(p ′ , t) > 0}
, respectively. Those definitions can canonically be lifted to subsets of places and of transitions, e.g., for Q ⊆ P we have • Q = p∈Q • p. We also introduce the neighbors of a subset of places/transitions by:

• Q • = • Q ∪ Q • . Let S ⊆ T , then N S is the sub-net defined by N S def = ( • S • , S, Pre• S • ×S , Post• S • ×S ).
We say that a transition t ∈ T is enabled at a marking m whenever m(p) ≥ Pre(p, t) for every p ∈ • t. A transition t that is enabled can be fired, leading to a new marking m ′ such that for all places p ∈ P , m

′ (p) = m(p) + C(p, t). We write m t -→ m ′ whenever t is enabled at m leading to m ′ , and write m -→ m ′ if m t -→ m ′ for some t ∈ T . By -→ * we denote the reflexive transitive closure of -→. A word σ = t 1 t 2 • • • t k ∈ T * is a firing sequence of (N , m 0 ) whenever there exist markings m 1 , . . . , m k such that m 0 t1 -→ m 1 t2 -→ • • • t k-1 ---→ m k-1 t k -→ m k .
Given a marking m, the reachability problem asks whether m 0 -→ * m. The reachability problem is decidable, EXPSPACE-hard [START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report[END_REF] and in F ω 3 [START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF], a nonprimitive-recursive complexity class. In this paper, however, we are interested in deciding coverability, an EXPSPACE-complete problem [START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report[END_REF][START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. Definition 2. Given a Petri net system S = (P, T, Pre, Post, m 0 ) and a marking m ∈ N P , the coverability problem asks whether m 0 -→ * m ′ for some m ′ ≥ m.

Continuous Petri nets are Petri nets in which markings may consist of rational numbers 5 , and in which transitions may be fired a fractional number of times. Formally, a marking of a continuous Petri net is a vector m ∈ Q P + . Let t ∈ T , the enabling degree of t with respect to m is a function enab(t, m) ∈ Q + ∪ {∞} defined by:

enab(t, m) def = min{m(p)/Pre(p, t) : p ∈ • t} if • t = ∅, ∞ otherwise.
We

say that t is Q-enabled at m if enab(t, m) > 0. If t is Q-enabled it may be fired by any amount q ∈ Q + such that 0 ≤ q ≤ enab(t, m), leading to a new marking m ′ such that for all places p ∈ P , m(p) ′ def = m(p)+q•C(p, t).
In this case, we write

m q•t --→ m ′ . The definition of a Q-firing sequence σ = q 1 t 1 • • • q k t k ∈ (Q + × T ) * is analogous to the standard definition of firing sequence, and so are -→ Q , -→ * Q and Q-reachability. The Q-Parikh image of the firing sequence σ is the vector π(σ) ∈ Q T + such that π(σ)(t) def = ti=t q i .
We also adapt the decision problems for Petri nets. Definition 3. Given a Petri net system S = (P, T, Pre, Post, m 0 ) and a marking m ∈ Q P + , the Q-reachability (respectively Q-coverability) problem asks whether

m 0 -→ * Q m (respectively m 0 -→ * Q m ′ for some m ′ ≥ m).
Recently Q-reachability and Q-coverability were shown to be decidable in polynomial time [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF]. In Section 3.2, we will discuss in detail the approach from [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF]. For now, observe that m -→ m ′ implies m -→ Q m ′ , and hence m -→ * m ′ implies m -→ * Q m ′ . Consequently, Q-coverability provides an overapproximation of coverability: this fact is the cornerstone of this paper.

Upward Closed Sets. A set V ⊆ N P is upward closed if for every v ∈ V and w ∈ N P , v ≤ w implies w ∈ V . The upward closure of a vector v ∈ N P is the set ↑v def = {w ∈ N P : v ≤ w}.
This definition can be lifted to sets V ⊆ N P in the obvious way, i.e., ↑V def = v∈V ↑v. Due to N P being well-quasi-ordered by ≤, any upward-closed set V contains a finite set F ⊆ V such that V = ↑F . Such an F is called a basis of V and allows for a finite representation of an upwardclosed set. In particular, it can be shown that V contains a unique minimal basis B ⊆ V that is minimal with respect to inclusion for all bases F ⊆ V . We denote minbase(F ) this minimal basis obtained by deleting vectors v ∈ F such that there exists w ∈ F with w < v (when F is finite).

Deciding Coverability and Q-Reachability

We now introduce and discuss existing algorithms for solving coverability and Q-reachability which form the basis of our approach. The main reason for doing so is that it allows us to smoothly introduce some additional notations and concepts that we require in the next section. For the remainder of this section, we fix some Petri net system S = (N , m 0 ) with N = (P, T, Pre, Post), and some marking m to be covered or Q-reached.

The Backward Coverability Algorithm

The standard backward coverability algorithm, Algorithm 1, is a simple to state algorithm.

-It iteratively constructs minimal bases M , where in the k-th iteration, M is the minimal basis of the (upward closed) set of markings that can cover m after a firing sequence of length at most k. If m 0 ∈ ↑M , the algorithm returns true, i.e., that m is coverable. Otherwise, in order to update M , for all

m ′ ∈ M and t ∈ T it computes m ′ t (p) def = max{Pre(p, t), m ′ (p)-C(p, t)}. The singleton {m ′ t }
is the minimal basis of the set of vectors that can cover m ′ after firing t.

-Thus defining pb(M ) as pb(M

) def = m ′ ∈M,t∈T {m ′ t }, M ∪ pb(M
) is a (not necessarily minimal) basis of the upward closed set of markings that can cover m after a firing sequence of length at most k + 1. This basis can be then minimized in every iteration.

Algorithm 1 Backward Coverability

Require: PNS S = (N , m0) and a marking m ∈ N P 1: M := {m}; 2: while m0 ∈ ↑M do 3:

B := pb(M ) \ ↑M ; 4: if B = ∅ then 5:
return false; 6: else 7:

M := minbase(M ∪ B); 8: return true;

The termination of the algorithm is guaranteed due to N P being well-quasiordered, which entails that M must stabilize and return false in this case. It can be shown that Algorithm 1 runs in 2-EXP [START_REF] Bozzelli | Complexity analysis of the backward coverability algorithm for VASS[END_REF]. The key point to the (empirical) performance of the algorithm is the size of the set M during its computation: the smaller, the better. Even though one can establish a doubly-exponential lower bound on the cardinality of M during the execution of the algorithm, in general not every element in M is coverable, even when m is coverable.

The Q-Reachability Algorithm

We now present the fundamental concepts of the polynomial-time Q-reachability algorithm of Fraca and Haddad [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF]. The key insight underlying their algorithm is that Q-reachability can be characterized in terms of three simple criteria. The algorithm relies on the notions of firing set and maximal firing set, denoted fs(N , m) and maxfs(N , m), and defined as follows:

fs(N , m) def = { π(σ) : σ ∈ (Q + × T ) * , there is m ′ ∈ Q P + s.t. m σ -→ Q m ′ } maxfs(N , m) def = T ′ ∈fs(N ,m) T ′ .
Thus, fs(N , m) is the set of supports of firing sequences starting in m. Even though fs(N , m) can be of size exponential with respect to |T |, deciding T ′ ∈ fs(N , m) for some T ′ ⊆ T can be done in polynomial time, and maxfs(N , m) is also computable in polynomial time [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF]. The following proposition characterizes the set of Q-reachable markings.

Proposition 4 ([14, Thm. 20]). A marking

m is Q-reachable in S = (N , m 0 ) if and only if there exists x ∈ Q T + such that (i) m = m 0 + C • x (ii) x ∈ fs(N , m 0 ) (iii) x ∈ fs(N -1 , m)
In this characterization, x is supposed to be the Parikh image of a firing sequence. The first item expresses the state equation of S with respect to m 0 , Algorithm 2 Q-reachability [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF] Require: PNS S = (N , m0) with N = (P, T, Pre, Post) and a marking m 1: if m = m0 then 2: return true; 3: T ′ := T ; 4: while T ′ = ∅ do 5:

S := ∅; 6:

for all t ∈ T ′ do 7:

x

:= solve(C P ×T ′ • x = m -m0 ∧ x(t) > 0 ∧ x ∈ Q T ′ + ); 8:
if x = undef then 9:

S := S ∪ x ; 10:

if S = ∅ then 11:

return false; 12:

T ′ := maxfs(NS, m0[ • S • ])) ∩ maxfs(N -1 S , m[ • S • ])) 13:
if T ′ = S then 14:

return true; 15: return false; m and x. The two subsequent items express that the support of the solution of the state equation has to lie in the firing sets of S and its reverse. As such, the characterization in Proposition 4 yields an NP algorithm. By employing a greatest fixed point computation, Algorithm 2, which is a decision variant of the algorithm presented in [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF], turns those criteria into a polynomial-time algorithm (see [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF] for a proof of its correctness). In order to use Algorithm 2 for deciding coverability, it is sufficient, for each place p, to add a transition to N that can at any time non-deterministically decrease p by one token. Denote the resulting Petri net system by S ′ , it can easily checked that m is Q-coverable in S if and only if m is Q-reachable in S ′ .

Backward Coverability Modulo Q-Reachability

We now present our decision algorithm for the Petri net coverability problem.

Encoding

Q-Reachability into Existential FO(Q + , +, >)
Throughout this section, when used in formulas, w and x are vectors of firstorder variables indexed by P representing markings, and y is a vector of firstorder variables indexed by T representing the Q-Parikh image of a transition sequence.

Condition (i) of Proposition 4, which expresses the state equation, is readily expressed as a system of linear equations and thus directly corresponds to a formula Φ(w, x, y) which holds whenever a marking x is reached starting at marking w by firing every transition y(t) times (without any consideration whether such a firing sequence would actually be admissible):

Φ N eqn (w, x, y) def = x = C • y + w.
Next, we show how to encode Conditions (ii) and (iii) into suitable formulas. To this end, we require an effective characterization of membership in the firing set fs(N , w) defined in Section 3.2. The following characterization can be derived from [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF]Cor. 19]. First, we define a monotonic increasing function incfs N ,w : 2 T → 2 T as follows:

incfs N ,w (S) def = S ∪ {t ∈ T (N ) : • t ⊆ w ∪ {s • : s ∈ S}} .
From [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF]Cor. 19], it follows that T ′ ∈ fs(N , w) if and only if T ′ = lfp(incfs N T ′ ,w ), where lfp is the least fixed point operator 6 , i.e.,

′ = incfs N T ′ ,w (• • • (incfs N T ′ ,w (∅)) • • • ).
Clearly, the least fixed point is reached after at most |T ′ | iterations.

In order to decide whether y ∈ fs(N , w), we simulate this fixed-point computation in an existential FO(Q + , +, >)-formula Φ N fs (w, y). Our approach is inspired by a technique of Verma, Seidl and Schwentick that was used to show that the reachability relation for communication-free Petri nets is definable by an existential Presburger arithmetic formula of linear size [START_REF] Kumar | On the complexity of equational horn clauses[END_REF]. The basic idea is to introduce additional first-order variables z indexed by P ∪ T that, given a firing set, capture the relative order in which transitions of this set are fired and the order in which their input places are marked. This order corresponds to the computation of lfp(incfs N y ,w ) and is encoded via a numerical value z(t) (respectively z(p)), representing an index that must be strictly greater than zero for a transition (respectively an input place of a transition) of this set. In addition, input places have to be marked before the firing of a transition:

Φ N dt (y, z) def = t∈T y(t) > 0 → p∈ • t 0 < z(p) ≤ z(t) .
Moreover, a place is either initially marked or after the firing of a transition of the firing set. So:

Φ N mk (w, y, z) def = p∈P z(p) > 0 → w(p) > 0 ∨ t∈ • p y(t) > 0 ∧ z(t) < z(p) .
We can now take the conjunction of the formulas above in order to obtain a logical characterization of fs(N , w):

Φ N fs (w, y) def = ∃z : Φ N dt (y, z) ∧ Φ N mk (w, y, z).
Having logically characterized all conditions of Proposition 4, we can define the global Q-reachability relation for a Petri net system S = (N , w) as follows:

Φ S (w, x) def = ∃y : Φ N eqn (w, x, y) ∧ Φ N fs (w, y) ∧ Φ N -1 fs (x, y).
In summary, we have thus proved the following result in this section. Φ(x) := Φ(x) ∧ v∈D x ≥ v; 13: return true; Proposition 5. Let S = (N , m 0 ) be a Petri net system and m be a marking. There exists an existential FO(Q + , +, >)-formula Φ S (w, x) computable in linear time such that m is Q-reachable in S if and only if Φ S (m 0 , m) is valid.

Checking satisfiability of Φ S is in NP, see e.g. [START_REF] Sontag | Real addition and the polynomial hierarchy[END_REF]. It is a valid question to ask why one would prefer an NP-algorithm over a polynomial-time one. We address this question in the next section. For now, note that in order to obtain an even more accurate over-approximation, we can additionally restrict y to be interpreted in the natural numbers while retaining membership of satisfiability in NP, due to the following variant of Proposition 4: If a marking is reachable in S then there exists some y ∈ N T such that Conditions (i), (ii) and (iii) of Proposition 4 hold. Remark 6. Proposition 5 additionally allows us to improve the best known upper bound for the inclusion problem of continuous Petri nets, which is EXP [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF]. Given two Petri net systems S = (N , m 0 ) and S ′ = (N ′ , m ′ 0 ) over the same set of places, this problem asks whether the set of reachable markings of S is included in S ′ , i.e., whether ∀m.Φ S (m 0 , m) → Φ S ′ (m ′ 0 , m) is valid. The latter is a Π 2 -sentence of FO(Q + , +, >) and decidable in Π P 2 [START_REF] Sontag | Real addition and the polynomial hierarchy[END_REF]. Hence, inclusion between continuous Petri nets is in Π P 2 .

The Coverability Decision Procedure

We now present Algorithm 3 for deciding coverability. This algorithm is an extension of the classical backward reachability algorithm that incorporates Qreachability checks during its execution in order to keep the set of minimal basis elements small. First, on Line 1 we derive an open formula Φ(x) from Φ S such that Φ(x) holds if and only if x is Q-coverable in S. Then, on Line 2, the algorithm checks whether the marking m is Q-coverable using the polynomial-time algorithm from [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF] and returns that m is not coverable if this is not the case. Otherwise, the algorithm enters a loop which iteratively computes a basis M of the backward coverability set starting at m whose elements are in addition Q-coverable in S. To this end, on Line 5 the algorithm computes a set B of new basis elements obtained from one application of pb, and on Line 7 it removes from B the set D which contains all elements of B which are not Q-coverable. If as a result B is empty the algorithm concludes that m is not coverable in S. Otherwise, on Line 11 it adds the elements of B to M . Finally, Line 12 makes sure that in future iterations of the loop the underlying SMT solver can immediately discard elements that lie in ↑D. The latter is technically not necessary, but it provides some guidance to the SMT solver. The proof of the following proposition is deferred to Appendix A. In this way, the empirically chosen parameters c and k create a bottleneck that gives priority to elements with small sum-norms, as they are more likely to allow for discarding elements with larger sum-norms in future iterations. This variation of Algorithm 3 has the same correctness properties as the original one: It can be shown that using min c,k B instead of B in Line 11 computes the same set ↑M at the expense of delaying its stabilization.

Before we conclude this section, let us come back to the question why in our approach we choose using Φ S (whose satisfiability is in NP) over Algorithm 2 which runs in polynomial time. In Algorithm 3, we invoke Algorithm 2 only once in Line 2 in order to check if S is not Q-coverable, and thereafter only employ Φ S which gets incrementally updated during each iteration of the loop. The reason is that in practice as observed in our experimental evaluation below, Algorithm 2 turns out to be often faster for a single Q-coverability query. Otherwise, as soon Φ S has been checked for satisfiability once, future satisfiability queries are significantly faster than Algorithm 2, which is a desirable behavior inside a backward coverability framework. Moreover we can constraint solutions to be in N instead of Q, leading to a more precise over approximation.

Relationship to the CEGAR-approach of Esparza et al.

In [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF], Esparza et al. presented a semi-decision procedure for coverability that is based on [START_REF] Esparza | Verification of safety properties using integer programming: Beyond the state equation[END_REF] and employs the Petri net state equation and traps inside a CEGAR-framework. A trap in N is a non-empty subset of places

Q ⊆ P such that Q • ⊆ • Q, and Q ⊆ P is a siphon in N whenever • Q ⊆ Q • . Given a marking m, a trap (respectively siphon) is marked in m if p∈Q m(p) > 0.
An important property of traps is that if a trap is marked in m, it will remain marked after

• p0 t1 p1 t2 2
Fig. 1. A Petri net that cannot mark p1.

any firing sequence starting in m. Conversely, when a siphon is unmarked in m it remains so after any firing sequence starting in m. By definition, Q is a trap in N if and only if Q is a siphon in N -1 . The coverability criteria that [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF] builds upon are derived from [START_REF] Esparza | Verification of safety properties using integer programming: Beyond the state equation[END_REF] and can be summarized as follows.

Proposition 9 ([10]). If m is Q-reachable (respectively reachable) in (N , m 0 ) then there exists x ∈ Q T + (respectively x ∈ N T ) such that: (i) m = m 0 + C • x (ii) for all traps Q ⊆ P , if Q is marked in m 0 then Q is marked in m
As in our approach, in [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF] those criteria are checked using an SMT-solver. The for-all quantifier is replaced in [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF] by incrementally enumerating all traps in a CEGAR-style fashion. It is shown in [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF]Prop. 18] that Condition (iii) of Proposition 4 is equivalent to requiring that N -1 x has no unmarked siphon in m, which appears to be similar to Condition (ii) of Proposition 9. In fact, we show the following.

Proposition 10. Conditions (i) and (iii) of Proposition 4 strictly imply Conditions (i) and (ii) of Proposition 9 (when interpreted over

Q + ).
Proof. We only show strictness, the remainder of the proof is deferred to Appendix B. To this end, consider the Petri net (N , m 0 ) depicted in Figure 1 with m = (0, 1). Clearly m is not reachable. There is a single solution to the state equation x = (1, 0). There is a single trap {p 1 } which is unmarked in m 0 . So the conditions of Proposition 9 hold, and hence the algorithm of [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF] does not decide this net safe. On the contrary in N -1

x , the reverse net without t 2 , {p 0 } is a siphon that is unmarked in m. So Condition (iii) of Proposition 4 does not hold.

⊓ ⊔

This proposition shows that the single formula stated in Proposition 5 strictly subsumes the approach from [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF]. Moreover, it provides a theoretical justification for why the approach of [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF] performs so well in practice: the conditions are a strict subset of the conditions developed for Q-reachability in [START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF].

Experimental Evaluation

We evaluate the backward coverability modulo Q-reachability algorithm on standard benchmarks from the literature with two goals in mind. First, we demonstrate that our approach is competitive with existing approaches. In particular, we prove significantly more safe instances of our benchmarks safe in less time when compared to any other approach. Overall our algorithm decides 142 out of 176 instances, the best competitor decides 122 instances. Second, we demonstrate that Q-coverability is a powerful pruning criterion by analyzing the relative number of minimal bases elements that get discarded during the execution of Algorithm 3. We implemented Algorithm 3 in a tool called QCover in the programming language Python. 7 The underlying SMT-solver is z3 [START_REF] Mendonça De Moura | Z3: an efficient SMT solver[END_REF]. For the min c,k heuristic mentioned in Remark 8, we empirically chose c = 10 and k = 5. We observed that any sane choice of c and k leads to an overall speed-up, though different values lead to different (even increasing) running times on individual instances. QCover takes as input coverability instances in the mist file format. 8 The basis of our evaluation is the benchmark suite that was used in order to evaluate the tool Petrinizer, see [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF] and the references therein. This suite consists of five benchmark categories: mist, consisting of 27 instances from the mist toolkit; bfc, consisting of 46 instances used for evaluating BFC; medical and bug tracking, consisting of 12 and 41 instances derived from the provenance analysis of messages of a medical and a bug-tracking system, respectively; and soter, consisting of 50 instances of verification conditions derived from Erlang programs [START_REF] Emanuele | Automatic verification of Erlang-style concurrency[END_REF].

We compare QCover with the following tools: Petrinizer [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF], mist [START_REF] Ganty | Algorithmes et structures de données efficaces pour la manipulation de contraintes sur les intervalles[END_REF] and bfc [START_REF] Kaiser | A widening approach to multithreaded program verification[END_REF] in their latest versions available at the time of writing of this paper. mist implements a number of algorithms, we use the backward algorithm that uses places invariant pruning [START_REF] Ganty | Symbolic data structure for sets of k-uples[END_REF]. 9 All benchmarks were performed on a single computer equipped with four Intel R Core TM 2.00 GHz CPUs, 8 GB of memory and Ubuntu Linux 14.04 (64 bits). The execution time of the tools was limited to 2000 seconds (i.e. 33 minutes and 20 seconds) per benchmark instance. The running time of every tool on an instance was determined using the sum of the user and sys time reported by the Linux tool time.

Figure 2 contains three tables which display the number of safe instances shown safe, unsafe instances shown unsafe, and the total number of instances of our benchmark suite decided by each individual tool. As expected, our algorithm outperforms all competitors on safe instances, since in this case a proof of safety (i.e. non-coverability) effectively requires the computation of the whole backward coverability set, and this is where pruning via Q-coverability becomes most beneficial. On the other hand, QCover remains competitive on unsafe instances, though a tool such as BFC handles those instances better since its heuristics are more suited for proving unsafety (i.e. coverability). Nevertheless, QCover is the overall winner when comparing the number of safe and unsafe instances decided, being far ahead at the top of the leader-board deciding 142 out of 176 instances.

QCover not only decides more instances, it often does so faster than its competitors. Figure 3 contains two graphs which show the cumulative number of instances proven safe and the total number of instances decided on all suites 7 QCover is available at http://www-etud.iro.umontreal.ca/ ~blondimi/qcover/. by each tool within a certain amount of time. When it comes to safety, QCover is always ahead of all other tools. However, when looking at all instances decided, BFC first has an advantage. We observed that this advantage occurs on instances of comparably small size. As soon as large instances come into play, QCover wins the race. Besides different heuristics used, one reason for this might be the choice of the implementation language (C for BFC vs. Python for QCover).

In particular, BFC can decide a non-negligible number of instances in less than 10ms, which QCover never achieves. Finally, we consider the effectiveness of using Q-coverability as a pruning criterion. To this end, consider Figure 4 in which we plotted the number of times a certain percentage of basis elements was removed due to not being Q-coverable. Impressively, in some cases more than 95% of the basis elements get discarded. Overall, on average we discard 56% of the basis elements, which substantiates the usefulness of using Q-coverability as a pruning criterion.

Before we conclude, let us mention that already 83 instances are proven safe by only checking the state equation, and that additionally checking for the criteria (ii) and (iii) of Proposition 4 increases this number to 101 instances. If we use Algorithm 2 instead of our FO(Q + , +, >) encoding then we can only decide 132 instances in total. Finally, in our experiments, interpreting variables over Q instead of N resulted in no measurable overall performance gain. In summary, our experimental evaluation shows that the backward coverability modulo Q-reachability approach to the Petri net coverability problem developed in this paper is highly efficient when run on real-world instances, and superior to existing tools and approaches when compared on standard benchmarks from the literature.

Conclusion

In this paper, we introduced backward coverability modulo Q-reachability, a novel approach to the Petri net coverability problem that is based on using coverability in continuous Petri nets as a pruning criterion inside a backward coverability framework. A key ingredient for the practicality of this approach is an existential FO(Q + , +, >)-characterization of continuous reachability, which we showed to strictly subsume a recently introduced coverability semi-decision procedure [START_REF] Esparza | An SMT-based approach to coverability analysis[END_REF]. Finally, we demonstrated that our approach significantly outperforms existing ones when compared on standard benchmarks.

There are a number of possible avenues for future work. It seems promising to combine the forward analysis approach based on incrementally constructing a Karp-Miller tree that is used in BFC [START_REF] Kaiser | A widening approach to multithreaded program verification[END_REF] with the Q-coverability approach introduced in this paper. In particular, recently developed minimization and acceleration techniques for constructing Karp-Miller trees should prove beneficial, see e.g. [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]. Another way to improve the empirical performance of our algorithm is to internally use more efficient data structures such as sharing trees [START_REF] Delzanno | Covering sharing trees: a compact data structure for parameterized verification[END_REF]. It seems within reach that a tool which combines all of the aforementioned techniques and heuristics could decide all of the benchmark instances we used in this paper within reasonable resource restrictions.

A Proof of Propositon 7

Proof. Let B n and M n be respectively the value of B and M at Line Since m can be covered from m 0 if and only if Q-coverable(S, m 0 ) and m 0 -→ * m, it follows that Line 9 and 13 are correct and thus that the algorithm is correct. Regarding termination, it is well-known that, for well-quasi-ordered sets, any inclusion chain of upward closed sets stabilizes. Therefore, the chain ↑M 1 ⊆ ↑M 2 ⊆ . . . stabilizes to some ↑M n . Thus, after a finite number of iterations, either B becomes empty at Line 8 or m 0 ∈ ↑M at Line 4. Hence, the algorithm always terminates.

⊓ ⊔

B Proof of Proposition 10

Proof. We write marked (Q, m) if Q is marked in m, and unmarked (Q, m) otherwise. We establish the contrapositive: assuming that for all x ∈ Q T + some condition of Proposition 9 does not hold, we show that for all x ∈ Q T + some Condition (i) and (iii) of Proposition 4 does not hold. To this end, let x ∈ Q T + , if Condition (i) of Proposition 9 does not hold, i.e., m = m 0 + C • x, then Condition (i) of Proposition 4 does not hold either. Thus, assume that m = m 0 +C•x. We then have the following: there is a trap Q in N s.t. marked (Q, m 0 ) and unmarked (Q, m) =⇒ there is a siphon Q in N -1 s.t. marked (Q, m 0 ) and unmarked(Q, m)

( * )
=⇒ there is a siphon Q ′ in N -1 T ′ s.t. unmarked (Q ′ , m), where T ′ = x =⇒ x / ∈ fs(N -1 , m).

In order to show the implication ( * ), we first observe that m

[Q] = m 0 [Q], since
Q is marked in m 0 and not marked in m. Let T ′ def = x and P ′ def = • T ′ • , we claim that Q ′ def = Q ∩ P ′ is a siphon in N T ′ . Let t ∈ T ′ and suppose that t ∈ • Q ′ . Since Q ′ ⊆ Q, we have t ∈ • Q and hence t ∈ Q • , which yields t ∈ Q ′• as all the neighbour places of t belong to P ′ . It remains to show that Q ′ = ∅. To the contrary, assume that Q ′ = ∅, then x(t) = 0 for every t ∈ • Q • and hence m[Q] = m 0 [Q], a contradiction.

⊓ ⊔

Algorithm 3 : return false 4 :

 34 Backward Coverability Modulo Q-Reachability Require: PNS S = (N , m0) and a marking m ∈ N P 1: M := {m}; Φ(x) := ∃y : ΦS (m0, y) ∧ y ≥ x; 2: if not Q-coverable(S, m) then 3while m0 ∈ ↑M do 5: B := pb(M ) \ ↑M ; 6: D := {v ∈ B : unsat (Φ(v)minbase(M ∪ B); 12:

Proposition 7 .

 7 Let S = (N , m 0 ) be a PNS and m be a marking. Then m is coverable in S if and only if Algorithm 3 returns true. Remark 8. In our actual implementation, we use a slight variation of Algorithm 3 in which the instruction M := minbase(M ∪ B) in Line 11 is replaced by M := minbase(M ∪ min c,k B). Here, c, k ∈ N are parameters to the algorithm, and min c,k B is the set of the c + |B|/k elements of B with the smallest sum-norm.

Fig. 3 .

 3 Fig. 3. Cumulative number of instances proven safe (left) and total number of instances decided (right) within a fixed amount of time.

Fig. 4 .

 4 Fig. 4. Number of times a certain percentage of basis elements was removed due to Q-coverability pruning.

  [START_REF] Delzanno | Attacking symbolic state explosion[END_REF] and Line 11 in the n-th iteration of the while-loop. It is possible to show by induction on n that↑M n = y∈↑m x ∈ N d : Q-coverable(S, x) ∧ ∃σ ∈ T * s.t. x σ -→ y ∧ |σ| ≤ n B n ⊆ ↑M n \ ↑M n-1 .

  Number of safe instances (top-left), unsafe instances (top-right) and total instances (bottom) decided by every tool. Bold numbers indicate the tool(s) which decide(s) the largest number of instances in the respective category.

	Suite	QCover Petrinizer mist bfc Total		Suite	QCover Petrinizer mist bfc Total
	mist	23	20		22 20	23		mist		3	-	4	4	4
	medical	11	4	11 3	12		medical		-	-	--	0
	bfc	2	2		2	2	2		bfc		26	-	29 42	44
	bug tracking	32	32		0 19	40	bug tracking	0	-	0	1	1
	soter	37	37		0 19	38		soter		8	-	6 12	12
	Total	105	95		35 63 115		Total		37	0		39 59	61
				Suite		QCover Petrinizer mist bfc Total
				mist		26		20	26 24	27
			medical	11		4		11 3	12
				bfc		28		2		31 44	46
			bug tracking	32		32	0 20	41
				soter		45		37	6 31	50
				Total		142	95	74 122 176
	Fig. 2. 1 20 40 60 80 100 number of instances proven safe in ≤ t secs.	4	16	64	256	2000	number of instances proven	(un)safe in ≤ t secs.	40 60 80 100 120 140	1	4	16	64	256	2000
			time t in seconds							time t in seconds
			QCover		Petrinizer		bfc	mist
	8 https://github.com/pierreganty/mist/wiki#input-format-of-mist
	9 https://github.com/pierreganty/mist/wiki#coverability-checkers-included-in-mist

This problem is commonly referred to as the symbolic state explosion problem, cf.[START_REF] Delzanno | Covering sharing trees: a compact data structure for parameterized verification[END_REF].

In fact, the original definition allows for real numbers, however for studying decidability and complexity issues, rational numbers are more convenient.

In[START_REF] Fraca | Complexity analysis of continuous Petri nets[END_REF] Cor. 19], an algorithm is presented that basically computes lfp(incfs N T ′ ,w ).

Acknowledgments. We would like to thank Vincent Antaki for an early implementation of Algorithm 2. We would also like to thank Gilles Geeraerts for his support with the MIST file format.

⋆ Supported by the Fonds québécois de la recherche sur la nature et les technologies (FQRNT), by the French ⋆ ⋆ ⋆ Supported by ERC project EQualIS (FP7-308087).