Michael Blondin
email: blondin@in.tum.de

Diro

Alain Finkel
email: finkel@lsv.ens-cachan.fr

Christoph Haase
email: christoph.haase@cs.ox.ac.uk

LSV Serge Haddad
email: haddad@lsv.ens-cachan.fr

A The Logical View on Continuous Petri Nets

Keywords: CCS Concepts:, Theory of computation → Automata over infinite objects, Logic and verification, Parallel computing models, Petri nets, vector addition systems, coverability, arithmetic theories, linear programming

Continuous Petri nets are a relaxation of classical discrete Petri nets in which transitions can be fired a fractional number of times, and consequently places may contain a fractional number of tokens. Such continuous Petri nets are an appealing object to study since they over approximate the set of reachable configurations of their discrete counterparts, and their reachability problem is known to be decidable in polynomial time. The starting point of this paper is to show that the reachability relation for continuous Petri nets is definable by a sentence of linear size in the existential theory of the rationals with addition and order. Using this characterization, we obtain decidability and complexity results for a number of classical decision problems for continuous Petri nets. In particular, we settle the open problem about the precise complexity of reachability set inclusion. Finally, we show how continuous Petri nets can be incorporated inside the classical backward coverability algorithm for discrete Petri nets as a pruning heuristic in order to tackle the symbolic state explosion problem. The cornerstone of the approach we present is that our logical characterization enables us to leverage the power of modern SMT-solvers in order to yield a highly performant and robust decision procedure for coverability in Petri nets. We demonstrate the applicability of our approach on a set of standard benchmarks from the literature.

of biological, chemical and business processes (see e.g. [START_REF] German | Reasoning about Systems with Many Processes[END_REF][START_REF] Ball | Parameterized Verification of Multithreaded Software Libraries[END_REF][START_REF] Venkatramana | Qualitative analysis of biochemical reaction systems[END_REF][START_REF] Heiner | Petri Nets for Systems and Synthetic Biology[END_REF][START_REF] Wil | The application of Petri nets to workflow management[END_REF]).

The reachability problem is the central decision problem for Petri nets: given an initial and a target configuration, the reachability problem asks whether there exist a sequence of transitions leading from the initial configuration to the target configuration. Even though the reachability problem has been shown decidable several times over the course of the last 35 years [START_REF] Mayr | An Algorithm for the General Petri Net Reachability Problem[END_REF][START_REF] Kosaraju | Decidability of Reachability in Vector Addition Systems (Preliminary Version)[END_REF][START_REF] Lambert | The General Vector Addition System Reachability Problem by Presburger Inductive Invariants[END_REF][START_REF] Lambert | The General Vector Addition System Reachability Problem by Presburger Inductive Invariants[END_REF][START_REF] Leroux | Vector Addition System Reachability Problem: a Short Self-contained Proof[END_REF][START_REF] Leroux | Vector Addition Systems Reachability Problem (A Simpler Solution)[END_REF], no practically useful algorithm has yet been found. In particular, the problem is EXPSPACE-hard [START_REF] Lipton | The Reachability Problem Requires Exponential Space[END_REF]], and the best known upper bound is F ω 3 , "cubic Ackermannian" time [START_REF] Leroux | Demystifying Reachability in Vector Addition Systems[END_REF].

In order to alleviate these high computational costs, one approach is to find suitable over approximations of the sets of reachable configurations. If a configuration is not included in an over approximation, it is guaranteed not to be reachable in the standard semantics. For instance, one may relax the semantics of Petri nets by allowing places to contain a negative amount of tokens along a run before ending in a configuration in which all places have a non-negative number of tokens. Then testing for reachability simply amounts to solving a system of linear Diophantine equations, which can be achieved efficiently, both in terms of computational complexity (the problem is NPcomplete [START_REF] Borosh | Bounds on Positive Integral Solutions of Linear Diophantine Equations[END_REF]) and in practice via IP or SMT solvers. Such an approach has, for instance, been investigated by [START_REF] Esparza | Verification of Safety Properties Using Integer Programming: Beyond the State Equation[END_REF] and [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF], where state equations and so-called trap constraints are used in a semi-decision procedure for disproving reachability.

The focus of this paper is on continuous Petri nets, a variant of Petri nets in which a transition may be fired a fractional number of times, and where places may consequently carry a non-negative fractional number of tokens. Continuous Petri nets were introduced by [START_REF] David | Continuous Petri nets[END_REF] and provide a good over approximation of standard Petri nets, see e.g. [START_REF] Recalde | Autonomous Continuous P/T Systems[END_REF][START_REF] David | Discrete, Continuous, and Hybrid Petri nets[END_REF]. Moreover, their big advantage is that their reachability problem has recently been shown decidable in polynomial time [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF], contrasting greatly with the EXPSPACEhardness of their discrete counterparts.

Our Contribution

The starting point of this paper is to show that the reachability relation of continuous Petri nets is definable by a sentence of linear size in the existential theory of the rationals with addition and order, FO Q, +, < . In contrast to discrete Petri nets, this in particular yields an easy proof of the fact that reachability sets of continuous Petri nets are closed under all Boolean operations and projections. It moreover entails decidability and complexity results for decision problems of continuous Petri nets that are definable in FO Q, +, < , albeit not necessarily with optimal upper complexity bounds. The decision problems we consider in this paper are reachability set inclusion, ε-liveness and home state problems, and we can show for many of them tight upper bounds. In particular, we settle the precise complexity of the inclusion problem, which was left open by [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF] and [START_REF] Blondin | Approaching the Coverability Problem Continuously[END_REF].

A further main contribution of our work is to derive from our logical characterization of reachability in continuous Petri nets a highly performant and robust decision algorithm for the coverability problem for discrete Petri nets. The coverability problem is a relaxation of the reachability problem and defined as follows: given an initial and a target configuration, does there exist a sequence of transitions leading from the initial configuration to a configuration that covers the target configuration, i.e., one that is larger or equal to the target configuration? This problem was one of the first problems for Petri nets shown decidable [START_REF] Karp | Parallel Program Schemata: A Mathematical Model for Parallel Computation[END_REF], and is known to be EXPSPACE-complete [START_REF] Lipton | The Reachability Problem Requires Exponential Space[END_REF][START_REF] Rackoff | The Covering and Boundedness Problems for Vector Addition Systems[END_REF]]. It has attracted much attention in the literature since it enables the verification of safety properties of many systems while being algorithmically and empirically easier to solve than the reachability problem. The backward algorithm [START_REF] Arnold | Récursivit et cônes rationnels fermés par intersection[END_REF][START_REF] Parosh | General Decidability Theorems for Infinite-State Systems[END_REF]] is one of the most prominent algorithms for deciding coverability. Starting from the target configuration, it successively computes a set of minimal basis elements which provide a finite symbolic representation of the set of configurations starting from which the target configuration can be covered. The main bottleneck of the algorithm is that the size of the finite representation may grow doubly exponentially during the execution of the backward algorithm [START_REF] Bozzelli | Complexity Analysis of the Backward Coverability Algorithm for VASS[END_REF]. This problem is commonly known as the symbolic state explosion problem [START_REF] Delzanno | Covering sharing trees: a compact data structure for parameterized verification[END_REF].

In this paper, we revisit the classical backward algorithm for the coverability problem and use reachability in continuous Petri nets as a pruning heuristic in order to keep the set of minimal basis elements small. Since continuous Petri nets over approximate the reachability set of their discrete counter parts, if no configuration in the set of configurations defined by a minimal basis element is continuously reachable then no configuration is discretely reachable either. Therefore, minimal basis elements defining a set of configurations that are not continuously reachable from the initial configuration can be discarded during the execution of the algorithm, keeping the set of minimal basis elements small and thus speeding up the algorithm. In particular, our logical characterization enables us to leverage the power of modern SMT solvers in order to decide continuous reachability efficiently. The usefulness of our approach is demonstrated by evaluating it on a set of standard benchmarks from the literature. We show that our approach decides more than 91% of non-coverability instances, most of the time much faster when compared to existing tools, and none of those tools can individually decide more than 84%. Additionally, we show that our approach is also competitive when run on positive instances of coverability. In particular, overall our approach decides 142 out of 176 (80%) instances of our benchmark suite, while the best competitor only decides 122 (69%) instances.

Structure of this Paper

In Section 2, we define general notation, discrete and continuous Petri nets, and linear rational arithmetic, and we also recall some results from the literature. Section 3 is devoted to our logical characterization of the reachability relation for continuous Petri nets. In Section 4, we study the complexity of the inclusion, ε-liveness and home-state problems. Section 5 presents our algorithm for the coverability problem and its implementation. In Section 6, we conclude with a summary of our results and discuss some perspectives of our work.

PRELIMINARIES

General Notation

We denote by Q, Z and N the set of rationals, integers, and natural numbers, respectively, and by Q + the set of non-negative rationals. Throughout the whole paper, all numbers are encoded in binary, and rational numbers are encoded as pairs of integers. For q = a/b ∈ Q, we denote by q def = log a + log b + 1 the number of bits required to represent q. Let D ⊆ Q and I be a finite set of indices, we denote by D I the set of vectors indexed by I. We write a vector u as u = (u i ) i∈I . Given vectors u = (u i ) i∈I , v = (v i ) i∈I ∈ D I , addition u + v is defined component-wise, and this definition can be lifted to sets of vectors. Moreover, u ≤ v whenever u i ≤ v i for all i ∈ I, and u < v whenever u ≤ v and u = v. The support of v is the set

v def = {i ∈ I : v i = 0}.
Given finite sets of indices I and J, and D ⊆ Q, D I×J denotes the set of matrices over D with rows and columns indexed by elements from I and J, respectively. Let M ∈ D I×J , I ⊆ I and J ⊆ J, we denote by M I ×J the D I ×J sub-matrix obtained from M whose row and columns indices are restricted to I and J , respectively.

Petri Nets

In what follows, we introduce the syntax and semantics of Petri nets. While we provide a single syntax for nets, we introduce in this section a discrete semantics (i.e. in N), and a continuous semantics (i.e. in Q + ) in the next section.

