Approaching the Coverability Problem Continuously

Abstract

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 backward-coverability 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.

M. Blondin—Supported by the Fonds québécois de la recherche sur la nature et les technologies (FQRNT), by the French Centre national de la recherche scientifique (CNRS), and by the “Chaire Digiteo, ENS Cachan — École Polytechnique”.

C. Haase—Supported by Labex Digicosme, Univ. Paris-Saclay, project VERICONISS.

S. Haddad—Supported by ERC project EQualIS (FP7-308087).

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 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 [19] 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 EXPSPACE-complete [4, 21, 24]. 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 [14], Fraca and Haddad solved long-standing open problems about the complexity of decision problems for so-called continuous Petri nets. This class was introduced by David and Alla [5] 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 [14] was to present polynomial-time 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 non-negative rational numbers with addition and order (FO($\mathbb {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 [10]; 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 [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 well-structured 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.¹ 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 semi-decision procedure for disproving coverability which was originally proposed by Esparza and Melzer [11]. It is based on the Petri-net state equation and traps as sufficient criteria in order to witness non-coverability. As shown in [11], those conditions can be encoded into an equi-satisfiable 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 CEGAR-based 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 SMT-solver. 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 CEGAR-approach 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 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 over-approximate 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 Karp-Miller tree is incrementally built in the approach described in [20], 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. [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 well-structured 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 non-negative 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 component-wise, 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'}$ sub-matrix 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 pre-sets 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 post-sets 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 sub-net 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})$.

We say that a transition $t \in T$ is enabled at a marking $\varvec{m}$ whenever $\varvec{m}(p) \ge \mathbf {Pre}(p, t)$ for every $p \in {^\bullet t}$. A transition t that is enabled can be fired, leading to a new marking $\varvec{m}'$ such that for all places $p \in P$, $\varvec{m}'(p) = \varvec{m}(p) + \mathbf {C}(p, t)$. We write $\varvec{m} \xrightarrow {t} \varvec{m}'$ whenever t is enabled at $\varvec{m}$ leading to $\varvec{m}'$, and write $\varvec{m} \xrightarrow {} \varvec{m}'$ if $\varvec{m} \xrightarrow {t} \varvec{m}'$ for some $t \in T$. By $\xrightarrow {}^*$ we denote the reflexive transitive closure of $\xrightarrow {}$. A word $\sigma = t_1 t_2 \cdots t_k \in T^*$ is a firing sequence of $(\mathcal {N}, \varvec{m}_0)$ whenever there exist markings $\varvec{m}_1, \ldots , \varvec{m}_k$ such that

$$\begin{aligned} \varvec{m}_0 \xrightarrow {t_1} \varvec{m}_1 \xrightarrow {t_2} \cdots \xrightarrow {t_{k-1}} \varvec{m}_{k-1} \xrightarrow {t_k} \varvec{m}_k. \end{aligned}$$

Given a marking $\varvec{m}$, the reachability problem asks whether $\varvec{m}_0 \xrightarrow {}^* \varvec{m}$. The reachability problem is decidable, EXPSPACE-hard [4] and in $\mathbf{F}_{\omega ^3}$ [23], a non-primitive-recursive complexity class. In this paper, however, we are interested in deciding coverability, an EXPSPACE-complete problem [4, 24].

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}$.

Continuous Petri nets are Petri nets in which markings may consist of rational numbers², and in which transitions may be fired a fractional number of times. Formally, a marking of a continuous Petri net is a vector $\varvec{m}\in \mathbb {Q}_{+}^P$. Let $t \in T$, the enabling degree of t with respect to $\varvec{m}$ is a function $enab (t,\varvec{m}) \in \mathbb {Q}_{+}\cup \{\infty \}$ defined by:

$$\begin{aligned} enab (t,\varvec{m}) \mathop {=}\limits ^{\text {def}}{\left\{ \begin{array}{ll} \min \{\varvec{m}(p) / \mathbf {Pre}(p,t) : p \in {^\bullet t}\} &{} \text {if } {^\bullet t} \ne \emptyset , \\ \infty &{} \text {otherwise.} \end{array}\right. } \end{aligned}$$

We say that t is $\mathbb {Q}$ -enabled at $\varvec{m}$ if $enab (t,\varvec{m}) > 0$. If t is $\mathbb {Q}$-enabled it may be fired by any amount $q \in \mathbb {Q}_{+}$ such that $0 \le q \le enab (t,\varvec{m})$, leading to a new marking $\varvec{m}'$ such that for all places $p \in P$, $\varvec{m}(p)' \mathop {=}\limits ^{\text {def}}\varvec{m}(p) + q \cdot \mathbf {C}(p,t)$. In this case, we write $\varvec{m} \xrightarrow {q \cdot t} \varvec{m}'$. The definition of a $\mathbb {Q}$ -firing sequence $\sigma = q_1t_1 \cdots q_kt_k \in (\mathbb {Q}_{+}\times T)^*$ is analogous to the standard definition of firing sequence, and so are $\xrightarrow {}_\mathbb {Q}$, $\xrightarrow {}^{*}_{\mathbb {Q}}$ and $\mathbb {Q}$-reachability. The $\mathbb {Q}$ -Parikh image of the firing sequence $\sigma$ is the vector ${\pi }(\sigma )\in \mathbb {Q}_{+}^T$ such that ${\pi }(\sigma )(t) \mathop {=}\limits ^{\text {def}}\sum _{t_i=t} q_i$. We also adapt the decision problems for Petri nets.

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 over-approximation 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 well-quasi-ordered by $\le$, any upward-closed 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 upward-closed 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 k-th 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 well-quasi-ordered, which entails that M must stabilize and return false in this case. It can be shown that Algorithm 1 runs in 2-EXP [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 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 $\varvec{m}$ is coverable.

3.2 The $\mathbb {Q}$-Reachability Algorithm

We now present the fundamental concepts of the polynomial-time $\mathbb {Q}$-reachability algorithm of Fraca and Haddad [14]. The key insight underlying their algorithm is that $\mathbb {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 }(\mathcal {N}, \varvec{m})$ and $maxfs (\mathcal {N},\varvec{m})$, and defined as follows:

$$\begin{aligned} { fs }(\mathcal {N},\varvec{m})&\mathop {=}\limits ^{\text {def}}\ \{\llbracket {\pi }(\sigma ) \rrbracket : \sigma \in (\mathbb {Q}_{+}\times T)^*,\ \text {there is } \varvec{m}' \in \mathbb {Q}_{+}^P \text { s.t. } \varvec{m} \xrightarrow {\sigma }_\mathbb {Q}\varvec{m}'\} \\ maxfs (\mathcal {N},\varvec{m})&\mathop {=}\limits ^{\text {def}}\ \bigcup _{T'\in { fs }(\mathcal {N}, \varvec{m})} T'. \end{aligned}$$

Thus, ${ fs }(\mathcal {N}, \varvec{m})$ is the set of supports of firing sequences starting in $\varvec{m}$. Even though ${ fs }(\mathcal {N}, \varvec{m})$ can be of size exponential with respect to $|T |$, deciding $T' \in { fs }(\mathcal {N}, \varvec{m})$ for some $T' \subseteq T$ can be done in polynomial time, and $maxfs (\mathcal {N},\varvec{m})$ is also computable in polynomial time [14]. The following proposition characterizes the set of $\mathbb {Q}$-reachable markings.

Proposition 4

([14, Theorem 20]). A marking $\varvec{m}$ is $\mathbb {Q}$-reachable in $\mathcal {S}= (\mathcal {N}, \varvec{m}_0)$ if and only if there exists $\varvec{x} \in \mathbb {Q}_{+}^T$ such that

• (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})$

In this characterization, $\varvec{x}$ is supposed to be the Parikh image of a firing sequence. The first item expresses the state equation of $\mathcal {S}$ with respect to $\varvec{m}_0$, $\varvec{m}$ and $\varvec{x}$. The two subsequent items express that the support of the solution of the state equation has to lie in the firing sets of $\mathcal {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 [14], turns those criteria into a polynomial-time algorithm (see [14] 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 $\mathcal {N}$ that can at any time non-deterministically decrease p by one token. Denote the resulting Petri net system by $\mathcal {S}'$, it can easily checked that $\varvec{m}$ is $\mathbb {Q}$-coverable in $\mathcal {S}$ if and only if $\varvec{m}$ is $\mathbb {Q}$-reachable in $\mathcal {S}'$.

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 first-order variables indexed by P representing markings, and $\varvec{y}$ is a vector of first-order variables indexed by T representing the $\mathbb {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 $\varPhi (\varvec{w}, \varvec{x},\varvec{y})$ which holds whenever a marking $\varvec{x}$ is reached starting at marking $\varvec{w}$ by firing every transition $\varvec{y}(t)$ times (without any consideration whether such a firing sequence would actually be admissible):

$$\begin{aligned} \varPhi _{ eqn }^{\mathcal {N}}(\varvec{w}, \varvec{x}, \varvec{y}) \mathop {=}\limits ^{\text {def}}\varvec{x} = \mathbf {C} \cdot \varvec{y} + \varvec{w}. \end{aligned}$$

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 }(\mathcal {N}, \varvec{w})$ defined in Sect. 3.2. The following characterization can be derived from [14, Corollary 19]. First, we define a monotonic increasing function ${ incfs }_{\mathcal {N}, \varvec{w}} : 2^T \rightarrow 2^T$ as follows:

$$\begin{aligned} { incfs }_{\mathcal {N}, \varvec{w}}(S) \mathop {=}\limits ^{\text {def}}S \cup \left\{ t \in T(\mathcal {N}) : {^\bullet t} \subseteq \llbracket \varvec{w} \rrbracket \cup \{ {s^\bullet } : s\in S\} \right\} . \end{aligned}$$

From [14, Corollary 19], it follows that $T'\in { fs }(\mathcal {N},\varvec{w})$ if and only if $T' = {{\mathrm{lfp}}}({ incfs }_{\mathcal {N}_{T'}, \varvec{w}})$, where ${{\mathrm{lfp}}}$ is the least fixed point operator³, i.e.,

$$\begin{aligned} T' = { incfs }_{\mathcal {N}_{T'}, \varvec{w}}(\cdots ({ incfs }_{\mathcal {N}_{T'}, \varvec{w}}(\emptyset ))\cdots ). \end{aligned}$$

Clearly, the least fixed point is reached after at most $|T' |$ iterations.

In order to decide whether $\llbracket \varvec{y} \rrbracket \in { fs }(\mathcal {N},\varvec{w})$, we simulate this fixed-point computation in an existential FO($\mathbb {Q}_{+},+,>$)-formula $\varPhi _{{ fs }}^\mathcal {N}(\varvec{w},\varvec{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 [28]. The basic idea is to introduce additional first-order variables $\varvec{z}$ indexed by $P\cup 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 ${{\mathrm{lfp}}}({ incfs }_{\mathcal {N}_{\llbracket \varvec{y} \rrbracket },\varvec{w}})$ and is encoded via a numerical value $\varvec{z}(t)$ (respectively $\varvec{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:

$$\begin{aligned} \varPhi _{ dt }^\mathcal {N}(\varvec{y}, \varvec{z}) \mathop {=}\limits ^{\text {def}}\bigwedge _{t\in T}\left( \varvec{y}(t) > 0 \rightarrow \bigwedge _{p\in {{^\bullet t}}} 0<\varvec{z}(p) \le \varvec{z}(t)\right) . \end{aligned}$$

Moreover, a place is either initially marked or after the firing of a transition of the firing set. So:

$$\begin{aligned} \varPhi _{ mk }^{\mathcal {N}} (\varvec{w},\varvec{y}, \varvec{z}) \mathop {=}\limits ^{\text {def}}\bigwedge _{p\in P} \left( \varvec{z}(p)> 0 \rightarrow \left( \varvec{w}(p)> 0 \vee \bigvee _{t\in {^\bullet p}} \varvec{y}(t) > 0 \wedge \varvec{z}(t)<\varvec{z}(p) \right) \right) . \end{aligned}$$

We can now take the conjunction of the formulas above in order to obtain a logical characterization of ${ fs }(\mathcal {N},\varvec{w})$:

$$\begin{aligned} \varPhi _{ fs }^\mathcal {N}(\varvec{w},\varvec{y}) \mathop {=}\limits ^{\text {def}}\exists \varvec{z} : \varPhi _{ dt }^\mathcal {N}(\varvec{y},\varvec{z}) \wedge \varPhi _{ mk }^\mathcal {N}(\varvec{w}, \varvec{y},\varvec{z}). \end{aligned}$$

Having logically characterized all conditions of Proposition 4, we can define the global $\mathbb {Q}$-reachability relation for a Petri net system $\mathcal {S}= (\mathcal {N}, \varvec{w})$ as follows:

$$\begin{aligned} \varPhi _{\mathcal {S}}(\varvec{w}, \varvec{x}) \mathop {=}\limits ^{\text {def}}\exists \varvec{y} : \varPhi _{ eqn }^\mathcal {N}(\varvec{w},\varvec{x},\varvec{y}) \wedge \varPhi _{ fs }^\mathcal {N}(\varvec{w}, \varvec{y}) \wedge \varPhi _{ fs }^{\mathcal {N}^{-1}}(\varvec{x}, \varvec{y}). \end{aligned}$$

In summary, we have thus proved the following result in this section.

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 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 $\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

We now present Algorithm 3 for deciding coverability. This algorithm is an extension of the classical backward reachability algorithm that incorporates $\mathbb {Q}$-reachability checks during its execution in order to keep the set of minimal basis elements small.

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 polynomial-time 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 sum-norm. 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 ${\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 CEGAR-approach of Esparza Et Al

In [10], Esparza et al. presented a semi-decision procedure for coverability that is based on [11] and employs the Petri net state equation and traps inside a CEGAR-framework. A trap in $\mathcal {N}$ is a non-empty 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

([10]). If $\varvec{m}$ is $\mathbb {Q}$-reachable (respectively reachable) in $(\mathcal {N},\varvec{m}_0)$ then there exists $\varvec{x} \in \mathbb {Q}_{+}^T$ (respectively $\varvec{x} \in \mathbb {N}^T$) such that:

• (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}$

As in our approach, in [10] those criteria are checked using an SMT-solver. The for-all quantifier is replaced in [10] by incrementally enumerating all traps in a CEGAR-style fashion. It is shown in [14, Proposition 18] that Condition (iii) of Proposition 4 is equivalent to requiring that $\mathcal {N}_{\llbracket \varvec{x} \rrbracket }^{-1}$ has no unmarked siphon in $\varvec{m}$, which appears to be similar to Condition (ii) of Proposition 9. In fact, we show the following.

Fig. 1.

A Petri net that cannot mark $p_1$.

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 evaluate the backward coverability modulo $\mathbb {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 $\mathbb {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.

Fig. 2.

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.

We implemented Algorithm 3 in a tool called QCover in the programming language Python.⁴ The underlying SMT-solver 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 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.⁵ 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 bug-tracking 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].⁶ 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.

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 $\mathbb {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.

Fig. 3.

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

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 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.

Fig. 4.

Number of times a certain percentage of basis elements was removed due to $\mathbb {Q}$-coverability pruning.

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 real-world 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 semi-decision 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 Karp-Miller 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 Karp-Miller 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.