key: cord-0060414-5th04g85 authors: Blondin, Michael; Haase, Christoph; Offtermatt, Philip title: Directed Reachability for Infinite-State Systems date: 2021-02-26 journal: Tools and Algorithms for the Construction and Analysis of Systems DOI: 10.1007/978-3-030-72013-1_1 sha: 426cd6bb260d76199ab34f06cc75c72d5b75a685 doc_id: 60414 cord_uid: 5th04g85 Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as [Formula: see text] and greedy best-first search. We provide and evaluate a prototype implementation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis. Many problems in program analysis, synthesis and verification reduce to deciding reachability of a vertex or a set of vertices in infinite graphs, e.g., when reasoning about concurrent programs with an unbounded number of threads, or when arbitrarily many components can be used in a synthesis task. For automated reasoning tasks, those infinite graphs are finitely represented by some mathematical model. Finding the right such model requires a trade-off between the two conflicting goals of maximal expressive power and computational feasibility of the relevant decision problems. Petri nets are a ubiquitous mathematical model that provides a good compromise between those two goals. They are expressive enough to find a plethora of applications in computer science, in particular in the analysis of concurrent processes, yet the reachability problem for Petri nets is decidable [47, 40, 41, 43] . Counter abstraction has evolved as a generic abstraction paradigm that reduces a variety of program analysis tasks to problems in Petri nets or variants thereof such as well-structured transition systems, see e.g. [30, 39, 61, 5] . Due to their generality and versatility, Petri nets and their extensions find numerous applications also in other areas, including the design and analysis of protocols [22] , business processes [57], biological systems [33, 11] and chemical systems [2] . The goal of this paper is to introduce and evaluate an efficient generic approach to deciding the Petri net reachability problem on instances arising from applications in program verification and synthesis. A Petri net comprises a finite set of places with a finite number of transitions. Places carry a finite yet unbounded number of tokens and transitions can remove and add tokens to places. A marking specifies how many tokens each place carries. An example of a Petri net is given on the left-hand side of Figure 1 , where the two places {p 1 , p 2 } are depicted as circles and transitions {t 1 , t 2 , t 3 } as squares. Places carry tokens depicted as filled circles; thus p 1 carries one token and p 2 carries none. We write this as [p 1 : 1, p 2 : 0], or (1, 0) if there is a clear ordering on the places. Transition t 1 can add a single token to place p 1 at any moment. As soon as a token is present in p 1 , it can be consumed by transition t 2 , which then adds a token to place p 2 and puts back one token to place p 1 . Finally, transition t 3 consumes tokens from p 1 without adding any token at all. A Petri net induces a possibly infinite directed graph whose vertices are markings, and whose edges are determined by the transitions of the Petri net, cf. the right side of Figure 1 . Given two markings, the reachability problem asks whether they are connected in this graph. In Figure 1 , the marking (0, 1) is reachable from (0, 0), e.g., via paths of lengths 3 and 5: (0, 0) In practice, the Petri net reachability problem is a challenging decision problem due to its horrendous worst-case complexity: an exponential-space lower bound was established in the 1970s [45] , and a non-elementary time lower bound has only recently been established [13] . One may thus question whether a problem with such high worst-case complexity is of any practical relevance, and whether reducing program analysis tasks to Petri net reachability is anything else than merely an intellectual exercise. We debunk those concerns and present a technique which decides most reachability instances appearing in the wild. When evaluated on large-scale instances involving Petri nets with thousands of places and tens of thousands of transitions, our prototype implementation is most of the time faster, even up to several orders of magnitude on large-scale instances, and solves more instances than existing state-of-the-art tools. Our implementation is also competitive with specialized domain-specific tools. One of the biggest advantages of our approach is that it is extremely simple to describe and implement, and it readily generalizes to many extensions of Petri nets. In fact, it was surprising to us that our approach has not yet been discovered. We now describe the main observations and techniques underlying our approach. Ever since the early days of research in Petri nets, state-space over-approximations have been studied to attenuate the high computational complexity of their decision problems. One such over-approximation is, informally speaking, to allow places to carry a negative number of tokens. Deciding reachability then reduces to solving the so-called state equation, a system of linear equations associated to a Petri net. Another over-approximation are continuous Petri nets, a variant where places carry fractional tokens and "fractions of transitions" can be applied [14] . The benefit is that deciding reachability drops down to polynomial time [25] . While those approximations have been applied for pruning search spaces, see e.g. [23, 4, 8, 29] , we make the following simple key observation: If a marking m is reachable from an initial marking in an overapproximation, then the length of a shortest witnessing path in the overapproximation lower bounds the length of a shortest path reaching m. The availability of an oracle providing lower bounds on the length of shortest paths between markings enables us to appeal to classical graph traversal algorithms which have been highly successful in artificial intelligence and require such oracles, namely A * and greedy best-first search, see e.g. [52] . In particular, determining the length of shortest paths in the over-approximations described above can be phrased as optimization problems in (integer) linear programming and optimization modulo theories, for which efficient off-the-shelf solvers are available [32, 7] . Thus, oracle calls can be made at comparably modest computational cost, which is crucial for the applicability of those algorithms. As a result, a large class of existing state-space over-approximations can be applied to obtain a highly efficient forward-analysis semi-decision procedure for the reachability problem. For example, in Figure 1 , using the state equation as distance oracle, A * only explores the four vertices in the blue region and directly reaches the target vertex, whereas a breadth-first search may need to explore all vertices of the figure and a depth-first search may even not terminate. In theory, our approach could be turned into a decision procedure by applying bounds on the length of shortest paths in Petri nets [44] . However, such lengths can grow non-elementarily in the number of places [13] , and just computing the cut-off length will already be infeasible for any Petri net of practical relevance. It is worth mentioning that, in practice, it has been observed that the over-approximations we employ also often witness non-reachability though, see e.g. [23] . Still, when dealing with finite state spaces, our procedure is complete. A noteworthy benefit of our approach is that it enables finding shortest paths when A * is used as the underlying algorithm. In program analysis, paths usually correspond to traces reaching an erroneous configuration. In this setting, shorter error traces are preferred as they help understanding why a certain error occurs. Furthermore, in program synthesis, paths correspond to synthesis plans. Again, shorter paths are preferred as they yield shorter synthesized programs. In fact, we develop our algorithmic framework for weighted Petri nets in which transitions are weighted with positive integers. Classical Petri nets correspond to the special instance where all weights are equal to one. Weighted Petri nets are useful to reflect cost or preferences in synthesis tasks. For example, there are program synthesis approaches where software projects are mined to determine how often API methods are called to guide a procedure by preferring more frequent methods [27, 26, 46] . Similarity metrics can also be used to obtain costs estimating the relevance of invoking methods [24] . It has further been argued that weighted Petri nets are a good model for synthesis tasks of chemical reactions as they can reflect costs of various chemical compounds [58] . Finally, weights can be viewed as representing an amount of time it takes to fire a transition, see e.g. [50] . Related work. Our approach falls under the umbrella term directed model checking coined in the early 2000s, which refers to a set of techniques to tackle the state-explosion problem via guided state-space exploration. It primarily targets disproving safety properties by quickly finding a path to an error state without the need to explicitly construct the whole state space. As such, directed model checking is useful for bug-finding since, in the words of Yang and Dill [60] , in practice, model checkers are most useful when they find bugs, not when they prove a property. The survey paper [20] gives an overview over various directed model checking techniques for finite-state systems. For Petri nets, directed reachability algorithms based on over-approximations as developed in this work have not been described. In [56] , it is argued that exploration heuristics, like A * , can be useful for Petri nets, but they do not consider over-approximations for the underlying heuristic functions. The authors of [36] use Petri nets for scheduling problems and employ the state equation, viewed as a system of linear equations over Q, in order to explore and prune reachability graphs. This approach is, however, not guaranteed to discover shortest paths. There has been further work on using A * for exploring the reachability graph of Petri nets for scheduling problems, see, e.g., [42, 48] and the references therein. We naturally extend operations componentwise. In particular, (u + v)(x) := u(x) + v(x) for every x ∈ X, and u ≥ v iff u(x) ≥ v(x) for every x ∈ X. Graphs. A (labeled directed) graph is a triple G = (V, E, A), where V is a set of nodes, A is a finite set of elements called actions, and E ⊆ V × A × V is the set of edges labeled by actions. We say that G has finite out-degree if the set of outgoing edges {(w, a, w ) ∈ E : w = v} is finite for every v ∈ V . Similarly, it has finite in-degree if the set of ingoing edges is finite for every v ∈ V . If G has both finite out-and in-degree, then we say that G is locally finite. A path π is a finite sequence of nodes (v i ) 1≤i≤n and actions (a i ) 1≤i0 is the weight function assigning weights to transitions. A marking is a vector m ∈ N P which indicates that place p holds m(p) tokens. A weighted Petri net with λ(t) = 1 for each t ∈ T is called a Petri net. For example, Figure 1 The guard and effect of a transition t ∈ T are vectors g t ∈ N P and If t is firable from m, then it may be fired, which leads to marking m := m + ∆ t . We write this as m t − → N m . These notions naturally extend to sequences of transitions, i.e. ε − → N denotes the identity relation over N P , ∆ ε := 0, λ(ε) := 0, and for every t 1 , t 2 , . . . , t k ∈ T : Given a sequence σ ∈ T * , denote by |σ| t ∈ N the number of times transition t occurs in σ. The Parikh image of σ is the vector σ ∈ N T that captures the number of occurrences of transitions appearing in σ, i.e. σ(t) := |σ| t for all t ∈ T . Each weighted Petri net N = (P, T, f, λ) induces a locally finite weighted graph G N (N ) := (V, E, T, µ), called its reachability graph, where V : An example of a reachability graph is given on the right of Figure 1 and if the latter holds, then dist N (m, m ) is the minimal weight among such firing sequences σ. Moreover, for (unweighted) Petri nets, dist N (m, m ) is the minimal number of transitions to fire to reach m from m. Our approach relies on classical pathfinding procedures guided by node selection strategies. Their generic scheme is described in Algorithm 1. Its termination with a value d = ∞ indicates that the weighted graph G = (V, E, A, µ) has a path from s to t of weight d, whereas termination with d = ∞ signals that dist G (s, t) = ∞. Algorithm 1 maintains a set of frontier nodes C and a map- is the weight of the best known path from s to w. In Line 4, a selection strategy S determines which node v to expand next. Starting from Line 6, a successor w of v is added to the frontier if its distance improves. yield the classical Dijkstra's, A * and greedy best-first search (GBFS ) algorithms. When instantiating S with Dijkstra's selection strategy, a return value d = ∞ is guaranteed to equal dist G (s, t). This is not true for A * and GBFS. However, if h fulfills the following consistency properties, then A * also has this guarantee: h(t) = 0 and h(v) ≤ µ(v, a, w) + h(w) for every (v, a, w) ∈ E (see, e.g., [52] ). In the setting of infinite graphs, unlike GBFS, A * and Dijkstra's selection strategies guarantee termination if dist G (s, t) = ∞. Yet, we introduce unbounded heuristics for which termination is also guaranteed for GBFS. Note that these guarantees would vanish in the presence of zero weights. An infinite path π is a sequence of nodes (v i ) i∈N and actions (a i ) i∈N such that In other words, unboundedness forbids an infinite simple path of G to "cap" at some distance estimate b. The following technical lemma enables to prove termination of GFBS in the presence of unbounded heuristics. Lemma 1. If G is locally finite, then the following holds: 1. The set of paths of weight at most c ∈ Q ≥0 starting from node s is finite. 3. No node is expanded infinitely often by Algorithm 1. Theorem 1. Algorithm 1 with the greedy best-first search selection strategy always finds reachable targets for locally finite graphs and unbounded heuristics. Proof. First observe that Algorithm 1 satisfies this invariant: For the sake of contradiction, suppose t is never expanded. Let K i be the subgraph of G induced by nodes expanded at least once within the first i iterations of the while loop. In particular, K 1 is the graph made only of node s. Let K = K 1 ∪ K 2 ∪ · · · . By Lemma 1 (3), no node is expanded infinitely often, hence K is infinite. Moreover, K has finite out-degree, and each node of K is reachable from s in K by ( * ). Thus, by König's lemma, K contains an infinite path v 0 , v 1 , . . . ∈ V of pairwise distinct nodes. Let w be a node of K minimizing dist G (w, t). That minimum is well-defined by Lemma 1 (2). Since s ∈ K 1 ⊆ K and t is reachable from s, we have dist G (w, t) ≤ dist G (s, t) < ∞. By minimality of w = t, there exists an edge (w, a, w ) of G such that dist G (w , t) < dist G (w, t) and w does not appear in K. Note that w is added to C at some point, but is never expanded as it would otherwise belong to K. Let i be the smallest index such that w belongs to K i . Since h is unbounded, there exists j such that h(v j ) > h(w ) and v j is expanded after iteration i of the while loop. This is a contradiction as w would have been expanded instead of v j . In this section, we explain how to instantiate Algorithm 1 for finding short(est) firing sequences witnessing reachability in weighted Petri nets. Since Dijkstra's selection strategy does not require any heuristic, we focus on A * and greedy bestfirst search which require consistent and unbounded heuristics. More precisely, we introduce distance under-approximations (Section 4.1); present relevant concrete distance under-approximations (Section 4.2); and put everything together into our framework (Section 4.3). A distance under-approximation of a weighted Petri net N = (P, T, f, λ) is a function d : N P × N P → Q ≥0 ∪ {∞} such that for all m, m , m ∈ N P : there is an algorithm that evaluates d on all inputs. We naturally obtain a heuristic from d for a directed search towards marking m target . Indeed, let h : The following proposition shows that h is a suitable heuristic for A * : Proof. Let m, m ∈ N P and t ∈ T be such that m t − → N m . We have: where the last equality follows from the fact that weights are positive. We now introduce classical relaxations of Petri nets which over-approximate reachability and consequently give rise to distance under-approximations. The main source of hardness of the reachability problem stems from the fact that places are required to hold a non-negative number of tokens. If we relax this requirement and allow negative numbers of tokens, we obtain a more tractable relation. More precisely, we write m t − → Z m iff m = m+∆ t . Note that transitions are always firable under this semantics. Moreover, they may lead to "markings" with negative components. Another source of hardness comes from the fact that markings are discrete. Hence, we can further relax − → Z into − → Q where transitions may be scaled down: One gets a less crude relaxation from considering nonnegative "markings" only: Under these, we obtain "markings" from Q P and Q P ≥0 respectively. Petri nets equipped with relation − → Q ≥0 are known as continuous Petri nets [14, 15] . To unify all three relaxations, we sometimes write m δt − → G m to emphasize the scaling factor δ, where δ = 1 whenever G = Z. Let d G : N P ×N P → Q ≥0 ∪{∞} be defined as d G (m, m ) := ∞ if m * − → G m , and otherwise: In words, d G (m, m ) is the weight of a shortest path from m to m in the graph induced by the relaxed step relation − → G , where weights are scaled accordingly. We now show that any d G , which we call the G-distance, is a distance underapproximation, and first show effectiveness of all d G . It is well-known and readily seen that reachability over G ∈ {Z, Q} is characterized by the following state equation, since transitions are always firable due to the absence of guards: Here, σ can be seen as the Parikh image of a sequence σ leading from m to m . Proof. By the state equation, we have: Therefore, d Q (m, m ) (resp. d Z (m, m )) are computable by (resp. integer) linear programming, which is complete for P (resp. NP), in its variant where one must check whether the minimal solution is at most some bound. For d Q ≥0 , note that the reachability relation of a continuous Petri net can be expressed in the existential fragment of linear real arithmetic [8] . Hence, effectiveness follows from the decidability of linear real arithmetic. Altogether, we conclude that d G is a distance under-approximation. Furthermore, we can show that d G yields unbounded heuristics, which, by Theorem 1, ensure termination of GBFS on reachable instances: Moreover, the heuristics arising from it are unbounded. Proof. Let N = (P, T, f, λ) be a weighted Petri net. Effectiveness of d G follows from Proposition 2. By definitions and a simple induction, σ − → N ⊆ σ − → G for any sequence σ ∈ T * , with weights left unchanged for unscaled transitions. This implies that d G (m, m ) ≤ dist N (m, m ) for every m, m ∈ G P . Moreover, the triangle inequality holds since for every m, m , m ∈ G P and sequences σ, σ : Let us sketch the proof of the second part. Let m target be a marking and let h G be the heuristic obtained from d G for m target . Since h Q (m) ≤ h G (m) for all m and G ∈ {Z, Q ≥0 }, it suffices to prove that d Q is unbounded. Suppose it is not. There exist b ∈ Q ≥0 and pairwise distinct markings m 0 , m 1 , . . . each with h Q (m i ) ≤ b. Let x i be a solution to the state equation that gives h Q (m i ). By well-quasi-ordering and pairwise distinctness, there is a subsequence such that m i0 (p) < m i1 (p) < · · · for some p ∈ P . Thus, lim j→∞ m target (p) − m ij (p) = −∞, and hence lim j→∞ x ij (s) = ∞ for some s ∈ T with ∆ s (p) < 0. This means that b ≥ h Q (m ij ) = t∈T λ(t) · x ij (t) > b for a sufficiently large j. We have all the ingredients to use Algorithm 1 for answering reachability queries. A distance under-approximation scheme is a mapping D that associates a distance under-approximation D(N ) to each weighted Petri net N . Let h D(N ),mtarget be the heuristic obtained from D(N ) for marking m target . By instantiating Algorithm 1 with this heuristic, we can search for a short(est) firing sequence witnessing that m target is reachable. Of course, constructing the reachability graph of N would be at least as difficult as answering this query, or impossible if it is infinite. Hence, we provide G N (N ) symbolically through N and let Algorithm 1 explore it on-the-fly by progressively firing its transitions. For each G ∈ {Z, Q, Q ≥0 }, the function D G mapping a weighted Petri net N to its G-distance d G is a distance under-approximation scheme with consistent and unbounded heuristics by Proposition 1, Theorem 1 and Theorem 2. Although Algorithm 1 is geared towards finding paths, it can prove non-reachability even for infinite reachability graphs. Indeed, at some point, every candidate marking m ∈ C may be such that h D(N ),mtarget (m) = ∞, which halts with ∞. There is no guarantee that this happens, but, as reported e.g. by [23, 8] , the G-distance for domains G ∈ {Z, Q, Q ≥0 } does well for witnessing non-reachability in practice, often from the very first marking m init . An example. We illustrate our approach with a toy example and D Q (the scheme based on the state equation over Q T ≥0 ). Consider the Petri net N illustrated on the left of Figure 1 We consider the case where Algorithm 1 follows a greedy best-first search, but the markings would be expanded in the same way with A * . Let us abbreviate a marking [p 1 : x, p 2 : y] as (x, y). Since ∆ t2 = (0, 1), the heuristic considers that m init can reach m target in a single step using transition t 2 (it is unaware of the guard). Marking (1, 0) is expanded and its heuristic value increases to 2 as the state equation considers that both t 2 and t 3 must be fired (in some unknown order). Markings (2, 0) and (1, 1) are both discovered with respective heuristic values 3 and 1. The latter is more promising, so it is expanded and target (0, 1) is discovered. Since its heuristic value is 0, it is immediately expanded and the correct distance dist N (m init , m target ) = 3 is returned. Note that, in this example, the only markings expanded are precisely those occurring on the shortest path. Handling multiple targets. Algorithm 1 can be adapted to search for some marking from a given target set X ⊆ N P . The idea consists simply in using a heuristic h X : N P → Q ≥0 ∪ {∞} estimating the weight of a shortest path to any target: This is convenient for partial reachability instances occurring in practice, i.e. X := m target ∈ N P : m target (p) ∼ p c(p) where c ∈ N P and each ∼ p ∈ {=, ≥}. We implemented Algorithm 1 in a prototype called FastForward [10] , which supports all presented selection strategies and distance under-approximations. We evaluate FastForward empirically with three main goals in mind. First, we show that our approach is competitive with established tools and can even vastly outperform them, and we also give insights on its performance w.r.t. its parameterizations. Second, we compare the length of the witnesses reported by the different tools. Third, we briefly discuss the quality of the heuristics. Technical details. Our tool is written in C# and uses Gurobi [32] , a state-ofthe-art MILP solver, for distance under-approximations. Benchmarks were run on an machine with an 8-Core Intel R Core TM i7-7700 CPU @ 3.60GHz running Ubuntu 18.04 and with memory constrained to ∼8GB. We used a timeout of 60 seconds per instance, and all tools were invoked from a Python script using the time module for time measurements. A minor challenge arises from the fact that many instances specify an upwardclosed set of initial markings rather than a single one. For example, m init (p) ≥ 1 to specify, e.g., an arbitrary number of threads. We handle this by setting m init (p) = 1 and adding a transition t p producing a token into p. As a preprocessing step, we implemented sign analysis [29] . It is a general pruning technique running in polynomial time that has been shown beneficial for reducing the size of the state-space of Petri nets. Initially, places that carry tokens are viewed as marked. For each transition whose input places are marked, the output places also become marked. When a fixpoint is reached, places left unmarked cannot carry tokens in any reachable marking, so they are discarded. Benchmarks. Due to the lack of tools handling reachability for unbounded state spaces, benchmarks arising in the literature are primarily coverability instances 5 , i.e. reachability towards an upward closed set of target markings. We gathered 61 positive and 115 negative coverability instances originating from five suites [39, 28, 6, 35, 18] previously used for benchmarking [23, 8, 29] . They arise from the analysis of multi-threaded C programs with shared-memory; mutual exclusion algorithms; communication protocols; provenance analysis in the context of a medical messaging and a bug-tracking system; and the verification of Erlang concurrent programs. We further extracted the sypet suite made of 30 positive (standard) reachability instances arising from queries encountered in type-directed program synthesis [24] . The overall goal of this work is to enable a vast range of untapped applications requiring reachability over unbounded state-spaces, rather than just coverability. To obtain further (positive) instances of the Petri net reachability problem, we performed random walks on the Petri nets from the aforementioned coverability benchmarks. To this end, we used the largest quarter of distinct Petri nets from each coverability suite, for a total of 33. We performed one random walk each of lengths 20, 25, 30, 35, 40, 50, 60, 75, 90 and 100, and we saved the resulting marking as the target. For nets with an upward-closed initial marking, we randomly chose to start with a number of tokens between 1 and 20% of the length of the walk. It is important to note that even with long random walks, instances can (and in fact tend to) have short witnesses. To remove trivial instances and only keep the most challenging ones, we removed those instances where any considered tool reported a witness of length at most 20, disregarding the transitions used to generate the initial marking. This leaves us with 127 challenging instances on which the shortest witness is either unknown or has length more than 20. Moreover, this yields real-world Petri nets with no bias towards any specific kind of targets. This Tool comparison. To evaluate our approach on reachability instances, we compare FastForward to LoLA [53] , a tool developed for two decades that wins several categories of the Model Checking Contest every year. LoLA is geared towards model checking of finite state spaces, but it implements semi-decision procedures for the unbounded case. We further compare the three selection strategies of Algorithm 1: A * , GBFS and Dijkstra; the two first with the distance under-approximation scheme D Q , which provides the best trade-off between estimate quality and efficiency. In fact, the other heuristics perform strictly worse on almost all instances. We also considered comparing with KReach [17] , a tool showcased at TACAS'20 that implements an exact non-elementary algorithm. However, it timed out on all instances with a larger time limit of 10 minutes. Figure 2 depicts the number of reachability instances decided by the tools within the time limit. As shown, all approaches outperform LoLA, with GBFS as the clear winner on the random-walk suite and A * slightly better on the sypet suite. Note that Dijkstra's selection strategy sometimes competes due to its locally very cheap computational cost (no heuristic evaluation), but its performance generally decreases as the distance increases. To show the versatility of our approach, we also benchmarked FastForward on the original coverability instances. Recall that coverability EXPSPACEcomplete and reduces to reachability in linear time [45, 51] . While exceeding the PSPACE-completeness of reachability for finite state-spaces [38, 21] , coverability is much more tame than the non-elementary complexity of (unbounded) reachability. We compare FastForward to four tools implementing algorithms tailored, some of which are specifically to the coverability problem: LoLA, Bfc [39] , ICover [29] and the backward algorithm (based on [1] ) of mist [28] . We did not test Petrinizer [23] since it only handles negative instances, while we focus on positive ones; likewise for QCover [8] since it is superseded by ICover. Figure 3 illustrates the number of coverability instances decided within the time limit. The left side corresponds to an evaluation on the original instances where FastForward performs pruning (included in its runtime). On the right-hand side the pruned instances are the input for all tools, and the time for this pruning is not included for any tool. As a caveat, ICover performs its own preprocessing which includes pruning among techniques specific to coverability. This preprocessing is enabled (and its time is included) even when pruning is already done. Using FastForward(A * , D Q ), we decide more instances than all tools on unpruned Petri nets, and one less than Bfc for pre-pruned instances. It is worth mentioning that with a time limit of 10 minutes per instance, FastForward(A * , D Q ) is the only tool to decide all 61 instances. We also compared the running time of A * and GBFS with D Q to the other tools and approaches. For each tool, we considered the type of instances it can handle: either reachability and coverability, or coverability only. Figure 4 depicts this comparison, where the base approach is faster for data points that lie in the upper-left half of the graph. The axes start at 0.1 second to avoid a comparison based on technical aspects such as the programming language. Yet, LoLA, Bfc and mist regularly solve instances faster than this, which speaks to their level of optimization. We can see that FastForward outperforms ICover, LoLA and mist overall. We cannot compete with Bfc in execution time as it is a highly optimized tool specifically tailored to only the coverability problem that can employ optimization techniques such as Karp-Miller trees that do not work for reachability queries. Length of the witnesses. Since our approach is also geared towards the identification of short(est) reachability witnesses, we compared the different tools with respect to length of the reported one, depicted in Figure 5 . Positive values on the y-axis mean the witness was not minimal, while y = 0 means it was. Note that the points for Bfc must be taken with a grain of salt: it uses a different file format, and its translation utility can introduce additional transitions. This means that even if Bfc found a shortest witness, it could be longer than a shortest one of the original instance. Still, the graph shows that reported witnesses can be far from minimal. For example, on one instance LoLA returns a witness that is 53 transitions longer than the one of FastForward(A * , D Q ). Still, LoLA returns a shortest witness on 28 out of 43 instances. Similarly, FastForward(GBFS, D Q ) finds a shortest path on 60 out of 83 instances 6 . In contrast, mist finds a shortest witness on all instances since its backward algorithm is guaranteed to do so on unweighted Petri nets, which constitute all of our instances. Again, this approach is tailored to coverability and cannot be lifted to reachability. Heuristics and pruning. We briefly discuss the quality of the heuristics and the impact of pruning. The left-hand side of Figure 6 compares the exact distance to the estimated distance from the initial marking. 7 It shows that it is incredibly accurate for all G-distances, but even more so for G = Q ≥0 . We experimented with this distance using the logical translation of [8] and Z3 [49] as the optimization modulo theories solver. At present, it appears that the gain in estimate quality does not compensate for the extra computational cost. As depicted on the right-hand side of Figure 6 , pruning can make some instances trivial, but in general, many challenging instances remain so. On average, around 50% of places and 40% of transitions were pruned. We presented an efficient approach to the Petri net reachability problem that uses state-space over-approximations as distance oracles in the classical graph traversal algorithms A * and greedy best-first search. Our experiments have shown that using the state equation over Q T ≥0 provides the best trade-off between computational feasibility and the accuracy of the oracle. However, we expect that further advances in optimization modulo theories solvers may enable employing stronger over-approximations such as continuous Petri nets in the future. Moreover, non-algebraic distance under-approximations also fit naturally in our framework, e.g. the syntactic distance of [55] and "α-graphs" of [24] . These are crude approximations with low computational cost. Our preliminary tests show that, although they could not compete with our distances, they can provide early speed-ups on instances with large branching factors. An interesting line of research consists in identifying cheap approximations with better estimates. We wish to emphasize that our approach to the reachability problem has the potential to also be naturally used for semi-deciding reachability in extensions of Petri nets with a recursively enumerable reachability problem, such as Petri nets with resets and transfers [3, 19] as well as colored Petri nets [37] . These extensions have, for instance, been used for the generation of program loop invariants [54] , the validation of business processes [59] and the verification of multi-threaded C and Java program skeletons with communication primitives [16, 39] . Linear rational and integer arithmetic over-approximations for such extended Petri nets exist [12, 9, 34, 31] and could smoothly be used inside our framework. Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. General decidability theorems for infinite-state systems A Petri net approach to the study of persistence in chemical reaction networks Some decision problems related to the reachability problem for Petri nets Unbounded-thread program verification using thread-state equations Structural counter abstraction Privacy and utility in business processes νZ -an optimizing SMT solver The logical view on continuous Petri nets Affine extensions of integer vector addition systems with states Fastforward: A tool for reachability in Petri nets with infinite state spaces. Artifact for the TACAS21 contribution "Directed Reachability for Infinite-State Systems Petri net modelling of biological networks Context-free commutative grammars with integer counters and resets The reachability problem for Petri nets is not elementary Continuous Petri nets Discrete, Continuous, and Hybrid Petri nets Towards the automated verification of multithreaded Java programs Kreach: A tool for reachability in Petri nets Automatic verification of erlang-style concurrency Reset nets between decidability and undecidability Survey on directed model checking Decidability and complexity of Petri net problems -An introduction Verification of population protocols An SMT-based approach to coverability analysis Component-based synthesis for complex APIs Complexity analysis of continuous Petri nets Dynamic and Interactive Synthesis of Code Snippets Codehint: dynamic and interactive synthesis of code snippets Algorithmes et structures de données efficaces pour la manipulation de contraintes sur les intervalles Occam's razor applied to the Petri net coverability problem Reasoning about systems with many processes Continuous reachability for unordered data Petri nets is in PTime Gurobi optimizer reference manual Petri nets for systems and synthetic biology Linear combinations of unordered data vectors Issue Tracking Systems. Master's thesis A heuristic search approach using approximate solutions to Petri net state equations for scheduling flexible manufacturing systems Coloured Petri nets: basic concepts, analysis methods and practical use Complexity of some problems in Petri nets A widening approach to multithreaded program verification Decidability of reachability in vector addition systems (preliminary version) A structure to decide reachability in Petri nets Scheduling flexible manufacturing systems using Petri nets and heuristic search Vector addition systems reachability problem (A simpler solution) Demystifying reachability in vector addition systems The reachability problem requires exponential space Accelerating API-based program synthesis via API usage pattern mining An algorithm for the general Petri net reachability problem An approach using Petri nets and improved heuristic search for manufacturing system scheduling Z3: an efficient SMT solver Petri nets: Properties, analysis and applications The covering and boundedness problems for vector addition systems Artificial Intelligence: A Modern Approach LoLA: A low level analyser Loop summarization with rational vector addition systems An algorithmic framework for checking coverability in well-structured transition systems Reachability trees for Petri nets: a heuristic approach Parameterized complexity and approximability of coverability problems in weighted Petri nets Synchronization and cancelation in workflows based on reset nets Validation with guided search of the state space Model checking and abstraction to the aid of parameterized systems (a survey) We thank Juliette Fournis d'Albiat for her help with extracting the sypet suite.Directed Reachability for Infinite-State Systems