Definition 2.1. A Petri net is a tuple N = (P, T, Pre, Post), where P is a finite set of places; T is a finite set of transitions such that P ∩ T = ∅; and Pre, Post ∈ N P ×T are the backward and forward incidence matrices, respectively. A (discrete) marking of N is a vector of N P . The incidence matrix Incid of N is the P × T integer matrix defined by

Incid def = Post -Pre.
For complexity purposes, we assume that a Petri net is encoded by enumerating the transitions of N , where every transition of N is encoded as a tuple listing its nonzero entries in Pre and Post. We denote by |N | the size of N . The reverse net of N is N -1 def = (P, T, Post, Pre). Let p ∈ P and t ∈ T , the pre-sets of p and t are the sets

• p def = {t ∈ T : Post(p, t ) > 0} and • t def = {p ∈ P : Pre(p , t) > 0}, respectively.
Likewise, the post-sets of p and t are p • def = {t ∈ T : Pre(p, t ) > 0} and t • = {p ∈ P : Post(p , t) > 0}, respectively. Those definitions can canonically be lifted to subsets of places and of transitions, e.g., for

Q ⊆ P we have • Q = p∈Q • p.
We also introduce the neighbors of a subset of places/transitions by:

• Q • = • Q ∪ Q • . Let S ⊆ T , then N S is the sub-net defined by N S def = ( • S • , S, Pre• S • ×S , Post• S • ×S ).
We say that a transition t ∈ T is enabled at a marking m whenever m(p) ≥ Pre(p, t) for every p ∈ • t. A transition t that is enabled can be fired, leading to a new marking m such that for all places p ∈ P , m (p) = m(p) + Incid(p, t). We write m t -→ m whenever t is enabled at m and leads to m , and write m -→ m if m t -→ m for some t ∈ T . By -→ * we denote the reflexive transitive closure of -→.

A word σ = t 1 t 2 • • • t k ∈ T * is a firing sequence of (N , m 0 ) whenever there exist markings m 1 , . . . , m k such that m 0 t1 -→ m 1 t2 -→ • • • t k-1 ---→ m k-1 t k -→ m k .
Two of the most prominent decision problems for Petri nets are reachability and coverability.

Definition 2.2. Given a Petri net N = (P, T, Pre, Post), an initial marking m 0 ∈ N P and a target marking m ∈ N P , reachability is the problem to decide whether m 0 -→ * m, and the coverability problem asks whether m 0 -→ * m for some m ≥ m.

Reachability is known to be decidable, EXPSPACE-hard [START_REF] Lipton | The Reachability Problem Requires Exponential Space[END_REF][START_REF] Cardoza | Exponential Space Complete Problems for Petri Nets and Commutative Semigroups: Preliminary Report[END_REF]] and in F ω 3 [START_REF] Leroux | Demystifying Reachability in Vector Addition Systems[END_REF], a non-primitive-recursive complexity class. Coverability is EXPSPACE-complete [START_REF] Lipton | The Reachability Problem Requires Exponential Space[END_REF][START_REF] Cardoza | Exponential Space Complete Problems for Petri Nets and Commutative Semigroups: Preliminary Report[END_REF][START_REF] Rackoff | The Covering and Boundedness Problems for Vector Addition Systems[END_REF]. The reachability relation of a Petri net N is defined as

R(N ) def = {(m, m ) ∈ N P × N P : m - → * m }.

Continuous Petri Nets

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

enab(t, m) def = min{m(p)/Pre(p, t) : p ∈ • t} if • t = ∅ ∞ otherwise.
We say that t is Q-enabled at m if enab(t, m) > 0. If t is Q-enabled it may be fired by any amount q ∈ Q + such that 0 ≤ q ≤ enab(t, m), leading to a new marking m such that for all places p ∈ P , m (p)

def = m(p)+q •Incid(p, t).
In this case, we write m

q•t --→ Q m . The definition of a Q-firing sequence σ = q 1 t 1 • • • q k t k ∈ (Q + × T ) * is
analogous to the standard definition of firing sequence, and so are -

→ Q , - → * Q and Q-reachability. The Q- Parikh image of the firing sequence σ is the vector π(σ) ∈ Q T + such that π(σ)(t) def =
ti=t q i . We also adapt the aforementioned decision problems for Petri nets. Definition 2.3. Given a Petri net N = (P, T, Pre, Post), an initial marking m 0 ∈ Q P + and a target marking m

∈ Q P + , the Q-reachability (respectively Q-coverability) problem asks whether m 0 - → * Q m (respectively m 0 - → * Q m for some m ≥ m).
Both reachability and coverability in continuous Petri nets can be decided with surprisingly low complexity, as captured in the following proposition. PROPOSITION 2.4 ([FRACA AND HADDAD 2015]). Both Q-reachability and Qcoverability are P-complete.

The continuous reachability relation of a Petri net N is defined as

QR(N ) def = {(m, m ) ∈ Q P + × Q P + : m - → * Q m }.
An important observation about continuous Petri nets is that their reachability sets over approximate the reachability sets of discrete Petri nets: m -→ m implies m -→ Q m , and hence m -→ * m implies m -→ * Q m , i.e., R(N ) ⊆ QR(N ) for any Petri net N .

Linear Rational Arithmetic

A tool allowing us to show decidability and complexity results in this paper is the first-order theory of the rational numbers with addition and order, FO Q, +, < . Atomic formulas in this theory are linear constraints over first-order variables x = (x 1 , . . . , x n ) that we write as a • x ∼ b, where ∼ ∈ {=, <, ≤, ≥, >}, a ∈ Q n and b ∈ Q. The size |Φ| of a formula Φ is the number of symbols required to write down Φ, where we assume binary encoding of numbers. Formulas of FO Q, +, < are interpreted in their natural semantics, and we write Φ(x) for the subset of n-tuples of rational numbers defined by Φ, i.e.,

Φ(x) def = {(q 1 , . . . , q n ) ∈ Q n : Φ(q 1 /x 1 , . . . , q n /x n ) is valid}.
We write ϕ(x) ≡ ψ(x) whenever ϕ and ψ are semantically equivalent, i.e., define the same tuples of rational numbers. It is an easy exercise to show that for an FO Q, +, < formula, we may with no loss of generality assume that it does not contain any negation symbol, and that the only relation symbols used are > and ≥.

The full theory of FO Q, +, < is decidable in EXPSPACE and in fact complete for STA( * , 2 O(n) , n) [START_REF] Berman | The Complexitiy of Logical Theories[END_REF]]. Here, STA(s(n), t(n), a(n)) is the space-time-alternation measure on the complexity of a decision problem, which consists of all problems decidable by an alternating Turing machine that uses on every computation path at most s(n) tape cells, runs in time t(n) and makes a(n) alternations. Moreover, " * " indicates an unbounded availability of a certain resource. For fixed quantifier alternation prefixes, the complexity of FO Q, +, < is more manageable, and its restriction to a fixed number of i quantifier alternations is only complete for the i-th level of the polynomial hierarchy.

PROPOSITION 2.5 ([SONTAG 1985, COR. 3.4]). For every i > 0, the Σ i -fragment (resp. Π i -fragment) of FO Q, +, < is complete for Σ P i (resp. Π P i ).

A LOGICAL CHARACTERIZATION OF REACHABILITY IN CONTINUOUS PETRI NETS

In this section, we develop a logical characterization of the continuous reachability relation of a given Petri net in the existential fragment of FO Q, +, < . Our starting point is the work of [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF] that presents an algorithm to decide reachability in continuous Petri nets in polynomial time. This algorithm builds upon a characterization of continuous reachability that we recall in Section 3.1 below. Subsequently, in Section 3.2 we show how this characterization can be used in order to obtain an existential FO Q, +, < formula of linear size defining the continuous reachability relation. For the remainder of this section, we fix a Petri net N = (P, T, Pre, Post).

Three Criteria Characterizing Continuous Reachability

The key insight underlying the algorithm developed by Fraca and Haddad is that continuous reachability can be characterized in terms of three simple criteria. First, for a Petri net N and a marking m ∈ Q P + , we introduce the auxiliary definition of firing set, denoted by fs(N , m). Recall that π(σ) denotes the Parikh image of a firing sequence σ, and that π(σ) ⊆ T is the support of this firing sequence. We set

fs(N , m) def = { π(σ) : σ ∈ (Q + × T ) * and there is m ∈ Q P + s.t. m σ -→ Q m }.
Thus, fs(N , m) is the set of supports of firing sequences starting in an initial marking m. Even though fs(N , m) can be of size exponential with respect to |T |, deciding T ∈ fs(N , m) for some T ⊆ T can be done in polynomial time. The following proposition characterizes the pairs of Q-reachable markings. PROPOSITION 3.1 ([FRACA AND HADDAD 2015, THM. 20]). Given a Petri net N = (P, T, Pre, Post), we have (m, m ) ∈ QR(N ) if, and only if, there exists

y ∈ Q T + such that (i) m = m + Incid • y (ii) y ∈ fs(N , m) (iii) y ∈ fs(N -1 , m ).
Here, y should be seen as the Parikh image of a firing sequence. The first item expresses the state equation of N with respect to m, m and y; the two subsequent items express that the support of the solution of the state equation has to lie in the firing set of N and its reverse.

The Logical Characterization

We now show how to encode the conditions of Proposition 3.1 in the existential fragment of FO Q, +, < . Condition (i) of Proposition 3.1, which expresses the state equation, is readily expressed as a system of linear equations and thus directly corresponds to a formula Φ N eqn (x, x , y) which holds whenever a marking x is reached starting in marking x by firing every transition y(t) times (without any consideration whether such a firing sequence would actually be admissible). Formally,

Φ N eqn (x, x , y) def = x = x + Incid • y ∧ y ≥ 0,
where 0 denotes the null-vector in an appropriate dimension.

Next, we show how to encode Conditions (ii) and (iii) into suitable formulas. To this end, we require an effective characterization of membership in the firing set fs(N , x) defined in Section 3.1. The following characterization can be derived from [Fraca and Haddad 2015, Cor. 19]. First, we define a monotonic increasing function incfs N ,x : 2 T → 2 T as follows:

