Approaching the Coverability Problem Continuously
 9 Citations
 1.3k Downloads
Abstract
The coverability problem for Petri nets plays a central role in the verification of concurrent sharedmemory programs. However, its high EXPSPACEcomplete complexity poses a challenge when encountered in realworld 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 polynomialtime 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.
Keywords
Coverability Problem Standard Benchmark Input Place Firing Sequence Pruning Criterion1 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 realworld 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 [19] multithreaded nonrecursive finitestate programs with shared variables, which naturally occur in predicateabstractionbased 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 [4, 21, 24]. Despite this huge worstcase 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 realworld 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 SMTsolvers inside a backwardcoverability framework. In [14], Fraca and Haddad solved longstanding open problems about the complexity of decision problems for socalled continuous Petri nets. This class was introduced by David and Alla [5] and allows for transitions to be fired a nonnegative real number of times—hence places may contain a nonnegative real number of tokens. The contribution of [14] was to present polynomialtime algorithms that decide all of coverability, reachability and boundedness in this class. A further benefit of [14] 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 nonnegative rational numbers with addition and order (FO(\(\mathbb {Q}_{+}, +,>\))). This encoding paves the way for deciding coverability in continuous Petri nets inside SMTsolvers 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 SMTsolvers. Moreover, we show that our encoding in effect strictly subsumes a recently introduced CEGARbased approach to coverability described by Esparza et al. in [10]; in particular we can completely avoid the potentially exponentially long CEGARloop, cf. the related work section below. The benefit of coverability in continuous Petri nets is that it provides a way to overapproximate 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 backwardcoverability framework as follows. Starting at the target configuration to be covered, the classical backwardcoverability algorithm [1] 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 wellstructured transition systems [13]. 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.^{1} 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.
Due to space constraints, we only sketch some of the proofs in this paper. Full details can be found in [2].
Related Work. Our approach is primarily related to the work by Esparza et al. [10], by Kaiser, Kroening and Wahl [20], and by Delzanno, Raskin and van Begin [7]. In [10], Esparza et al. presented an implementation of a semidecision procedure for disproving coverability which was originally proposed by Esparza and Melzer [11]. It is based on the Petrinet state equation and traps as sufficient criteria in order to witness noncoverability. As shown in [11], those conditions can be encoded into an equisatisfiable system of linear inequalities called the trap inequation in [11]. This approach is, however, prone to numerical imprecision that become problematic even for instances of small size [11, Sect. 5.3]. For that reason, the authors of [10] resort to a CEGARbased variant of the approach described in [11] 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 SMTsolver. We will show in Sect. 4.3 that the conditions used in [10] are strictly subsumed by a subset of the conditions required to witness coverability in continuous Petri nets: whenever the procedure described in [10] 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(\(\mathbb {Q}_{+}, +,>\)) encoding continuous coverability that we develop in this paper completely subsumes the CEGARapproach presented in [10]. Another difference to [10] is that here we present a sound and complete decision procedure.
Regarding the relationship of our work to [20], Kaiser et al. develop in their paper an approach to coverability in richer classes of wellstructured transition systems that is also based on the classical backwardanalysis 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 [20] is needed, which is required when the widened basis turns out to be too inaccurate. Another difference is that for the forward analysis, a KarpMiller tree is incrementally built in the approach described in [20], whereas we use the continuous coverability overapproximation of coverability.
The idea of using an overapproximation 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. [7], 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 wellstructured transition systems have been described in the literature. They are, for instance, based on efficient data structures [8, 12, 15, 16] and generic algorithmic frameworks such as EEC [17] and IC3 [22].
2 Preliminaries
We denote by \(\mathbb {Q}\), \(\mathbb {Z}\) and \(\mathbb {N}\) the set of rationals, integers, and natural numbers, respectively, and by \(\mathbb {Q}_{+}\) the set of nonnegative rationals. Throughout the whole paper, numbers are encoded in binary, and rational numbers as pairs of integers encoded in binary. Let \(\mathbb {D}\subseteq \mathbb {Q}\), \(\mathbb {D}^E\) denotes the set of vectors indexed by a finite set E. A vector \(\varvec{u}\) is denoted by \(\varvec{u}=(u_i)_{i\in E}\). Given vectors \(\varvec{u} = (u_i)_{i\in E}, \varvec{v} = (v_i)_{i\in E}\in \mathbb {D}^E\), addition \(\varvec{u} + \varvec{v}\) is defined componentwise, and \(\varvec{u} \le \varvec{v}\) whenever \(u_i \le v_i\) for all \(i\in E\). Moreover, \(\varvec{u} < \varvec{v}\) whenever \(\varvec{u} \le \varvec{v}\) and \(\varvec{u} \ne \varvec{v}\). Let \(E' \subseteq E\) and \(\varvec{v}\in \mathbb {D}^{E}\), we sometimes write \(\varvec{v}[E']\) as an abbreviation for \((v_i)_{i \in E'}\). The support of \(\varvec{v}\) is the set \(\llbracket \varvec{v} \rrbracket \mathop {=}\limits ^{\text {def}}\{ i \in E : \varvec{v}_i \ne 0 \}\).
Given finite sets of indices E and F, and \(\mathbb {D}\subseteq \mathbb {Q}\), \(\mathbb {D}^{E\times F}\) denotes the set of matrices over \(\mathbb {D}\) with rows and columns indexed by elements from E and F, respectively. Let \(\mathbf {M}\in \mathbb {D}^{E\times F}\), \(E'\subseteq E\) and \(F' \subseteq F\), we denote by \(\mathbf {M}_{E'\times F'}\) the \(\mathbb {D}^{E'\times F'}\) submatrix obtained from \(\mathbf {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 \(\mathbb {N}\)) and a continuous (i.e. in \(\mathbb {Q}_{+}\)) semantics.
Definition 1
A Petri net is a tuple \(\mathcal {N}= (P, T, \mathbf {Pre}, \mathbf {Post})\), where P is a finite set of places; T is a finite set of transitions with \(P\cap T = \emptyset \); and \(\mathbf {Pre}, \mathbf {Post}\in \mathbb {N}^{P\times T}\) are the backward and forward incidence matrices, respectively.
A (discrete) marking of \(\mathcal {N}\) is a vector of \(\mathbb {N}^P\). A Petri net system (PNS) is a pair \(\mathcal {S}= (\mathcal {N}, \varvec{m}_0)\), where \(\mathcal {N}\) is a Petri net and \(\varvec{m}_0 \in \mathbb {N}^P\) is the initial marking. The incidence matrix \(\mathbf {C}\) of \(\mathcal {N}\) is the \(P \times T\) integer matrix defined by \(\mathbf {C} \mathop {=}\limits ^{\text {def}}\mathbf {Post} \mathbf {Pre}\). The reverse net of \(\mathcal {N}\) is \(\mathcal {N}^{1} \mathop {=}\limits ^{\text {def}}(P, T, \mathbf {Post}, \mathbf {Pre})\). Let \(p \in P\) and \(t \in T\), the presets of p and t are the sets \({^\bullet p} \mathop {=}\limits ^{\text {def}}\{t' \in T : \mathbf {Post}(p,t') > 0\}\) and \({^\bullet t}\mathop {=}\limits ^{\text {def}}\{ p' \in P : \mathbf {Pre}(p',t) > 0\}\), respectively. Likewise, the postsets of p and t are \({p^\bullet } \mathop {=}\limits ^{\text {def}}\{t' \in T : \mathbf {Pre}(p, t') > 0\}\) and \({t^\bullet } = \{p' \in P : \mathbf {Post}(p', t) > 0\}\), respectively. Those definitions can canonically be lifted to subsets of places and of transitions, e.g., for \(Q\subseteq P\) we have \({^\bullet Q} = \bigcup _{p\in Q} {^\bullet p}\). We also introduce the neighbors of a subset of places/transitions by: \({^\bullet {Q} ^\bullet }={^\bullet Q}\cup {Q^\bullet }\). Let \(S\subseteq T\), then \(\mathcal {N}_{S}\) is the subnet defined by \(\mathcal {N}_{S} \mathop {=}\limits ^{\text {def}}({^\bullet {S} ^\bullet }, S, \mathbf {Pre}_{{^\bullet {S} ^\bullet }\times S}, \mathbf {Post}_{{^\bullet {S} ^\bullet }\times S})\).
Definition 2
Given a Petri net system \(\mathcal {S}= (P, T, \mathbf {Pre}, \mathbf {Post}, \varvec{m}_0)\) and a marking \(\varvec{m} \in \mathbb {N}^P\), the coverability problem asks whether \(\varvec{m}_0 \xrightarrow {}^* \varvec{m}'\) for some \(\varvec{m}'\ge \varvec{m}\).
Definition 3
Given a Petri net system \(\mathcal {S}= (P, T, \mathbf {Pre}, \mathbf {Post}, \varvec{m}_0)\) and a marking \(\varvec{m} \in \mathbb {Q}_{+}^P\), the \(\mathbb {Q}\)reachability (respectively \(\mathbb {Q}\)coverability) problem asks whether \(\varvec{m}_0 \xrightarrow {}_\mathbb {Q}^* \varvec{m}\) (respectively \(\varvec{m}_0 \xrightarrow {}_\mathbb {Q}^* \varvec{m}'\) for some \(\varvec{m}'\ge \varvec{m}\)).
Recently \(\mathbb {Q}\)reachability and \(\mathbb {Q}\)coverability were shown to be decidable in polynomial time [14]. In Sect. 3.2, we will discuss in detail the approach from [14]. For now, observe that \(\varvec{m} \xrightarrow {} \varvec{m}'\) implies \(\varvec{m} \xrightarrow {}_\mathbb {Q}\varvec{m}'\), and hence \(\varvec{m} \xrightarrow {}^* \varvec{m}'\) implies \(\varvec{m} \xrightarrow {}_\mathbb {Q}^* \varvec{m}'\). Consequently, \(\mathbb {Q}\)coverability provides an overapproximation of coverability: this fact is the cornerstone of this paper.
Upward Closed Sets. A set \(V \subseteq \mathbb {N}^P\) is upward closed if for every \(\varvec{v} \in V\) and \(\varvec{w} \in \mathbb {N}^P\), \(\varvec{v} \le \varvec{w}\) implies \(\varvec{w} \in V\). The upward closure of a vector \(\varvec{v} \in \mathbb {N}^P\) is the set \({\uparrow }\varvec{v} \mathop {=}\limits ^{\text {def}}\{\varvec{w}\in \mathbb {N}^P : \varvec{v} \le \varvec{w}\}\). This definition can be lifted to sets \(V \subseteq \mathbb {N}^P\) in the obvious way, i.e., \({\uparrow }V \mathop {=}\limits ^{\text {def}}\bigcup _{\varvec{v} \in V} {\uparrow }\varvec{v}\). Due to \(\mathbb {N}^P\) being wellquasiordered by \(\le \), any upwardclosed set V contains a finite set \(F \subseteq V\) such that \(V = {\uparrow }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 \subseteq V\) that is minimal with respect to inclusion for all bases \(F \subseteq V\). We denote \( minbase (F)\) this minimal basis obtained by deleting vectors \(\varvec{v}\in F\) such that there exists \(\varvec{w}\in F\) with \(\varvec{w}<\varvec{v}\) (when F is finite).
3 Deciding Coverability and \(\mathbb {Q}\)Reachability
We now introduce and discuss existing algorithms for solving coverability and \(\mathbb {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 \(\mathcal {S}= (\mathcal {N}, \varvec{m}_0)\) with \(\mathcal {N}= (P, T, \mathbf {Pre}, \mathbf {Post})\), and some marking \(\varvec{m}\) to be covered or \(\mathbb {Q}\)reached.
3.1 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 kth iteration, M is the minimal basis of the (upward closed) set of markings that can cover \(\varvec{m}\) after a firing sequence of length at most k. If \(\varvec{m}_0 \in {\uparrow }M\), the algorithm returns true, i.e., that \(\varvec{m}\) is coverable. Otherwise, in order to update M, for all \(\varvec{m}' \in M\) and \(t \in T\) it computes \(\varvec{m}'_t(p) \mathop {=}\limits ^{\text {def}}\max \{\mathbf {Pre}(p, t),\ \varvec{m}'(p)  \mathbf {C}(p, t)\}\). The singleton \(\{\varvec{m}'_t\}\) is the minimal basis of the set of vectors that can cover \(\varvec{m}'\) after firing t.

Thus defining pb(M) as \( pb (M) \mathop {=}\limits ^{\text {def}}\bigcup _{\varvec{m'} \in M, t \in T} \{\varvec{m}_t'\}\), \(M\cup pb(M)\) is a (not necessarily minimal) basis of the upward closed set of markings that can cover \(\varvec{m}\) after a firing sequence of length at most \(k+1\). This basis can be then minimized in every iteration.
The termination of the algorithm is guaranteed due to \(\mathbb {N}^P\) being wellquasiordered, which entails that M must stabilize and return false in this case. It can be shown that Algorithm 1 runs in 2EXP [3]. 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 doublyexponential lower bound on the cardinality of M during the execution of the algorithm, in general not every element in M is coverable, even when \(\varvec{m}\) is coverable.
3.2 The \(\mathbb {Q}\)Reachability Algorithm
Proposition 4
 (i)
\(\varvec{m} = \varvec{m}_0 + \mathbf {C} \cdot \varvec{x}\)
 (ii)
\(\llbracket \varvec{x} \rrbracket \in { fs }(\mathcal {N}, \varvec{m}_0)\)
 (iii)
\(\llbracket \varvec{x} \rrbracket \in { fs }(\mathcal {N}^{1}, \varvec{m})\)
4 Backward Coverability Modulo \(\mathbb {Q}\)Reachability
We now present our decision algorithm for the Petri net coverability problem.
4.1 Encoding \(\mathbb {Q}\)Reachability into Existential FO(\(\mathbb {Q}_{+},+,>\))
Throughout this section, when used in formulas, \(\varvec{w}\) and \(\varvec{x}\) are vectors of firstorder variables indexed by P representing markings, and \(\varvec{y}\) is a vector of firstorder variables indexed by T representing the \(\mathbb {Q}\)Parikh image of a transition sequence.
Proposition 5
Let \(\mathcal {S}=(\mathcal {N}, \varvec{m}_0)\) be a Petri net system and \(\varvec{m}\) be a marking. There exists an existential \(\text {FO}(\mathbb {Q}_{+},+,>)\)formula \(\varPhi _\mathcal {S}(\varvec{w}, \varvec{x})\) computable in linear time such that \(\varvec{m}\) is \(\mathbb {Q}\)reachable in \(\mathcal {S}\) if and only if \(\varPhi _\mathcal {S}(\varvec{m}_0,\varvec{m})\) is valid.
Checking satisfiability of \(\varPhi _\mathcal {S}\) is in NP, see e.g. [26]. It is a valid question to ask why one would prefer an NPalgorithm over a polynomialtime one. We address this question in the next section. For now, note that in order to obtain an even more accurate overapproximation, we can additionally restrict \(\varvec{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 \(\mathcal {S}\) then there exists some \(\varvec{y}\in \mathbb {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 [14]. Given two Petri net systems \(\mathcal {S}=(\mathcal {N}, \varvec{m}_0)\) and \(\mathcal {S}'=(\mathcal {N}', \varvec{m}_0')\) over the same set of places, this problem asks whether the set of reachable markings of \(\mathcal {S}\) is included in \(\mathcal {S}'\), i.e., whether \(\forall \varvec{m}.\varPhi _{\mathcal {S}} (\varvec{m}_0,\varvec{m}) \rightarrow \varPhi _{\mathcal {S}'}(\varvec{m}_0',\varvec{m})\) is valid. The latter is a \(\varPi _2\)sentence of \(\text {FO}(\mathbb {Q}_{+},+,>)\) and decidable in \(\mathsf {\varPi _2^{P}}\) [26]. Hence, inclusion between continuous Petri nets is in \(\mathsf {\varPi _2^{P}}\).
4.2 The Coverability Decision Procedure
First, on Line 1 we derive an open formula \(\varPhi (\varvec{x})\) from \(\varPhi _\mathcal {S}\) such that \(\varPhi (\varvec{x})\) holds if and only if \(\varvec{x}\) is \(\mathbb {Q}\)coverable in \(\mathcal {S}\). Then, on Line 2, the algorithm checks whether the marking \(\varvec{m}\) is \(\mathbb {Q}\)coverable using the polynomialtime algorithm from [14] and returns that \(\varvec{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 \(\varvec{m}\) whose elements are in addition \(\mathbb {Q}\)coverable in \(\mathcal {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 \(\mathbb {Q}\)coverable. If as a result B is empty the algorithm concludes that \(\varvec{m}\) is not coverable in \(\mathcal {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 \({\uparrow }D\). The latter is technically not necessary, but it provides some guidance to the SMT solver. The proof of the following proposition can be found in [2].
Proposition 7
Let \(\mathcal {S}= (\mathcal {N}, \varvec{m}_0)\) be a PNS and \(\varvec{m}\) be a marking. Then \(\varvec{m}\) is coverable in \(\mathcal {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 \cup B)\) in Line 11 is replaced by \(M := minbase (M \cup { min }_{c,k} B)\). Here, \(c,k\in \mathbb {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 sumnorm. In this way, the empirically chosen parameters c and k create a bottleneck that gives priority to elements with small sumnorms, as they are more likely to allow for discarding elements with larger sumnorms 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 \({\uparrow }{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 \(\varPhi _\mathcal {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 \(\mathcal {S}\) is not \(\mathbb {Q}\)coverable, and thereafter only employ \(\varPhi _\mathcal {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 \(\mathbb {Q}\)coverability query. Otherwise, as soon \(\varPhi _\mathcal {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 \(\mathbb {N}\) instead of \(\mathbb {Q}\), leading to a more precise over approximation.
4.3 Relationship to the CEGARapproach of Esparza Et Al
In [10], Esparza et al. presented a semidecision procedure for coverability that is based on [11] and employs the Petri net state equation and traps inside a CEGARframework. A trap in \(\mathcal {N}\) is a nonempty subset of places \(Q\subseteq P\) such that \({Q^\bullet } \subseteq {^\bullet Q}\), and \(Q\subseteq P\) is a siphon in \(\mathcal {N}\) whenever \({^\bullet Q} \subseteq {Q^\bullet }\). Given a marking \(\varvec{m}\), a trap (respectively siphon) is marked in \(\varvec{m}\) if \(\sum _{p\in Q} \varvec{m}(p)>0\). An important property of traps is that if a trap is marked in \(\varvec{m}\), it will remain marked after any firing sequence starting in \(\varvec{m}\). Conversely, when a siphon is unmarked in \(\varvec{m}\) it remains so after any firing sequence starting in \(\varvec{m}\). By definition, Q is a trap in \(\mathcal {N}\) if and only if Q is a siphon in \(\mathcal {N}^{1}\). The coverability criteria that [10] builds upon are derived from [11] and can be summarized as follows.
Proposition 9
 (i)
\(\varvec{m} = \varvec{m}_0 + \mathbf {C} \cdot \varvec{x}\)
 (ii)
for all traps \(Q\subseteq P\), if Q is marked in \(\varvec{m}_0\) then Q is marked in \(\varvec{m}\)
Proposition 10
Conditions (i) and (iii) of Proposition 4 strictly imply Conditions (i) and (ii) of Proposition 9 (when interpreted over \(\mathbb {Q}_{+}\)).
Proof
We only show strictness, the full proof can be found in [2]. To this end, consider the Petri net \((\mathcal {N},\varvec{m}_0)\) depicted in Fig. 1 with \(\varvec{m}=(0,1)\). Clearly \(\varvec{m}\) is not reachable. There is a single solution to the state equation \(\varvec{x}=(1,0)\). There is a single trap \(\{p_1\}\) which is unmarked in \(\varvec{m}_0\). So the conditions of Proposition 9 hold, and hence the algorithm of [10] does not decide this net safe. On the contrary in \(\mathcal {N}_{\llbracket \varvec{x} \rrbracket }^{1}\), the reverse net without \(t_2\), \(\{p_0\}\) is a siphon that is unmarked in \(\varvec{m}\). So Condition (iii) of Proposition 4 does not hold. \(\square \)
This proposition shows that the single formula stated in Proposition 5 strictly subsumes the approach from [10]. Moreover, it provides a theoretical justification for why the approach of [10] performs so well in practice: the conditions are a strict subset of the conditions developed for \(\mathbb {Q}\)reachability in [14].
5 Experimental Evaluation
We implemented Algorithm 3 in a tool called QCover in the programming language Python.^{4} The underlying SMTsolver is z3 [6]. 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 speedup, though different values lead to different (even increasing) running times on individual instances. QCover takes as input coverability instances in the mist file format.^{5} The basis of our evaluation is the benchmark suite that was used in order to evaluate the tool Petrinizer, see [10] 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 bugtracking system, respectively; and soter, consisting of 50 instances of verification conditions derived from Erlang programs [9].
We compare QCover with the following tools: Petrinizer [10], mist [15] and bfc [20] 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 [16].^{6} All benchmarks were performed on a single computer equipped with four Intel® Core™ 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 s (i.e. 33 min and 20 s) 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.
Finally, we consider the effectiveness of using \(\mathbb {Q}\)coverability as a pruning criterion. To this end, consider Fig. 4 in which we plotted the number of times a certain percentage of basis elements was removed due to not being \(\mathbb {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 \(\mathbb {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(\(\mathbb {Q}_{+},+,>\)) encoding then we can only decide 132 instances in total. Finally, in our experiments, interpreting variables over \(\mathbb {Q}\) instead of \(\mathbb {N}\) resulted in no measurable overall performance gain.
In summary, our experimental evaluation shows that the backward coverability modulo \(\mathbb {Q}\)reachability approach to the Petri net coverability problem developed in this paper is highly efficient when run on realworld instances, and superior to existing tools and approaches when compared on standard benchmarks from the literature.
6 Conclusion
In this paper, we introduced backward coverability modulo \(\mathbb {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(\(\mathbb {Q}_{+},+,>\))characterization of continuous reachability, which we showed to strictly subsume a recently introduced coverability semidecision procedure [10]. 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 KarpMiller tree that is used in BFC [20] with the \(\mathbb {Q}\)coverability approach introduced in this paper. In particular, recently developed minimization and acceleration techniques for constructing KarpMiller trees should prove beneficial, see e.g. [18, 25, 27]. Another way to improve the empirical performance of our algorithm is to internally use more efficient data structures such as sharing trees [8]. 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.
Footnotes
 1.
This problem is commonly referred to as the symbolic state explosion problem, cf. [8].
 2.
In fact, the original definition allows for real numbers, however for studying decidability and complexity issues, rational numbers are more convenient.
 3.
In [14, Corollary 19], an algorithm is presented that basically computes \({{\mathrm{lfp}}}({ incfs }_{\mathcal {N}_{T'}, \varvec{w}})\).
 4.
QCover is available at http://wwwetud.iro.umontreal.ca/~blondimi/qcover/.
 5.
 6.
Notes
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.
References
 1.Cerans, K., Jonsson, B., Tsay, Y.K.: Algorithmic analysis of programs with well quasiordered domains. Inf. Comput. 160(1–2), 109–127 (2000)MathSciNetzbMATHGoogle Scholar
 2.Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously (2015). CoRR, abs/1510.05724
 3.Bozzelli, L., Ganty, P.: Complexity analysis of the backward coverability algorithm for VASS. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 96–109. Springer, Heidelberg (2011)CrossRefGoogle Scholar
 4.Cardoza, E., Lipton, R.J., Meyer, A.R.: Exponential space complete problems for Petri nets, commutative semigroups: preliminary report. In: Symposium on Theory of Computing, STOC, pp. 50–54 (1976)Google Scholar
 5.David, R., Alla, H.: Continuous Petri nets. In: Proceedings of the 8th European Workshop on Application and Theory of Petri nets, pp. 275–294 (1987)Google Scholar
 6.de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
 7.Delzanno, G., Raskin, J.F., Van Begin, L.: Attacking symbolic state explosion. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 298. Springer, Heidelberg (2001)CrossRefGoogle Scholar
 8.Delzanno, G., Raskin, J.F., Van Begin, L.: Covering sharing trees: a compact data structure for parameterized verification. STTT 5(2–3), 268–297 (2004)CrossRefGoogle Scholar
 9.D’Osualdo, E., Kochems, J., Ong, C.H.L.: Automatic verification of erlangstyle concurrency. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 454–476. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 10.Esparza, J., LedesmaGarza, R., Majumdar, R., Meyer, P., Niksic, F.: An SMTbased approach to coverability analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 603–619. Springer, Heidelberg (2014)Google Scholar
 11.Esparza, J., Melzer, S.: Verification of safety properties using integer programming: beyond the state equation. Formal Meth. Syst. Des. 16(2), 159–189 (2000)CrossRefGoogle Scholar
 12.Finkel, A., Raskin, J.F., Samuelides, M., Van Begin, L.: Monotonic extensions of Petri nets: forward and backward search revisited. Electr. Notes Theor. Comput. Sci. 68(6), 85–106 (2002)CrossRefzbMATHGoogle Scholar
 13.Finkel, A., Schnoebelen, P.: Wellstructured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
 14.Fraca, E., Haddad, S.: Complexity analysis of continuous Petri nets. Fundam. Informaticae 137(1), 1–28 (2015)MathSciNetzbMATHGoogle Scholar
 15.Ganty, P.: Algorithmes et structures de données efficaces pour la manipulation de contraintes sur les intervalles (in French). Master’s thesis, Université Libre de Bruxelles, Belgium (2002)Google Scholar
 16.Ganty, P., Meuter, C., Delzanno, G., Kalyon, G., Raskin, J.F., Van Begin, L.: Symbolic data structure for sets of \(k\)uples. Technical report 570, Université Libre de Bruxelles, Belgium (2007)Google Scholar
 17.Geeraerts, G., Raskin, J.F., Van Begin, L.: Expand, enlarge and check: new algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180–203 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
 18.Geeraerts, G., Raskin, J.F., Van Begin, L.: On the efficient computation of the minimal coverability set of petri nets. Int. J. Found. Comput. Sci. 21(2), 135–165 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
 19.German, S.M., Prasad Sistla, A.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
 20.Kaiser, A., Kroening, D., Wahl, T.: A widening approach to multithreaded program verification. ACM Trans. Program. Lang. Syst. 36(4), 1–29 (2014)CrossRefGoogle Scholar
 21.Karp, R.M., Miller, R.E.: Parallel program schemata: a mathematical model for parallel computation. In Switching and Automata Theory, pp. 55–61. IEEE Computer Society (1967)Google Scholar
 22.Kloos, J., Majumdar, R., Niksic, F., Piskac, R.: Incremental, inductive coverability. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 158–173. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 23.Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: Logic in Computer Science, LICS, pp. 56–67. IEEE (2015)Google Scholar
 24.Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223–231 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
 25.Reynier, P.A., Servais, F.: Minimal coverability set for petri nets: karp and miller algorithm with pruning. Fundam. Inform. 122(1–2), 1–30 (2013)MathSciNetzbMATHGoogle Scholar
 26.Sontag, E.D.: Real addition and the polynomial hierarchy. Inf. Process. Lett. 20(3), 115–120 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
 27.Valmari, A., Hansen, H.: Old and new algorithms for minimal coverability sets. Fundam. Inform. 131(1), 1–25 (2014)MathSciNetzbMATHGoogle Scholar
 28.Verma, K.N., Seidl, H., Schwentick, T.: On the complexity of equational horn clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 337–352. Springer, Heidelberg (2005)CrossRefGoogle Scholar