incfs N ,x (S) def = S ∪ {t ∈ T : • t ⊆ ( x ∪ {s • : s ∈ S})} .
Loosely speaking, incfs N ,x (S) returns the set of transitions S, and additionally those transitions that can be fired when the places in x and those that receive tokens from transitions in S all carry tokens. Fraca and Haddad [2015, Cor. 19] considered an algorithm from which it follows that

T ∈ fs(N , x) ⇐⇒ T = lfp(incfs N T ,x ), ( 1
)
where lfp is the least fixed point operator, i.e.,

T = incfs N T ,x (• • • (incfs N T ,x (∅)) • • • ).
Notice the restriction of N to N T . Clearly, the least fixed point is reached after at most |T | iterations.

In order to decide whether y ∈ fs(N , x), we simulate this fixed-point computation by an existential FO Q, +, > -formula Φ N fs (x, 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 a formula in existential Presburger arithmetic of linear size [START_REF] Kumar | On the Complexity of Equational Horn Clauses[END_REF]. The basic idea is to introduce additional first-order variables z indexed by P ∪ T that, given a firing set, capture the relative order in which transitions of this set are fired and the order in which their input places are marked. This order corresponds to the computation of lfp(incfs N y ,x ) and is encoded via a numerical value z(t) (respectively z(p)), representing an index that must be strictly greater than zero for a transition (respectively an input place of a transition) of this set. In addition, input places have to be marked before the firing of a transition, which is captured by the following formula:

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

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

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

Φ N (x, x ) def = ∃y : Φ N eqn (x, x , y) ∧ Φ N fs (x, y) ∧ Φ N -1 fs (x , y). PROPOSITION 3.2. Let N be a Petri net. There exists an existential FO Q, +, < - formula Φ N (x, x ) computable in time O(|N |) with 4 • |P | + 3 • |T | variables such that QR(N ) = Φ N (x, x ) . PROOF. We first show that QR(N ) ⊆ Φ N (x, x ) . Suppose (m, m ) ∈ QR(N ). By Proposition 3.1, there is some y ∈ Q T + such that m = m + Incid • y, y ∈ fs(N , m) and y ∈ fs(N , m ). Consequently, Φ N eqn (m/x, m /x , y) holds. Let T = y , since T ∈ fs(N , m), by (1) we have T = lfp(incfs N T ,m ). Denote by incfs i N T ,m (∅) the i-fold application of incfs N T ,m on ∅.
For every transition t ∈ T , we record the first time t occurs in the fixed point computation and define

z(t) def = i if t ∈ incfs i N T ,m (∅) and t / ∈ incfs i-1 N T ,m (∅) 0 otherwise. Since lfp(incfs N T ,m ) = incfs |T | N T ,m (∅), z(t)
> 0 for all t ∈ T , and z(t) = 0 for every t ∈ T \ T . For every p ∈ P , define

z(p) def = i if p ∈ • (incfs i N T ,m (∅)) and p / ∈ • (incfs i-1 N T ,m (∅)) 0 otherwise. We now claim that z is a valid solution for Φ N dt (y, z) and Φ N mk (m/x, y, z). Regarding the former, since y(t) > 0 whenever t ∈ T , by construction z(p) ≤ z(t) for every p ∈ • t, since t ∈ incfs z(t)
N T ,m (∅), and hence p ∈ • (incfs

z(t)
N T ,m (∅)). Likewise, it follows that z(p) > 0, and, as already discussed above, z(t) > 0. Regarding validity of Φ N mk (m/x, y, z), suppose z(p) > 0. If z(p) = 1 then by definition of incfs N T ,m we have m(p) > 0.

Otherwise, again by definition of incfs N T ,m , there is some t ∈ incfs

z(p)-1 N T ,m (∅) such that p ∈ t • , and hence 0 < z(t) < z(p). It follows that Φ N fs (m/x, y) is valid. Validity of Φ N -1 fs (m/x, y) can be shown along similar lines. It follows that Φ N (m/x, m /x ) is valid.
In order to show Φ N (x, x ) ⊆ QR(N ), let x, x , y, z 1 and z 2 be valuations of variables such that Φ N (x, x ) evaluates to true (here, we implicitly view Φ N to be open in all those variables). Again, Condition (i) of Proposition 3.1 is easily seen to be true due to Φ N eqn (x, x , y) being valid. Thus, let us show that Condition (ii) of Proposition 3.1 holds, i.e., that y ∈ fs(N , x). Our starting point is that

Φ N dt (y, z 1 /z) and Φ mk (x, y, z 1 /z) hold. Let T def = y and T 1 , . . . , T m ⊆ T be such that -z 1 (t) = z 1 (t ) whenever {t, t } ⊆ T i ; -z 1 (t i ) < z 1 (t j ) for all i < j such that t i ∈ T i and t j ∈ T j ; and -z 1 (t) > 0 if and only if t ∈ T i for some 1 ≤ i ≤ m.
We now show by induction on i ≥ 1 that 1≤j≤i T j ⊆ incfs i N T ,m (∅). For the induction base case, since Φ N dt (y, z 1 /z) holds, for every transition t ∈ T 1 we have either • t = ∅, or 0 < z 1 (p) ≤ z 1 (t) for all p ∈ • t. In the latter case, since Φ mk (x, y, z 1 /z) holds, we have x(p) > 0, i.e., p ∈ x , for all p ∈ • t since there cannot Table I. Decision problems for continuous Petri nets N , M, where N = (P, T, Pre, Post). Here, ε is a firstorder variable and x, x and x are vectors of first-order variables indexed by places p ∈ P , e.g., x = (xp) p∈P . New complexity results established in this paper are colored.

Decision Problem

Definition Complexity

Coverability Φ N cvr (x, x ) def = ∃x : Φ N (x, x ) ∧ x ≥ x P-complete Boundedness Φ bnd (x) def = ∃x : ∀x : Φ N (x, x ) → x ≥ x P-complete Inclusion Φ N ,M inc (x, x ) def = ∀x : Φ N (x, x ) → Φ M (x , x ) coNP-complete ε-Liveness Φ N lv (x) def = ∃ε : ε > 0 ∧ ∀x : Φ N (x, x ) → → t∈T ∃x : Φ N (x , x ) ∧ Φ N ,t nbld (ε, x ) in Σ P 3 Struct. ε-Liveness Φ N slv def = ∃x : Φ N lv (x) in Σ P 3 Home State Φ N hm (x, x ) def = ∀x : Φ N (x, x ) → Φ N (x , x ) coNP-complete Exist. Home State Φ N ehm (x) def = ∃x : Φ hm (x, x ) in Σ P 2 be transitions t ∈ T such that 0 < z 1 (t ) < z 1 (p) due to all transitions in T 1 being minimal with respect to z 1 . Hence T 1 ⊆ incfs 1 N T ,m (∅). For the induction step, suppose that 1≤j≤i T j ⊆ incfs i N T ,m (∅) and let t ∈ T i+1 . As in the base case, if • t = ∅ we are done. Otherwise, since Φ N dt (y, z 1 /z) holds, we have 0 < z 1 (p) ≤ z 1 (t) for all p ∈ • t. Since Φ mk (x, y, z 1 /z) also holds, for p ∈ • t we have x(p) > 0, or there is some t ∈ 1≤j≤i T j such that p ∈ t • . By the induction hypothesis, we conclude that • t ⊆ ( x ∪ {t • : t ∈ incfs i N T ,m (∅)}), and hence t ∈ incfs i+1 N T ,m (∅). Now since y(t) > 0 implies z(t) > 0, we have T = 1≤i≤m T i , and consequently T = y ∈ fs(N , x).
Regarding the complexity of computing Φ N (x, x ), we first note that in linear time we can compute a list that keeps for each place p ∈ P its set of incoming transitions,

• p, and its set of outgoing transitions, p • . It follows that every formula Φ N eqn (x, x , y), Φ N fs (x, y) and Φ N -1 fs (x , y) can be computed by traversing the encoding of N or the aforementioned generated list once, and hence Φ N (x, x ) can overall be computed in O(|N |). Finally, observe that both x and x are vectors of |P | variables each, y is a vector of |T | variables, and z is a vector of |P | + |T | variables occurring twice. Consequently,

Φ N (x, x ) contains 4 • |P | + 3 • |T | variables.

DECISION PROBLEMS FOR CONTINUOUS PETRI NETS

Besides reachability, there exists a plethora of further decision problems for Petri nets whose decidability and computational complexity has been studied in the literature, both in the continuous and discrete setting. In Table I, we employ the formula Φ N (x, x ) defining the continuous reachability relation from Proposition 3.2 in order to give an overview of some decision problems for continuous Petri nets, their formal definition in FO Q, +, < , and their computational complexity. Cells with blue background color indicate results that we will establish in the subsequent sections.

In words, given a Petri net N , an initial marking m and a marking m , coverability asks whether there is some configuration m that is reachable and in which every place contains at least as many tokens as specified by m . This problem is Pcomplete [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF]. Boundedness asks whether there is some marking m such that every marking m reachable from m does not exceed m in any of its components. This problem is also P-complete [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF]. Given another Petri net M with the same set of places as N , inclusion asks whether every marking m reachable from m in N is also reachable in M starting in m . This problem is known to be coNP-hard and in EXP [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF], and we improve this result in Section 4.2 and show that inclusion is actually coNP-complete. ε-Liveness asks whether there exists a rational ε > 0 such that for every marking m reachable from m and every transition t ∈ T , a marking m is reachable such that t has enabling degree at least ε in m . For x = (x p ) p∈P , Table I uses the abbreviation

Φ N ,t nbld (ε, x) def = p∈ • t 1 Pre(p,t) • x p ≥ ε if • t = ∅ true otherwise,
i.e., Φ N ,t nbld (ε, x) holds whenever the enabling degree of t in x is at least ε. Structural εliveness asks whether there exists some initial marking m such that N is ε-live in m. We show in Section 4.3 that ε-liveness and structural ε-liveness are decidable in Σ P 3 . As mentioned by Recalde et al. [1999, Sec. 5], the definition of (structural) ε-liveness is arguably more suitable for continuous Petri nets as compared to the standard definitions from discrete Petri nets which only require enabledness. For example, consider a Petri net such that all of its transitions decrease the number of tokens. Such a Petri net is not live under the discrete semantics. However, it could be "live" under the continuous semantics by firing transitions by increasingly smaller amounts. It is difficult to give a natural interepration justifying such Zeno runs to contribute to liveness, especially in such a system that strictly monotonically decreases the number of tokens of every place. Finally, a marking m is a home state if m can be reached from every marking m that can be reached from m. The existential home-state problem is to decide whether there exists a home state for a given initial marking m. In Section 4.4, we show that the home-state problem is coNP-complete, and that the existential homestate problem is decidable in Σ P 2 . The benefit of our characterization of continuous reachability in FO Q, +, < is that we immediately obtain decidability of all decision problems presented in Table I via Proposition 2.5, albeit not always with optimal upper bounds. Roughly speaking, the reason for this is that satisfiability in existential FO Q, +, < is NP-complete while reachability in continuous Petri nets is P-complete. Nevertheless, our characterization turns out to be a good starting point for the (tight) upper bounds that we develop.

In the discrete setting, the complexity of the decision problems we consider is only rarely known and significantly higher than in the continuous setting. Both coverability and boundedness are EXPSPACE-complete [START_REF] Lipton | The Reachability Problem Requires Exponential Space[END_REF][START_REF] Rackoff | The Covering and Boundedness Problems for Vector Addition Systems[END_REF]; inclusion is undecidable [START_REF] Henri | Decidability questions for Petri Nets[END_REF]]; standard liveness is inter-reducible with reachability [START_REF] Henri | The Recursive Equivalence of the Reachability Problem and the Liveness Problem for Petri Nets and Vector Addition Systems[END_REF]] and structural liveness has recently been shown decidable and hard for reachability [START_REF] Jančar | Deciding Structural Liveness of Petri Nets[END_REF]]; the home state problem is decidable [de Frutos [START_REF] De | Decidability of home space property[END_REF][START_REF] Desel | Free Choice Petri nets[END_REF], and the existential home-state problem has recently been shown decidable and hard for reachability in discrete Petri nets [START_REF] Best | Existence of home states in Petri nets is decidable[END_REF].

It is worth mentioning that, except for coverability, the discrete versions of the decision problems of Table I cannot be over approximated via the continuous semantics. Let N 1 , N 2 and N 3 be the Petri nets illustrated in Figure 1 from left to right. It is readily seen that of N 1 from (1, 0) since it is the unique reachable marking. However, N 1 has no continuous home state from (1, 0) since r strictly increases the number of tokens. Therefore, inclusion, boundedness and the (existential) home state problems cannot be over approximated by the continuous semantics. As for liveness, observe that N 3 is live from (1, 1) as its only discrete run is (1, 1)

R(N 1 )(1, 0) = {(1, 0)}, R(N 2 )(1, 0) = {(n + 1, 0) : n ∈ N}, QR(N 1 )(1, 0) = {(1, n) : n ∈ Q + }, QR(N 2 )(1, 0) = {(n + 1, 0) : n ∈ Q + }. We have R(N 1 )(1, 0) ⊆ R(N 2 )(1, 0), but QR(N 1 )(1, 0) ⊆ QR(N 2 )(1, 0). Moreover R(N 1 )(1, 0) is bounded, but QR(N 1 )(1, 0) is not. Clearly, (
t - → (3, 0) u -→ (1, 1) t - → • • • . However, for every mark- ing (m, n), we have (m, n) (m/2)u -----→ Q (0, m/2 + n) and (0, m/2 + n)
is dead, regardless of the enabling degree.

Small Points in Convex Polyhedra and Projections of Convex Polyhedra

As a preparatory step for the subsequent sections, here we recall and establish a number of results concerning linear programming and FO Q, +, < . We first show that nonempty systems of mixed linear inequalities and strict inequalities contain small points.

Here and in the following, by "small" we mean objects which can be represented using a polynomial number of bits in the representation of a given system. Next, we show that the set of solutions of such systems can be obtained as the union of solutions sets of a finite number of polyhedra of small facet complexity. Finally, we provide a quantifier elimination method for FO Q, +, < which yields formulas of small facet complexity. All terminology will be clarified below.

The results explored in this section have partly been obtained by [START_REF] Sontag | Real Addition and the Polynomial Hierarchy[END_REF] and [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF], and are not novel as such. However, when looking at the exposition of [START_REF] Sontag | Real Addition and the Polynomial Hierarchy[END_REF], we observed that some proof details are rather coarse, and that more detailed yet no more complex arguments are possible. In Proposition 4.4 below, compared to the work of [START_REF] Sontag | Real Addition and the Polynomial Hierarchy[END_REF], we also provide a more explicit geometric characterization of projections of systems of mixed linear inequalities and strict inequalities. We believe and hope that an interested reader will view and appreciate our exposition as a valuable complement to the results and reasoning presented by [START_REF] Sontag | Real Addition and the Polynomial Hierarchy[END_REF].

We begin with introducing some auxiliary definitions. Let A ∈ Q m×n be an (m × n)matrix with rational coefficients, and let c ∈ Q m . We call S : A • x ≥ c a system of linear inequalities in the unknowns x = (x i ) 1≤i≤n . Writing A = (a i,j ) 1≤i≤m,1≤j≤n and c = (c i ) 1≤i≤m , S can alternatively be viewed as the conjunction

Ψ S (x) def = 1≤i≤m (a i,1 , . . . , a i,n ) • x ≥ c i .
(2)

We define the set S of solutions of S as

S def = Ψ S (x) ⊆ Q n .
The facet complexity S of S is the largest bit size needed to represent any row of S; formally:

S def = 1 + max 1≤i≤m 1≤j≤n a i,j + c i .
Note that the facet complexity is independent of the number of rows of S. For a single vector v ∈ Q m , v is the bit size of the largest component of v. By v we denote the maximum of the absolute values of all components of v, and for finite sets V ⊆ Q m we define V def = max v∈V v . If in the representation in (2) we allow further relational symbols such as > and =, we obtain systems of mixed linear inequalities, strict inequalities and equalities. We write such systems, e.g., as S : A • x ≥ c ∧ B • x > d (in particular, an equality can always be written as a conjunction of two non-strict inequalities). The definition of S is analogous as above.

Given a finite set of vectors V = {v 1 , . . . , v n } ⊆ Q m , in this paper the convex hull and the cone generated by V are defined as

conv V def = v ∈ Q m : v = n i=1 λ i • v i , λ i ∈ Q, 0 ≤ λ i ≤ 1, n i=1 λ i ≤ 1 cone V def = v ∈ Q m : v = n i=1 λ i • v i , λ i ∈ Q, λ i ≥ 0 .
Note that for subsequent technical convenience, in our definition of the convex hull we require the λ i to only sum up to less or equal to one, as opposed to exactly one which is more commonly found in the literature. We may do so as it is not difficult to check that for V as above there are u ∈ Q m and U = {u 2 , . . . ,

u n } ⊆ Q m such that u , U ≤ O( V ) and u + conv U = v ∈ Q m : v = n i=1 λ i • v i , λ i ∈ Q, 0 ≤ λ i ≤ 1, n i=1 λ i = 1 ,
and vice versa.

We first recall a classical result from the theory of linear programming that states that the set of solutions of a systems of linear inequalities can be obtained as the sum of a finite polyhedron and a cone. PROPOSITION 4.1. [Schrijver 1998, Thm. 10.2] Let S : A • x ≥ c be a system of linear inequalities. Then there exist a rational vector u and finite sets of rational vectors {v j } j∈J , {w k } k∈K such that u , v j , w k ≤ poly( S ) and

S = u + conv{v j } j∈J + cone{w k } k∈K .
In our first result, we apply Proposition 4.1 in order to show that non-empty systems of mixed linear inequalities and strict inequalities contain points whose representation size is polynomial in the facet complexity of the system. For such a system S : A

• x ≥ c ∧ B • x > d,
S = u + conv{v j } j∈J + cone{w k } k∈K
for some index sets J, K, and vectors u, {v j } j∈J and {w k } k∈K of bit size polynomial in S = S .

Let E be the linear subspace generated by {v j } j∈J and {w k } k∈K . It has dimension at most n. So there are subsets {v 1 , . . . v r } ⊆ {v j } j∈J and some {w 1 , . . . w s } ⊆ {w k } k∈K such that {v 1 , . . . v r , w 1 , . . . w s } generates E, r > 0 and r + s ≤ n. In particular, z = u + 1≤j≤r λ j • v j + 1≤j≤s µ j • w j for some {λ j } 1≤j≤r , {µ j } 1≤j≤s ⊆ Q.

Now define

z def = u + 1≤j≤r 1 2•r • v j + 1≤j≤s w j .
By construction z ∈ S and z ≤ poly( S ). We claim that z ∈ S. For the sake of contradiction, assume that some strict inequality of

B • z > d is violated, say b • z = d for some row b • x > d of B • x > d. For some ε > 0, consider vector z ε = (1 + ε) • z -ε • z. On the one hand, we have b • z ε = (1 + ε) • b • z -ε • b • z = d -ε • (b • z -d) < d.
On the other hand,

z ε = u + 1≤j≤r ( 1+ε 2•r -ε • λ j ) • v j + 1≤j≤s (1 + ε -ε • µ j ) • w j .
Thus for ε enough small, z ε ∈ S which yields a contradiction.

Next, we recall the reverse direction of Proposition 4.1. PROPOSITION 4.3. [Schrijver 1998, Thm. 10.2] Let u be a rational vector, and let {v j } j∈J , {w k } k∈K be finite sets of rational vectors. There exists a system of linear inequalities S : A • x ≥ b such that S ≤ poly( u + max j∈J v j + max k∈K w k ) and

S = u + conv{v j } j∈J + cone{w k } k∈K .
We now turn towards projections of systems of mixed linear inequalities and strict inequalities. Given such a system S : A • x ≥ c ∧ B • x > d such that x = (y, z), we denote by π y S the projection of the set of solutions of S onto y. The next proposition establishes that projections of the set of solutions of systems of mixed linear inequalities and strict inequalities can be obtained as the union of the set of solutions of a finite number of systems of mixed linear equalities and strict inequalities. PROPOSITION 4.4. Let S : A•x ≥ c∧B•x > d be a system of mixed linear inequalities and strict inequalities such that x = (y, z). Then there are a finite number of systems of mixed linear equalities and strict inequalities S i :

A i • y = b i ∧ B i • y > d i , i ∈ I,
such that S i ≤ poly( S ) for all i ∈ I, and

π y S = i∈I S i .
PROOF. By Proposition 4.1, there exist a rational vector u and finite sets of rational vectors {v j } j∈J , {w k } k∈K for some index sets J, K such that u , v j , w k ≤ poly( S ) and

S = u + conv{v j } j∈J + cone{w k } k∈K .
Projecting all vectors onto the y-components and applying Proposition 4.3, we obtain a system of linear inequalities S : C • y ≥ e such that π y S = S and S ≤ poly( S ). Write S as a conjunction of linear inequalities Ψ S such that

Ψ S = k∈K c k • y ≥ e k .
For a partition of K as K = E G, let S E,G be the system of mixed linear equalities and strict inequalities corresponding to

Ψ E,G : k∈E c k • y = e k ∧ k∈G c k • y > e k . Moreover, let I def = {(E, G) : π y S ∩ S E,G = ∅}.
We claim that π y S = i∈I S i . Since π y S ⊆ S , we have

π y S = π y S ∩ S = K=E G π y S ∩ S E,G = i∈I π y S ∩ S i ⊆ i∈I S i .
It thus remains to show that S E,G ⊆ π y S for every (E, G) ∈ I. To this end, let

(E, G) ∈ I, let u ∈ π y S ∩ S E,G and let v ∈ S E,G . For ε > 0, set v ε def = (1 + ε) • v -ε • u. For all k ∈ E we have c k •v ε = e k , and for all k ∈ G we have c k •v ε = c k •v +ε•c k •(v -u).
Thus, for small enough ε, we have v ε ∈ S E,G . Since u ∈ π y S and v ε ∈ S E,G ⊆ S = π y S , there exist w, w ε such that (u, w) ∈ S and (v ε , w ε ) ∈ S . It can easily be shown that α

1 • z 1 + α 2 • z 2 ∈ S for every z 1 ∈ S , z 2 ∈ S and α 1 , α 2 > 0 such that α 1 + α 2 = 1. Therefore, in particular, ε ε+1 • (u, w) + 1 ε+1 • (v ε , w ε ) ∈ S . Now, observe that v = ε 1+ε u + 1 1+ε v ε . This implies that (v, ε 1+ε • w + 1 1+ε • w ε ) ∈ S , and hence that v ∈ π y S .
Finally, we can employ Proposition 4.4 in order to provide a quantifier elimination procedure for FO Q, +, < which yields formulas of small facet complexity. Given a quantifier-free formula ϕ(x), recall that we may assume that no negation symbols occur in ϕ(x), and that the only relation symbols occurring in ϕ(x) are > and ≥. Hence, the disjunctive normal form of ϕ(x) can be written as

ϕ(x) ≡ i∈I A i • x ≥ c i ∧ B i • x > d i .
We define the facet complexity ϕ(x) as the maximum over S i , i ∈ I, where each S i is

A i •x ≥ c i ∧B i •x > d i .
Observe that negating ϕ(x) does not change its facet complexity. COROLLARY 4.5. Let ϕ(y, z) be a quantifier-free FO Q, +, < -formula. Then there is ψ(y) such that ψ(y) = π y ϕ(y, z) and ψ(y) ≤ poly( ϕ(y, z) ).

PROOF. Let x = (y, z), and let S

i : A i • x ≥ c i ∧ B i • x > d i , i ∈ I,
be all systems of mixed linear inequalities and strict inequalities in the disjunctive normal form of ϕ. By Proposition 4.4, for every S i there exist systems S i,j : A i,j • y ≥ c i,j ∧ B i,j • y > d i,j , j ∈ J i , such that π y S i = j∈Ji S i,j , and S i,j ≤ poly( S i ). Consequently, ψ(y) def = i∈I j∈Ji A i,j • y ≥ c i,j ∧ B i,j • y > d i,j has the desired properties.

The Inclusion Problem

Given continuous Petri nets N , M with the same set of places and initial markings m, m , inclusion asks whether every marking m reachable from m in N is also reachable in M from m . Recall the logical definition of inclusion provided in Table I

given as Φ N ,M inc (x, x ) def = ∀x : Φ N (x, x ) → Φ M (x , x ).
Here, we improve the EXP upper bound developed by [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF] and the immediate Π P 2 -upper bound from Proposition 2.5, and show that the coNP lower bound given by [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF] is actually tight. PROPOSITION 4.6. Inclusion for continuous Petri nets is coNP-complete.

PROOF. For fixed initial markings m, m , using standard transformations and renaming of variables, we have that

Φ N ,M inc (m, m ) is equivalent to a Π 2 -sentence ϕ = ∀x : ∃y : ψ(x, y) such that ψ(x, y) ≤ |Φ N ,M inc (m, m )| ≤ poly(|M| + |N | + m + m )
. By Corollary 4.5, there is ψ (x) such that ϕ ≡ ∀x : ψ (x) and ψ (x) ≤ poly ψ(x, y) . Hence, if ϕ is invalid it follows from Proposition 4.2 that there exists some witness v such that ψ (v) does not hold and v ≤ poly( ψ (x) ).

Consequently, an NP algorithm deciding non-inclusion proceeds as follows: guess a v such that v ≤ poly(|M|+|N |+ m + m ), and by Proposition 2.4 verify in polynomial time that (m, v) ∈ QR(N ) and (m, v) / ∈ QR(M). Hence, inclusion for continuous Petri nets is in coNP.

Remark 4.7. It is worth mentioning that Proposition 4.6 additionally yields a coNPcompleteness result for reversibility of a continuous Petri net. Given a Petri net N and a configuration m, reversibility is to decide whether QR(N )(m) ⊆ QR(N -1 )(m) holds. This problem is coNP-hard [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF] and by Proposition 4.6 in coNP, hence coNP-complete.

ε-Liveness Problems

Given a continuous Petri net N and a marking m, recall that the ε-liveness problem asks whether there exists an ε > 0 such that for every marking m reachable from m and every transition t ∈ T , a marking m is reachable such that t has enabling degree at least ε in m . Recall the logical definition from Table I:

Φ N lv (x) def = ∃ε : ε > 0 ∧ ∀x : Φ N (x, x ) → t∈T ∃x : Φ N (x , x ) ∧ Φ N ,t nbld (ε, x ) .
Structural ε-liveness asks whether there exists some initial marking m such that N is ε-live in m, i.e., whether

Φ N slv def = ∃x : Φ N lv (x) is valid.
To the best of our knowledge, the following is the first decidability and complexity result for (structural) ε-liveness.

PROPOSITION 4.8. ε-Liveness and structural ε-liveness are decidable in Σ P 3 . PROOF. Inspecting Φ N slv , we see that it is a Σ 3 -sentence in FO Q, +, < . Consequently, an application of Proposition 2.5 yields the desired upper bounds.

Unfortunately, there does not seem to be an obvious way to decrease those upper bounds, though we suspect them not to be tight. The precise complexity of (structural) ε-liveness remains an open problem of this paper.

Home-State Problems

Given a continuous Petri net N and an initial marking m, a marking m is a home state if m can be reached from every marking m that can be reached from m. The existential home-state problem is to decide whether there exists a home state for a given initial marking m. Again, we recall the logical definitions of those problems from Table I

: Φ N hm (x, x ) def = ∀x : Φ N (x, x ) → Φ N (x , x
) for the home-state problem, and Φ N ehm (x) def = ∃x : Φ hm (x, x ) for the existential home-state problem.

PROPOSITION 4.9. The home-state problem for continuous Petri nets is coNPcomplete.

PROOF. The home-state problem can be rephrased as an inclusion problem. We have that m is a home state if and only if QR(N )(m) ⊆ QR(N -1 )(m ). Consequently, by Proposition 4.6, it is decidable in coNP.

To show coNP-hardness of the home-state problem, we adapt a reduction from 3-SAT used by Fraca and Haddad [2015, Prop. 34] and Desel and Esparza [1995, Thm. 4.28] to show that the liveness problem is coNP-complete, respectively, for continuous and discrete free-choice Petri nets. Let ϕ be a formula in 3-CNF with k variables x 1 , x 2 , . . . , x k and m clauses C 1 , C 2 , . . . , C m . For each clause C j , we define j,1 , j,2 and j,3 as its three literals. Consider the continuous Petri net N obtained from ϕ as follows:

-for every 1 ≤ i ≤ k, we add a place p i initially marked by the marking m 0 , and transitions t i and f i that both have p i as an their sole input place; -for every 1 ≤ j ≤ m, we add empty places q j,1 , q j,2 , q j,3 such that q j,b is an output place of t i if q j,b = ¬x i or an output place of f i if q j,b = x i ; -for every 1 ≤ j ≤ m, we add a transition c j with q j,1 , q j,2 and q j,3 as its only input places.

-we add an empty place p main as the output place of c 1 , c 2 , . . . , c m .

It was shown by Fraca and Haddad [2015, Prop. 34] that ϕ is unsatisfiable if, and only if, for every marking m reachable from m 0 in N , there exists a marking m reachable from m such that m (p main ) > 0.

We exploit this observation to obtain a reduction to the home-state problem. Let N be the continuous Petri net obtained from N as follows:

-we add a transition t dec that removes two tokens from p main and adds one token to p main ; -we add a transition t inc that removes one token from p main and adds two token to p main ; -for every place p = p main from N , we add a transition t p with input places p and p main , and output place p main .

Let m be a marking such that m(p main ) > 0. It is not so difficult to see that it is possible to increase or decrease m(p main ) to any positive value, but never to 0; in particular, a marking of p main with value 1 can always be reached. Moreover, from m, any place p = p main can reach zero by executing t p by the appropriate amount. Therefore, if ϕ is unsatisfiable, by the above observation on N , any marking reachable from m 0 can reach a marking with a non-zero value in p main . Moreover, by construction of N , any marking with a non-zero value in p main can lead to a marking where all of the other places are emptied, and then where p main is set to 1.

Let m home be the marking of N defined by m home (p) = 1 if p = p main and 0 otherwise. We conclude that ϕ is unsatisfiable if, and only if, m home is a home state of N .

PROPOSITION 4.10. The existential home-state problem is decidable in Σ P 2 . PROOF. For a fixed initial marking m, by repeated quantifier elimination we have that Φ N ehm (m) ≡ ∃x : ψ(x) for some ψ(x) such that ψ(x) ≤ poly( Φ N ehm (m) ) ≤ poly(|N | + m ). Consequently, it follows from Proposition 4.2 that if there exists a home state m then there is one, say v, such that v ≤ poly(|N | + m ). Hence, v can be guessed in NP, and using a coNP oracle it can be verified that v is indeed a home state with respect to the initial marking m.

As remarked by [START_REF] Jančar | Deciding Structural Liveness of Petri Nets[END_REF], structural versions of Petri-net decision problems are often easier to decide, as is exemplified by the structural boundedness problem for discrete Petri nets. This problem is solvable in P, see e.g. [START_REF] Thoen | Modeling, verification and exploration of task-level concurrency in real-time embedded systems[END_REF], whereas boundedness is EXPSPACE-complete [START_REF] Lipton | The Reachability Problem Requires Exponential Space[END_REF][START_REF] Rackoff | The Covering and Boundedness Problems for Vector Addition Systems[END_REF]. It does not seem inconceivable that the existential home-state problem can be decided with lower complexity.

COVERABILITY IN PETRI NETS VIA REACHABILITY IN CONTINUOUS PETRI NETS

Recall that, given a (continuous or discrete) Petri net N , an initial marking m 0 and a target marking m, the coverability problem asks whether m is coverable from m 0 in N , i.e., whether m 0 -→ * m for some marking m ≥ m. The coverability problem was one of the first decision problems shown decidable for discrete Petri nets [START_REF] Karp | Parallel Program Schemata: A Mathematical Model for Parallel Computation[END_REF][START_REF] Henri | Decidability questions for Petri Nets[END_REF]]. In the approach pioneered by Karp and Miller, a finite tree representing markings coverable from m 0 is constructed. This tree is obtained from building the reachability tree starting from the initial marking m 0 and computing so-called accelerations whenever a node has a smaller or equal ancestor. The scalability of this approach is limited since the size of this tree may be non-primitive recursive. Nevertheless, heuristics have been investigated that keep the size of the tree manageable in practice, see e.g. [START_REF] Geeraerts | On the Efficient Computation of the Minimal Coverability Set of Petri Nets[END_REF][START_REF] Reynier | Minimal Coverability Set for Petri Nets: Karp and Miller Algorithm with Pruning[END_REF][START_REF] Valmari | Old and New Algorithms for Minimal Coverability Sets[END_REF].

Another popular approach for solving the coverability problem, namely the backward approach, that forms the basis of the approach that we present in this paper, was introduced by [START_REF] Arnold | Récursivit et cônes rationnels fermés par intersection[END_REF] for vector addition systems with resets, and first formalized and popularized by [START_REF] Parosh | General Decidability Theorems for Infinite-State Systems[END_REF] in the more general context of well-structured transition systems. This approach is based on an algorithm that begins with the target marking m and iteratively computes predecessors of m from which a marking larger or equal to m may be reached; hence its name, the backward algorithm. A bottleneck of the backward algorithm is that its number of iterations may be doubly exponential in the worst case [START_REF] Bozzelli | Complexity Analysis of the Backward Coverability Algorithm for VASS[END_REF]. In particular, as the set of predecessors computed by the algorithm may also grow doubly exponentially [START_REF] Bozzelli | Complexity Analysis of the Backward Coverability Algorithm for VASS[END_REF], computations tend to become much slower as the number of iterations increases, even on Petri nets of relatively modest size.

In this section, we show how to speedup computations of the backward algorithm by exploiting reachability in continuous Petri nets as a pruning criterion. That is, in every iteration of the backward algorithm, we use the over approximation provided by continuous Petri nets in order to discard all predecessors which define a set of configurations which are not coverable in the continuous semantics. A cornerstone of the empirical performance of our approach is that the logical characterization of reachability in continuous Petri nets enables us to employ SMT-solvers in our prototype implementation for those purposes.

This section is structured as follows. In Section 5.1, we introduce some auxiliary definitions and recall the backward algorithm. Subsequently, in Section 5.2 we develop our variant of the backward algorithm in which Q-coverability is used as a pruning criterion. Section 5.3 describes an implementation and the evaluation of the algorithm developed in Section 5.2. Finally, in Section 5.4 we discuss the relationship of our variant of the backward algorithm to approaches that have appeared in the literature.

The Backward Algorithm

We first present the classical backward algorithm and introduce some auxiliary definitions. A set V ⊆ N P is upward-closed if for every v ∈ V and w ∈ N P , v ≤ w implies w ∈ V . The upward closure of a vector v ∈ N P is the set

↑v def = {w ∈ N P : v ≤ w}.
This definition can be lifted to sets V ⊆ N P in the obvious way, i.e., ↑V def = v∈V ↑v. Due to N P being well-quasi-ordered by ≤, any upward-closed set V contains a finite subset F ⊆ V such that V = ↑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 ⊆ V that is minimal with respect to inclusion for all bases F ⊆ V . We use minbase(V ) to denote this minimal basis. For any finite basis F of V , minbase(V ) is obtained by deleting vectors v ∈ F such that there exists w ∈ F with w < v. For a Petri net N = (P, T, Pre, Post) and a set of markings M , we define pred (M ) as the set of predecessors of M , i.e., pred (M )

def = {m ∈ N P : m t - → m for some t ∈ T, m ∈ M }. Note that for every upward-closed set M , pred (M ) is upward-closed.
Formally, the backward algorithm computes a sequence

M 0 , M 1 , M 2 , . . . (3)
such that ↑M 0 = ↑m and ↑M i = pred (↑M i-1 ) for every i > 0. Since Petri nets are well-structured, (3) stabilizes to some M n such that ↑M n = {x ∈ N P : x -→ * ALGORITHM 1: Backward algorithm solving the coverability problem for Petri nets.

Input: Petri net N = (P, T, Pre, Post) and m0, m ∈ N P . Output: Does there exist m ∈ ↑m such that m0 -→ * m ? 1 M ← {m} 2 while m0 ∈ ↑M do m for some m ≥ m} (see e.g. [START_REF] Parosh | General Decidability Theorems for Infinite-State Systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF]). Therefore, the target marking m is coverable from the initial marking m 0 if, and only if, m 0 ∈ ↑M n .

We detail the backward algorithm in Algorithm 1. Each upward-closed set ↑M i is represented by its unique minimal basis M i . Moreover, to implement the computation of pred (↑M i-1 ), we follow [START_REF] Finkel | Recent and simple algorithms for Petri nets[END_REF]. We associate to each marking v ∈ N P and each transition t ∈ T the marking v t defined by

v t (p) def = max{Pre(p, t), v(p) -Incid(p, t)} for every p ∈ P.
It is possible to verify that {v t } is the minimal basis of markings covering v after firing t, i.e.

{v t } = minbase({u ∈ N P : there is v ∈ ↑v such that u t - → v }).
Let V ⊆ N P , we let pb(V ) def = u∈V,t∈T {u t }, which allows us to obtain the potentially non-minimal finite basis pb(V ) of pred (↑V ), i.e.

↑pb(V ) = {u ∈ N P : there is v ∈ ↑V such that u - → v } = pred (↑V ).

The Backward Algorithm Modulo Q-Coverability

We now present our extension of the classical backward algorithm that incorporates Q-coverability checks during its execution in order to keep the set of minimal basis elements small. This algorithm is detailed in Algorithm 2. Blue font color indicates differences to Algorithm 1.

Let N be a Petri net, m 0 an initial marking and m a target marking to cover. On Line 1, we first test whether m is Q-coverable from m 0 . If it is the case, on Line 3, we derive an open formula ψ(x) from Φ N cvr (m 0 , x) from Table I such that ψ(x) holds if and only if x is Q-coverable in N . On Lines 6 and 7, we prune new markings, i.e., markings from B that are not Q-coverable from m 0 , and that would have thus never led to m 0 in subsequent iterations. PROPOSITION 5.1. Let N = (P, T, Pre, Post) be a Petri net and m 0 , m ∈ N P . Algorithm 2 always halts, and returns "true" if, and only if, m is coverable from m 0 .

The Logical View on Continuous Petri Nets A:19 ALGORITHM 2: Backward algorithm modulo Q-coverability.

Input: Petri net N = (P, T, Pre, Post) and m0, m ∈ N P . Output: Does there exist m ∈ ↑m such that m0 -→ * m ? PROOF. Let B n and M n be respectively the values of B and M on Lines 7 and 11 of Algorithm 2 in the n-th iteration of the while loop. We note that

1 if m is not Q-coverable from m0 then return false 2 M ← {m} 3 ψ(x) ← Φ N cvr (m0, x) 4 while m0 ∈ ↑M do 5 B ← pb(M ) \ ↑M 6 D ← {v ∈ B : ¬ψ(v)} 7 B ← B \ D 8 if B = ∅ then
↑M n = x ∈ N P : m 0 - → * Q x and x k -→ y for some x ≥ x, y ≥ m and 0 ≤ k ≤ n , B n ⊆ ↑M n \ ↑M n-1 .
Moreover, we have that m is coverable from m 0 if, and only if, m is Q-coverable from m 0 and there is y ∈ ↑m such that m 0 -→ * y. Therefore, by definition of Lines 9 and 14, the algorithm is correct.

Since ≤ is a well-quasi-order for N P , we know that the sequence ↑M 1 ⊆ ↑M 2 ⊆ . . . stabilizes after a finite number of iterations n. Thus, after n iterations, either B = ∅ on Line 8, or m 0 ∈ ↑M on Line 4. In both cases, the algorithm halts. Therefore, it always halts.

QCover: An Implementation of the Backward Algorithm Modulo Q-Coverability

In this section, we provide an empirical evaluation of Algorithm 2 on a benchmark set from the literature. In Section 5.3.1, we discuss some details of our implementation, and in Section 5.3.2 we compare QCOVER against various tools from the literature. 5.3.1. Implementation Details. We have implemented the backward algorithm modulo Q-coverability in a tool called QCOVER2 in the programming language PYTHON. Petri Nets are represented by their Pre and Post matrices with the NUMPY3 library. QCOVER also supports sparse matrices representation for very large Petri nets through SCIPY4 . The input file format of coverability instances for QCOVER is a strict subset of the MIST file format 5 .

In order to achieve a better performance, for a given coverability instance we first use a single pass of the polynomial-time algorithm of [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF] in order to discharge instances which are not Q-coverable. If the instance is Q-coverable, we resort to Algorithm 2. In order to check satisfiability of ψ(x), we make use of the SMT solver Z3 [de Moura and Bjørner 2008], and we additionally interpret variables over N instead of Q + with the goal of pruning more markings. The reason why we do not use the polynomial-time algorithm of [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF] throughout the whole while-loop of Algorithm 2 is that on a single instance, this algorithm is usually faster, however when running multiple Q-coverability queries on the same Petri net, caching strategies in Z3 yield a speed-up that cannot be achieved by any other means.

5.3.2. Benchmarks. We evaluated QCOVER on 176 systems modeled by Petri nets and coverability queries. This set of systems was used by [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF] in order to benchmark the tool PETRINIZER presented therein, and is composed of the following five suites:

mist: 27 systems drawn from the literature (mutual exclusion protocols, communication protocols, etc.) and used, in particular, to evaluate MIST6 ; bfc: 46 systems obtained from concurrent C programs (multi-threaded programs with shared-memory, pseudorandom number generators, mutual exclusion protocols, etc.) and used, in particular, to test BFC7 [START_REF] Kaiser | Efficient Coverability Analysis by Proof Minimization[END_REF][START_REF] Kaiser | A Widening Approach to Multithreaded Program Verification[END_REF]]; soter: 50 systems obtained from concurrent ERLANG programs and used, in particular, by D'Osualdo et al. [2013] to test SOTER [START_REF] Emanuele | Soter: an automatic safety verifier for Erlang[END_REF]], a tool built on top of BFC; medical: 12 systems, described by [START_REF] Majumdar | Static Provenance Verification for Message Passing Programs[END_REF], modeling provenance analysis of messages of a simple medical messaging system of Vanderbilt University Medical Center; bug tracking: 41 systems, described by [START_REF] Majumdar | Static Provenance Verification for Message Passing Programs[END_REF], modeling provenance analysis of messages of a bug-tracking system [START_REF] Jank | Issue Tracking Systems[END_REF]].

As detailed in Table II, roughly two-thirds of the systems are safe (i.e., they are a no-instances of coverability). On average, the Petri nets used for the evaluation have 1054 places and 8458 transitions.

In order to evaluate our tool, we executed QCOVER and three other tools on the 176 systems with a timeout of 2000 secs. (33min and 20s) per instance. We compared QCOVER with the following tools: PETRINIZER [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF], MIST [START_REF] Ganty | Algorithmes et structures de données efficaces pour la manipulation de contraintes sur les intervalles[END_REF] and BFC [START_REF] Kaiser | Efficient Coverability Analysis by Proof Minimization[END_REF][START_REF] Kaiser | A Widening Approach to Multithreaded Program Verification[END_REF] in their latest versions available at the time of writing [START_REF] Blondin | Approaching the Coverability Problem Continuously[END_REF]. MIST implements a number of algorithms, we used the backward algorithm8 that uses places invariant pruning [START_REF] Ganty | Symbolic Data Structure for sets of k-uples[END_REF]. All benchmarks were performed on a single computer equipped with four Intel R Core TM 2.00 GHz i7-4510U CPUs, 8 GB of memory and Ubuntu Linux 14.04 (64 bits).

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.

Table III consists of 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. Our algorithm outperforms all competitors on safe instances, since in this case a proof of safety (i.e. non-coverability) effectively requires the computation of the whole backward coverability set, and this is where pruning via Q-coverability becomes most beneficial. On the other hand, QCOVER remains competitive on unsafe instances, though a tool such as BFC handles those instances better since its heuristics are more suited for disproving safety (i.e. coverability). Nevertheless, QCOVER is the overall winner when comparing the number of safe and unsafe instances decided, being far ahead at the top of the leader board deciding 142 out of 176 instances. QCOVER not only decides more instances, it often does so faster than its competitors. Figure 2 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.

Finally, we consider the effectiveness of using Q-coverability as a pruning criterion. To this end, consider Figure 3 in which we plotted the number of times a certain percentage of basis elements was removed due to not being Q-coverable. Impressively, in some cases more than 95% of the basis elements get discarded. Overall, the average and the median proportion of basis elements discarded are respectively 56% and 59%, which substantiates the usefulness of using Q-coverability as a pruning criterion.

Before we conclude, let us mention that already 83 instances are proven safe by only checking the state equation, and that additionally checking for the Conditions (ii) and (iii) of Proposition 3.1 increases this number to 101 instances. If we use the polynomial-time algorithm of [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF] instead of our FO Q, +, < encoding then we can only decide 132 instances in total (within the set time limit). Finally, in our experiments, interpreting variables over Q + instead of N resulted in no measurable overall performance gain.

Concluding, our experimental evaluation demonstrates that the backward algorithm modulo Q-reachability approach to the Petri net coverability problem developed in this paper is highly efficient when run on real-world instances, and superior to existing tools and approaches when compared on standard benchmarks from the literature.

Relationship to Other Approaches from the Literature

The approach for deciding coverability in Petri nets presented in the previous sections is primarily related to the work by [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF]; by [START_REF] Kaiser | A Widening Approach to Multithreaded Program Verification[END_REF]; and by [START_REF] Delzanno | Attacking Symbolic State Explosion[END_REF]. [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF] presented an implementation of a semi-decision procedure for disproving coverability. This semi-decision procedure was originally proposed by [START_REF] Esparza | Verification of Safety Properties Using Integer Programming: Beyond the State Equation[END_REF] and is based on the Petri-net state equation and traps as sufficient criteria in order to witness non-coverability. As shown by [START_REF] Esparza | Verification of Safety Properties Using Integer Programming: Beyond the State Equation[END_REF], those conditions can be encoded into an equi-satisfiable system of linear inequalities called the trap inequation. This approach is, however, prone to numerical imprecisions that become problematic even for instances of small size [Esparza and Melzer 2000, Sec. 5.3]. For that reason, [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF] resort to a CEGAR-based variant of the trap inequation approach which has the drawback that in the worst case, the CEGAR loop has to be executed an exponential number of times leading to an exponential number of queries to the underlying SMT-solver. We will show in Section 5.4.1 that the conditions used by [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF] are strictly subsumed by a subset of the conditions required to witness coverability in continuous Petri nets: whenever the procedure described therei returns uncoverable then coverability does not hold in the continuous setting either, but not vice versa. Thus, a single satisfiability check to our formula in existential FO Q + , +, < encoding continuous coverability that we developed in this paper completely subsumes the CEGAR-approach presented by [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF]. Another difference is that we presented a sound and complete decision procedure.

Regarding the relationship of our work with the work of [START_REF] Kaiser | A Widening Approach to Multithreaded Program Verification[END_REF], they present an approach to coverability in richer classes of well-structured transition systems that is also based on the backward algorithm. They additionally employ 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 the approach of [START_REF] Kaiser | A Widening Approach to Multithreaded Program Verification[END_REF] is needed, which is required when the widened basis turns out to be too inaccurate.

The idea of using an over approximation of the reachability set of a Petri net in order to prune minimal basis elements inside the backward algorithm was first described by [START_REF] Delzanno | Attacking Symbolic State Explosion[END_REF], where place invariants are used as a pruning criterion. However, computing such invariants and checking if a minimal basis element can be pruned potentially requires exponential time.

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

5.4.1. Relationship to the Approach of Esparza et al. [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF] presented a semidecision procedure for coverability that employs the Petri net state equation and trap constraints inside a CEGAR-framework. Here we discuss in some more detail similarities and differences between our approach and the one of [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF].

Let N = (P, T, Pre, Post) be a Petri net. A trap in N is a non-empty subset of places

Q ⊆ P such that Q • ⊆ • Q, and Q ⊆ P is a siphon in N whenever • Q ⊆ Q • .
We say that a trap (respectively siphon) is marked by a marking m if p∈Q m(p) > 0. An important property of marked traps is that they may never become unmarked, i.e., if a trap is marked by some marking m, then it will remain marked after any firing sequence starting in m. Conversely, when a siphon is unmarked in some marking m, it remains so after any firing sequence starting in m. By definition, Q is a trap in N if, and only if, Q is a siphon in N -1 .

The coverability criteria that [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF] build upon are derived from the work of [START_REF] Esparza | Verification of Safety Properties Using Integer Programming: Beyond the State Equation[END_REF] and can be summarized as follows: PROPOSITION 5.2 ([ESPARZA ET AL. 2014]). Let N = (P, T, Pre, Post) be a discrete (resp. continuous) Petri net, and m 0 , m ∈ N P (resp. ∈ Q

P + ). If m 0 - → * m then there exists y ∈ N T (resp. ∈ Q T + ) such that (i) m = m 0 + Incid • y, and (ii) for every trap Q ⊆ P , if Q is marked by m 0 , then Q is marked by m.
In the approach of [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF], it is checked whether the conditions of Proposition 5.2 are fulfilled. To this end, the for-all quantifier is replaced by incrementally enumerating all traps in a CEGAR-style fashion. If either condition is violated the semi-decision procedure returns "uncoverable", and "don't know" otherwise. We show that the criteria of Proposition 3.1 imply those of Proposition 5.2: PROPOSITION 5.3. Let N = (P, T, Pre, Post) be a continuous Petri net, and let m 0 , m ∈ Q P + . If N , m 0 , m satisfy Conditions (i) and (iii) of Proposition 3.1, then they also satisfy Conditions (i) and (ii) of Proposition 5.2.

PROOF. We proceed by contraposition, i.e., we show that if for every y ∈ Q T + , one of the conditions of Proposition 5.2 is not satisfied, then for every y ∈ Q T + , one of conditions (i) or (iii) of Proposition 3.1 is not satisfied.

Let y ∈ Q T + . Suppose that y does not satisfy Condition (i) of Proposition 5.2. Since this condition is identical to Condition (i) of Proposition 3.1, we are done. Therefore, we may assume that y satisfies Condition (i) of Proposition 5.2, i.e.,

m = m 0 + Incid • y , (4)
but not its Condition (ii). Thus, there exists a trap Q ⊆ P in N marked by m 0 , but not marked by m. We note that Q is a siphon in N -1 marked by m 0 , but not marked by m. Let T def = y ,

P def = • T • and Q def = Q ∩ P . We claim that Q is a siphon in N -1
T that is not marked by m.

(5)

From this claim, we are done. Indeed, by [Fraca and Haddad 2015, Prop. 18], Claim (5) implies that T ∈ fs(N -1 T , m). Consequently, y ∈ fs(N -1 , m), hence Condition (iii) of Proposition 3.1 is not satisfied.

Let us prove Claim (5). Since Q is not marked by m, Q ⊆ Q is also not marked by m. Let t ∈ T be such that t ∈ • Q . Since Q ⊆ Q, we also have that t ∈ • Q. Moreover, since Q is siphon in N -1 , we have that t ∈ Q • . By definition, t ∈ P • , hence t ∈ Q • ∩ P • and consequently t ∈ Q • . Therefore, • Q ⊆ Q • . In order to show that Q is indeed a siphon, it remains to show that Q = ∅. Since Q is marked by m 0 , but not by m, there exists p ∈ Q such that m 0 (p) > 0 and m(p) = 0. By ( 4 Since m 0 (p) > 0, there exists some t ∈ T such that Incid(p, t) < 0. Therefore, p ∈ • t • , whence p ∈ P . Consequently p ∈ Q ∩ P = Q , which concludes the proof.

In fact, we may strengthen the previous proposition by showing that Proposition 3.1 is stronger than Proposition 5.2: PROPOSITION 5.4. There exists a continuous Petri net N = (P, T, Pre, Post), and markings m 0 , m ∈ Q P + satisfying the conditions of Proposition 5.2, but not satisfying the Conditions (i) and (iii) of Proposition 3.1.

The Logical View on Continuous Petri Nets

A:25 PROOF. Let N = ({p, q}, {s, t}, Pre, Post) be the continuous Petri net depicted in Figure 4, m 0 = (1, 0) and m = (0, 1). We note that m is not reachable from m 0 . Indeed, the unique solution to m = m 0 + Incid • y is y = (0, 1), yet it is impossible to fully fire t in m 0 . The unique trap of N is {q} and it is not marked by m 0 . Therefore, N , m 0 and m satisfy conditions of Proposition 5.2. Suppose that Conditions (i) and (iii) of Proposition 3.1 are satisfied. They must be satisfied by the unique solution y = (0, 1). Thus, {t} = y ∈ fs N -1 (m). By [Fraca and Haddad 2015, Prop. 18], N -1 {t} does not possess any siphon marked by m. Yet, {q} is a siphon in N -1 {t} marked by m. This is contradiction, hence Conditions (i) and (iii) of Proposition 3.1 are not satisfied.

The previous proposition shows that the single formula stated in Proposition 3.2 strictly subsumes the approach of [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF]. Moreover, it provides a theoretical justification for why the approach of [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF] performs so well in practice: the conditions are a strict subset of the conditions developed by [START_REF] Fraca | Complexity Analysis of Continuous Petri Nets[END_REF] for Q-reachability.

CONCLUSION

In this paper, we developed a characterization of the reachability relation for continuous Petri nets in existential FO Q, +, < . Given a Petri net N , we showed how to compute in linear time a formula Φ N (x, x ) whose set of solutions defines the continuous reachability relation of N . Using this characterization as a starting point, we derived novel upper bounds for standard decision problem for continuous Petri nets, such as inclusion, (structural) ε-liveness, and the (existential) home state problem. Moreover, we showed how to integrate continuous coverability checks as a pruning heuristic inside the backward algorithm for deciding coverability in discrete Petri nets. In particular, the logical characterization of continuous reachability enables the use of SMT solvers in order to decide continuous coverability, and in effect we obtained a decision procedure for the Petri net coverability problem that outperforms all its competitors on standard benchmarks from the literature. At the time of writing, [START_REF] Geffroy | Occam's Razor Applied to the Petri Net Coverability Problem[END_REF] have adjusted our encoding of continuous reachability to specifically target continuous coverability, and reported a two-fold speed-up on the benchmarks used in this paper.

Using pruning invariants inside the backward algorithm is not a novelty as such and was first described by [START_REF] Delzanno | Attacking Symbolic State Explosion[END_REF]. However, we believe that this paper demonstrates that the significant progress on SMT solvers that has taken place over the last fifteen years provides new perspectives on developing and applying invariants which are definable in a logical theory that an SMT solver can handle. In particular, over approximations of reachability sets via arithmetic theories have been developed for even more expressive models, for instance for Petri nets with resets [START_REF] Chistikov | Context-free commutative grammars with integer counters and resets[END_REF] for which coverability is Ackermann-complete [START_REF] Schnoebelen | Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets[END_REF]], and could directly be integrated inside the backward algorithm as proposed in this paper (provided that those more expressive models are well structured). We believe that this approach will enable the practical algorithmic analysis of models that have mostly been studied from a theoretical perspective due to the high worst-case complexity of their decision problems.

  by S we denote the system of linear inequalities S :( A B ) • x ≥ ( c d ), whose set of solutions is the topological closure of the solutions of S. PROPOSITION 4.2. Let S : A•x ≥ c∧B•x > d be a system of mixed linear inequalities and strict inequalities such that S = ∅. Then there is v ∈ S such that v ≤ poly( S ).PROOF. Let A and B be m × n and m × n matrices, respectively. Let z ∈ S , and consequently z ∈ S . By Proposition 4.1,

3 B

 3

Fig. 2 .Fig. 3 .

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

  ), m = m 0 + Incid • y. Thus,0 = m 0 (p) + (Incid • y)(p) = m 0 (p) + t∈T Incid(p, t) • y(t) = m 0 (p) + t∈ y Incid(p, t) • y(t) (since y(t) = 0 for t ∈ y ) = m 0 (p) + t∈T Incid(p, t) • y(t)(by T = y ).

Fig. 4 .

 4 Fig. 4. Example of continuous Petri net for which the conditions of Proposition 5.2 are not sufficient to certify non-reachability.

  Examples of Petri nets N 1 , N 2 and N 3 showing that boundedness, inclusion, liveness and home states problems cannot be over approximated by the continuous semantics. The rightmost Petri net is borrowed from[START_REF] Recalde | Autonomous Continuous P/T Systems[END_REF].

	The Logical View on Continuous Petri Nets				A:11
								t
								3
	p	2	r	q	p	s	q	p	q
								u
		2						2
	Fig. 1.

Table II .

 II Left: number of safe and unsafe systems for each suite. Right: Petri nets average number of places and transitions for each suite.

	Suite	Safe	Unsafe	Total	Suite	Avg. num. of places	Avg. num. of transitions
	mist	23	4	27	mist	43	69
	bfc	2	44	46	bfc	207	1,350
	soter	38	12	50	soter	2,805	4,985
	medical	12	0	12	medical	312	5,431
	bug tracking	40	1	41	bug tracking	754	27,370
	Total	115	61	176	Total	1,054	8,458

Table III .

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

	Suite	QCOVER	PETRINIZER	MIST	BFC	Total		Suite	QCOVER	PETRINIZER	MIST	BFC	Total
	mist	23	20	22	20	23		mist	3		-	4	4	4
	medical	11	4	11	3	12	medical	-		-	-	-	0
	bfc	2	2	2	2	2		bfc	26		-	29	42	44
	bug tracking	32	32	0	19	40	bug tracking	0		-	0	1	1
	soter	37	37	0	19	38	soter	8		-	6	12	12
	Total	105	95	35	63	115		Total	37		0	39	59	61
				Suite	QCOVER	PETRINIZER	MIST	BFC	Total
				mist	26		20	26	24	27
			medical	11		4	11	3	12
				bfc	28		2	31	44	46
			bug tracking	32		32	0	20	41
			soter	45		37	6	31	50
				Total	142		95	74	122	176

ACM Transactions on Computational Logic, Vol. V, No. N, Article A, Publication date: January YYYY.

In fact, the original definition of[START_REF] David | Continuous Petri nets[END_REF] allows for real numbers, hence the name continuous Petri nets. However for studying decidability and complexity issues, rational numbers are more convenient.ACM Transactions on Computational Logic, Vol. V, No. N, Article A, Publication date: January YYYY.

QCOVER is available at https://github.com/blondimi/qcover/.

NUMPY is available at http://www.numpy.org/.

SCIPY is available at http://www.scipy.org/scipylib/.

See https://github.com/pierreganty/mist/wiki#input-format-of-mist. Note that this format supports counter machines more general than Petri nets; QCOVER only supports a strict subset corresponding to Petri nets.ACM Transactions on Computational Logic, Vol. V, No. N, Article A, Publication date: January YYYY.

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

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

See backward at https://github.com/pierreganty/mist/wiki#coverability-checkers-included-in-mist.ACM Transactions on Computational Logic, Vol. V, No. N, Article A, Publication date: January YYYY.

ACKNOWLEDGMENTS

We would like to thank Vincent Antaki for an early implementation of the polynomial-time algorithm of Fraca and Haddad [2015], and also Gilles Geeraerts for his support with the MIST file format. We are grateful to the anonymous reviewers of TACAS'16 and ACM TOCL for their comments and suggestions.

M. Blondin was supported by the Fonds de recherche du Québec -Nature et technologies (FRQNT), by the French Centre national de la recherche scientifique (CNRS), and by the "Chaire Digiteo, ENS Cachan -École Polytechnique". C. Haase was supported by Labex Digicosme, Univ. Paris-Saclay, project VERI-CONISS. S. Haddad was supported by the ERC project EQualIS (FP7-308087).