Khalil Ghorbal
email: kghorbal@cs.cmu.edu

Andrew Sogokon
email: a.sogokon@sms.ed.ac.uk

André Platzer
email: aplatzer@cs.cmu.edu

A Hierarchy of Proof Rules for Checking Positive Invariance of Algebraic and Semi-Algebraic Sets $

Keywords: Formal Verification, Polynomial Differential Equations, Positive Invariance, Deductive Power, Dynamical Systems

This paper studies sound proof rules for checking positive invariance of algebraic and semi-algebraic sets, that is, sets satisfying polynomial equalities and those satisfying finite boolean combinations of polynomial equalities and inequalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the trade-off between proof rule generality and practical performance and evaluate our theoretical observations on a set of benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship is interesting.

Introduction

In safety verification of dynamical systems, one is typically concerned with ensuring that by initializing a system in some set of states X 0 ⊆ X (where X is the state space), the system will never evolve into an unsafe state (belonging to some X u ⊆ X). When the system is given by ordinary differential equations, one may attempt to solve the safety verification problem by showing that the solution to the initial value problem for any initial value x 0 ∈ X 0 cannot enter the unsafe region, that is x(x 0 , t) / ∈ X u for all t ≥ 0, where x(x 0 , t) is the state of the system at time t w.r.t. the initial value x 0 . The safety verification problem is in this case equivalent to showing that the intersection of the reachable set {x(x 0 , t) ∈ X | t ≥ 0} with the set of unsafe states is empty. However, solutions to ordinary differential equations will rarely be available in closed form1 ; even when they are, their description will often be much more involved than that of the differential equations themselves. Instead, it is possible to work with the differential equations directly [START_REF] Sankaranarayanan | Constructing invariants for hybrid systems[END_REF][START_REF] Platzer | Differential-algebraic dynamic logic for differential-algebraic programs[END_REF]Platzer, , 2012a;;[START_REF] Tiwari | Abstractions for hybrid systems[END_REF].

A fundamental notion in safety verification is that of a (positively) invariant set. In fact, exact reachable sets of any given state x 0 of the system are the smallest positively invariant sets one can hope to find that include x 0 . However, obtaining and working with exact descriptions of reachable sets is not always practical or even possible. This does not mean that system safety cannot be established by other means -if one finds a larger positively invariant set, I ⊆ X, with a simpler (preferably algebraic, or semi-algebraic) description and which (i) contains the set of initial states (i.e. X 0 ⊆ I) and (ii) does not intersect the set of unsafe states (i.e. I ∩ X u = ∅), then one can soundly conclude that the system is safe.

We focus on methods for checking whether a given set defines a positively invariant region, i.e. one from which no system trajectory can escape in positive time (t ≥ 0). In particular, we consider the important case of algebraic and semi-algebraic sets, i.e. sets that can be defined by polynomial equations and finite boolean combinations of polynomial equations and inequalities, respectively. We review previously reported methods and introduce extensions to automatically check positive invariance of semi-algebraic sets. Our work aims at identifying sweetspots in the various methods in order to suggest efficient strategies for invariant checking inside a deductive prover.

Contributions. We extend our earlier analysis presented in [START_REF] Ghorbal | A hierarchy of proof rules for checking differential invariance of algebraic sets[END_REF] to include proof rules that are concerned with checking positive invariance of semi-algebraic sets. In addition to recalling proof rules reported previously, we introduce in Section 5.2 a new sufficient condition that we term NSSBC for Nonsmooth Strict Barrier Certificate. NSSBC is able to prove positive invariance in a special class of closed semi-algebraic sets and can be seen as a generalization of strict barrier certificates introduced by Prajna [START_REF] Prajna | A framework for worst-case and stochastic safety verification using barrier certificates[END_REF]. We also investigate in Section 7.4 the effect of square-free decomposition-which generalizes the square-free reduction-on the deductive power of proof rules. Finally, we complement our theoretical results with a practical assessment of the proof rule performance on a set of benchmarks and explore interesting connections between the deductive power and the practical running time performance (Section 8.2).

Preliminaries

We consider autonomous2 polynomial vector fields (see Def. 1 below). Let x = (x 1 , . . . , x n ) ∈ R n , and x(t) = (x 1 (t), . . . , x n (t)), where x i : R → R, t → x i (t). The ring of polynomials over the reals will be denoted by R[x 1 , . . . , x n ].

Definition 1 (Polynomial Vector Field). Let p i , 1 ≤ i ≤ n, be multivariate polynomials of the polynomial ring R[x 1 , . . . , x n ]. A polynomial vector field, p, is an explicit system of ordinary differential equations with polynomial right-hand side:

dx i dt = ẋi = p i (x), 1 ≤ i ≤ n . (1)
Since polynomial functions are smooth (C ∞ , i.e. they have derivatives up to any order), they are locally Lipschitz-continuous. By the Cauchy-Lipschitz theorem (a.k.a. Picard-Lindelöf) [START_REF] Lindelöf | Sur l'application de la méthode des approximations successives aux équations différentielles ordinaires du premier ordre[END_REF], there exists a unique maximal solution to the initial value problem ( ẋ = p, x(0) = x 0 ) defined for t in some non-empty open interval; it is often denoted by x(t), or more explicitly as ϕ t (x 0 ).

For S ⊆ R n , if ϕ t (x 0 ) ∈ S for all t ≥ 0 and x 0 ∈ S, we say that the set S is a (positive) invariant under the flow of p. If S is described by a quantifier-free formula of real arithmetic (i.e. is a semi-algebraic set satisfying a finite boolean combination of polynomial equalities and inequalities), positive invariance of S is semantically equivalent to the validity of the following formula in differential dynamic logic [START_REF] Platzer | Differential dynamic logic for hybrid systems[END_REF]:

S → [ ẋ = p] S.
(2)

A result about positive invariance of closed sets under the flow of locally Lipschitz-continuous ODEs, known as the Nagumo theorem [START_REF] Nagumo | Über die Lage der Integralkurven gewöhnlicher Differentialgleichungen[END_REF]Walter, 1998, Chapter 10, XV-XVI, pp. 117-119), gives a powerful (but generally intractable) geometric characterization of positively invariant closed sets. Nagumo's theorem requires the geometric notion of sub-tangential vectors to a set.

Definition 2 (Sub-tangent vector). A vector v ∈ R n is sub-tangential to a set

S ⊆ R n at x ∈ S if lim inf λ→0 + dist (S, x + λv) λ = 0,
where dist denotes the Euclidean set distance, i.e. dist(S, x) ≡ inf y∈S xy .

The set of all sub-tangent vectors to a set S at x ∈ S is known as the contingent cone to S at x and is denoted K x (S).

Theorem 3 (Nagumo's Theorem). Given a continuous system ẋ = p(x) and assuming that solutions exist and are unique inside some open set O ⊆ R n , let S ⊂ O be a closed set. Then, S is positively invariant under the flow of the system if and only if p(x) is sub-tangential to S (or equivalently, p(x) ∈ K x (S), where K x (S) is the set of all sub-tangential vectors to S at x, known as the contingent cone) for all x ∈ bdr(S), where bdr(S) is the boundary of S.

Using Nagumo's Theorem, the following proof rule is sound and complete when S is a closed semi-algebraic set:

(Nagumo) ∀ x ∈ bdr(S). p(x) ∈ K x (S) S → [ ẋ = p] S .
More recently, a different characterization of positively invariant sets (described in detail in subsequent sections) was reported in [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF].

In the important special case where a closed set S is described by the equation h = 0, with h ∈ R[x 1 . . . , x n ], positive invariance of h = 0 is semantically equivalent to the validity of the formula:

(h = 0) → [ ẋ = p](h = 0).
(3)

Geometrically, the equation h = 0 represents the set of real roots of the polynomial h. Such a set is known as real algebraic set or a real variety and will be henceforth denoted by V R (h). Algebraic sets are intimately related to sets of polynomials with special algebraic properties called ideals. Ideals are closed under addition and external multiplication; that is, if I is an ideal, then for all h 1 , h 2 ∈ I, the sum h 1 + h 2 ∈ I; and if h ∈ I, then, qh ∈ I, for all q ∈ R[x 1 . . . , x n ]. To say that the real variety V R (h) of the ideal generated by h is invariant under the flow of the vector field p is equivalent to the statement that the equation h = 0 is invariant.

We will use ∇h to denote the gradient of h : R n → R, that is the vector of its partial derivatives ∂h ∂x 1 , . . . , ∂h ∂xn . The Lie derivative of h along the vector field p gives the rate of change of h along the flow of ẋ = p(x) and is formally defined as the scalar product of ∇h and p.

L p (h) def = ∇h • p . (4)
Higher-order Lie derivatives are defined recursively as

L (k+1) p (h) = L p (L (k) p (h)), with L (0) p (h) = h.

Proof Rules for Algebraic Sets

We recall five important proof rules for checking invariance of polynomial equalities, or equivalently the validity of Equation 3. In Figure 1, FI refers to invariant polynomial functions. 4 The premise of the Polynomial-scale consecution proof rule [START_REF] Sankaranarayanan | Constructing invariants for hybrid systems[END_REF], P-c in Figure 1, requires L p (h) to be in the ideal generated by h. The condition given in the premise is only sufficient (but is eminently suitable for generating invariant varieties [START_REF] Matringe | Generating for nonlinear hybrid systems by linear algebraic methods[END_REF]). We also consider the constant-scale consecution proof rule [START_REF] Sankaranarayanan | Constructing invariants for hybrid systems[END_REF][START_REF] Tiwari | Abstractions for hybrid systems[END_REF], denoted by C-c. The premise of proof rule C-c requires that L p (h) = λh, where λ is a scalar, not a polynomial as in P-c. It is therefore a simple special case of P-c. When λ = 0, one obtains the premise of the proof rule FI. It is worth noting that the condition in the premise of P-c, including its special case C-c, was mentioned as early as 1878 [START_REF] Darboux | Mémoire sur les équations différentielles algébriques du premier ordre et du premier degré[END_REF] and used extensively in the study of integrability of dynamical systems (e.g. see second integrals in (Goriely, 2001, Chapter 2)). It serves as a natural extension to invariant functions, also known as first integrals, which are covered by the proof rule FI.

(FI) The proof rule Lie gives Lie's criterion [START_REF] Lie | Vorlesungen über continuierliche Gruppen mit Geometrischen und anderen Anwendungen[END_REF][START_REF] Olver | Applications of Lie Groups to Differential Equations[END_REF] for invariance of h = 0; this proof rule will be discussed in more depth and extended to handle tricky cases in Section 4. The last rule, DRI in Fig. 1, was recently introduced and characterizes (i.e. gives necessary and sufficient conditions for) invariant real varieties under the flow of polynomial vector fields (Ghorbal and Platzer, 2014). The number N in the premise of DRI is the maximum length of the ascending chain of polynomial ideals h ⊂ h, L p (h) ⊂ h, L p (h), L

L p (h) = 0 (h = 0) → [ ẋ = p](h = 0) (C-c) ∃λ ∈ R, L p (h) = λh (h = 0) → [ ẋ = p](h = 0) (Lie) h = 0 → (L p (h) = 0 ∧ ∇h = 0) (h = 0) → [ ẋ = p](h = 0) (P-c) L p (h) ∈ h (h = 0) → [ ẋ = p](h = 0) (DRI) h = 0 → N -1 i=0 L (i) p (h) = 0 (h = 0) → [ ẋ = p](h = 0)
(2) p (h) ⊂ • • • , which is finite and computable (Ghorbal and Platzer, 2014).

Extending Lie's Criterion

One immediate deficiency of the proof rule Lie (Fig. 1) is its inability to prove invariance properties for isolated points (e.g. system equilibria) for the simple reason that a description of such a point a = (a 1 , . . . , a n ) ∈ R n , e.g. given by the sum-of-squares equation h

(x) = (x 1 -a 1 ) 2 + • • • + (x n -a n ) 2 =
0, will have an extremum at a, i.e. h(a) = 0 and h(x) > 0 for all x ∈ R n \ {a}. Functions whose real roots characterize isolated points have vanishing gradient at these roots, in this case a, and thus the formula h = 0 → ∇h = 0 holds. This violates the regularity condition in the premise of the proof rule Lie, namely:

h = 0 -→ ∇h = 0 .
(5)

In fact, h = 0 → L p (h) = 0 is a necessary condition when h = 0 is an invariant equation. Note that simply removing Eq. ( 5) from the premise of the proof rule Lie is unsound (see e.g. (Platzer, 2012a)); that is, the condition h = 0 → L p (h) = 0 alone is insufficient to prove the invariance property for h = 0. Unsoundness in the above naïve attempt at a generalization is a consequence of singularities that may be present in the variety

V R (h). Singularities of V R (h) are points x ∈ V R (h)
where the gradient of h vanishes, i.e. ∇h(x) = 0.

Definition 4 (Singular Locus). Let h ∈ R[x 1 , . . . , x n ], the singular locus of h = 0, henceforth denoted SL(h), is the set of singular points, that is, points x satisfying

h = 0 ∧ ∂h ∂x 1 = 0 ∧ • • • ∧ ∂h ∂x n = 0 .
Points that are not singular are called regular. At singular points, the Lie derivative of h along any vector field is 0 • p = 0. To avoid these degenerate cases, the regularity condition (Eq. ( 5)) rules out singularities altogether. In the next section we present two extensions of Lie's criterion that, in a similar vein to [START_REF] Taly | Deductive verification of continuous dynamical systems[END_REF], partially overcome the strong regularity condition by treating the points on the singular locus separately.

Handling Singularities

Equilibria are points in the state space where the vector field vanishes (p = 0) so that there is no motion. However, as seen above, Lie's criterion cannot generally be applied to prove invariance properties of isolated equilibria because their description involves singularities. One simple way to resolve this issue is to drop the non-vanishing gradient condition and replace it with the proviso that there be no flow (that is p = 0) in the variables of the invariant candidate on the singular locus; this will allow singularities in the invariant candidate and will provide a sound proof method in which there is no need to check for non-vanishing gradient. Below we present two extensions to the proof rule Lie and justify their soundness after recalling some basic geometric notions.

Definition 5 (Lie • : Lie + Equilibria).

(Lie • ) h = 0 → L p (h) = 0 ∧ SL(h) → x i ∈vars(h) p i = 0 (h = 0) → [ ẋ = p](h = 0) ,
where vars(h) denotes the set of state variables x i occurring in the polynomial h.

The Lie • proof rule can be generalized further at the expense of adding an extra variable by replacing the "no flow" condition (p i = 0) for points on the singular locus with ∀λ. h(x + λp(x)) = 0, where λ is a fresh symbol.

Definition 6 (Lie * : Lie + Vanishing Sub-tangent).

(Lie * ) h = 0 → L p (h) = 0 ∧ (SL(h) → h(x + λp) = 0) (h = 0) → [ ẋ = p](h = 0) .
To prove soundness of Lie • and Lie * , we appeal to the Nagumo theorem. Let us observe that given x ∈ bdr(S), if x + λp(x) ∈ S for all λ ∈ R, then dist (S, x + λp(x)) = 0 and so p(x) is sub-tangential to S at x. This observation is important for algebraic sets, for which bdr(S) = S, and the condition x + λp(x) ∈ S translates to h(x + λp(x)) = 0. This is the main idea behind the soundness of the proof rule Lie * .

Proposition 7. The proof rule Lie * is sound.

Proof. A point on the variety is either regular or singular. For regular points (these form an open subset of the variety), since L p (h)(x) = 0, the vector p(x) is sub-tangent to the variety at x (in fact, it is even tangent, so the condition we check is exactly that which is used in Lie). At singular points x ∈ V R (h) if h(x + λp(x)) = 0 holds for all λ then dist(V R (h), x + λp(x)) = 0 for all λ, from which it follows that lim inf λ→0 + dist(V R (h),x+λp(x)) λ = 0 and thus p(x) is sub-tangential to V R (h) at x. Assuming solutions exist and are unique, the variety V R (h) is positively invariant under the vector field p by Nagumo's theorem.

The case p(x) = 0 for all x in the singular locus is a special case of the proof rule Lie * . Therefore, the soundness of Lie • is an immediate corollary of Prop. 7.

Corollary 8. The proof rule Lie • is sound.

Remark 9. It is worth remarking that the proof rules presented in this section, as well as Lie and FI, also work for non-polynomial vector fields and invariant candidates which themselves are not polynomial but sufficiently smooth. However, in such cases the resulting arithmetic may no longer be decidable [START_REF] Richardson | Some undecidable problems involving elementary functions of a real variable[END_REF].

Proof rules for semi-algebraic sets

In this section we will discuss three different methods for proving positive invariance of semi-algebraic sets, that is sets described by boolean combinations of polynomial equalities and inequalities.

Differential Invariants

Differential induction with differential invariants (henceforth DI) was introduced in (Platzer, 2010, Theorem 1).

Theorem 10 (Differential Invariants (DI)). Given a polynomial system ẋ = p and a quantifier-free formula of real arithmetic S in the state variables (describing some semi-algebraic set), the following rule of inference is sound:

(DI) D(S) p ẋ S → [ ẋ = p] S .
In DI, S is a quantifier-free first-order formula in the theory of real arithmetic and D is the derivation operator (Platzer, 2012a, Definition 3.2), which is defined as follows:

D(r) = 0 for numbers, D(x) = ẋ for variables, D(a + b) = D(a) + D(b), D(a • b) = D(a) • b + a • D(b), D a b = D(a) • b -a • D(b) b 2 , D(S 1 ∧ S 2 ) ≡ D(S 1 ) ∧ D(S 2 ), D(S 1 ∨ S 2 ) ≡ D(S 1 ) ∧ D(S 2 ), (∧ here is important for soundness) D(a ≤ b) ≡ D(a) ≤ D(b), accordingly for ≥, >, < . (6)
The formula D(S) p ẋ is obtained by replacing each ẋi in D(S) with the corresponding right hand side in the system of differential equations, i.e. by p i (x).

Remark 11. Note that if S has the form h ≤ 0 for a polynomial h, then the requirements in the premise of DI are exactly the conditions that a barrier certificate [START_REF] Prajna | Safety verification of hybrid systems using barrier certificates[END_REF]) has to satisfy. Thus, for this case, differential invariants include barrier certificates as a special case [START_REF] Platzer | Differential-algebraic dynamic logic for differential-algebraic programs[END_REF]. Barrier certificates are, however, also accompanied with interesting techniques for generating such invariant regions.

Remark 12. When S ≡ h = 0, the premise of DI is equivalent to the premise of FI. Thus, DI lifts FI to formulas following the arithmetic of the D operator in Eq. (6).

In practice, although differential invariants allow one to work with sets that are expressed using formulas with boolean operators, the conditions are very conservative (because they are required to hold everywhere in the state space, rather than only on the boundary of the set defined by S) and may fail to hold even for seemingly simple positively invariant sets. That is why differential invariants are used in conjunction with differential cuts [START_REF] Platzer | Differential-algebraic dynamic logic for differential-algebraic programs[END_REF](Platzer, , 2012b)), a process of successively augmenting the system dynamics with provable invariants, which we do not consider here.

Non-Smooth Strict Barrier Certificate

Another criterion, which we term non-smooth strict barrier certificate, may be seen as a generalization of the strict barrier certificates criterion [START_REF] Prajna | Safety verification of hybrid systems using barrier certificates[END_REF][START_REF] Prajna | A framework for worst-case and stochastic safety verification using barrier certificates[END_REF] (limited to closed sets of the form h ≤ 0) to generic closed semi-algebraic sets. Notice that our generalization only concerns the sufficient conditions for checking the invariance of supplied candidates. In particular, we do not extend nor adapt the computation techniques (convex optimization) underlying the barrier certificates generation to the new criterion we present in the sequel.

Given a closed semi-algebraic set

S ≡ k i=1 m(i) j=1 h ij ≤ 0 with polynomials h ij ∈ R[x 1 , . . . , x n ],
we can equivalently rewrite S by a sub-level set of a continuous function, namely

S ≡ k i=1 m(i) j=1 h ij ≤ 0 ≡ min i=1,...,k max j=1,...,m(i) h ij ≤ 0 .
Before stating the proof rule, we first define the Lie derivation for min max functions as follows. The set L p (max(h 1 , h 2 , . . . , h m )) < 0 is defined inductively by L p (h 1 ) < 0 if m = 1, and for m ≥ 2 by

(h 1 > max(h 2 , . . . , h m ) → L p (h 1 ) < 0) ∧ (h 1 < max(h 2 , . . . , h m ) → L p (max(h 2 , . . . , h m )) < 0) ∧ (h 1 = max(h 2 , . . . , h m ) → L p (h 1 ) < 0 ∧ L p (max(h 2 , . . . , h m )) < 0) (7) For instance, for m = 2, one gets: L p (max(h 1 , h 2 )) < 0 def = (h 1 > h 2 → L p (h 1 ) < 0) ∧ (h 1 < h 2 → L p (h 2 ) < 0) ∧ (h 1 = h 2 → L p (h 1 ) < 0 ∧ L p (h 2 ) < 0)
We similarly define the set L p (min(g 1 , . . . , g m )) < 0 by L p (g 1 ) < 0 if m = 1, and for m ≥ 2,

(g 1 < min(g 2 , . . . , g m ) → L p (g 1 ) < 0) ∧ (g 1 > min(g 2 , . . . , g m ) → L p (min(g 2 , . . . , g m )) < 0) ∧ (g 1 = min(g 2 , . . . , g m ) → L p (g 1 ) < 0 ∨ L p (min(g 2 , . . . , g m )) < 0) . (8)
where g i is of the form max(h i,1 , . . . , h i,m ). For instance,

L p (min(max(h 1 , h 2 ), h 3 )) < 0 ≡ (max(h 1 , h 2 ) < h 3 → L p (max(h 1 , h 2 )) < 0) ∧ (max(h 1 , h 2 ) > h 3 → L p (h 3 ) < 0) ∧ (max(h 1 , h 2 ) = h 3 → L p (max(h 1 , h 2 )) < 0 ∨ L p (h 3 ) < 0) (9)
We are now ready to state the non-smooth strict barrier certificate proof rule.

Proposition 13 (Non-smooth strict barrier certificates (NSSBC)). Given a continuous system ẋ = p and a closed semi-algebraic set

S ≡ k i=1 m(i) j=1 h ij ≤ 0, where h ij ∈ R[x 1 , . . . , x n ],
then, the following proof rule is sound:

(NSSBC) min i=1,...,k max j=1,...,m(i) h ij = 0 → L p min i=1,...,k max j=1,...,m(i) h ij < 0 k i=1 m(i) j=1 h ij ≤ 0 → [ ẋ = p] k i=1 m(i) j=1 h ij ≤ 0 . Proof. Consider an arbitrary point x 0 ∈ R n such that min i=1,...,k max j=1,...,m(i) h ij x 0 = 0,
then it is necessarily the case that for those active max arguments with indices i * in I * ⊆ {1, . . . , k} such that max j=1,...,m(i * )

h i * j x 0 = 0 for all i * ∈ I * , the condition L p max j=1,...,m(i * ) h i * j
x 0 < 0 needs to hold for at least some i * ∈ I * (otherwise the premise of the proof rule is not satisfied). Without loss of generality, assume that at x 0 there is one such i * .

The condition guarantees that for all polynomial arguments of the max function, their Lie derivative is strictly negative at x 0 . Since Lie derivatives of polynomials under polynomial vector fields are also polynomial functions (and thus continuous), there exists an open neighbourhood around x 0 inside which L p (h i * j ) < 0 is true for all j ∈ {1, . . . , m(i * )}. Thus, if the system is initialized at x 0 , it is guaranteed to enter the region where max j=1,...,m(i * )

h i * j < 0
and remain there for some non-empty time interval (0, ), where > 0, by following the solution ϕ t (•), which implies that

min i=1,...,k max j=1,...,m(i) h ij (ϕ t (x 0 )) ≤ 0 for all t ∈ [0, 2 ].
The closed set S is thus locally positively invariant and therefore positively invariant.

Nagumo-like Conditions for Closed Semi-algebraic Sets

Nagumo's theorem gives a necessary and sufficient condition for positive invariance of arbitrary closed sets (cf. Theorem 3); however, one needs to be careful when applying this result to sets defined by formulas with logical connectives. It is often tempting to apply the sub-tangency condition element-wise to sets defined by atomic formulas, but in certain degenerate cases this leads to incorrect conclusions. To appreciate this problem, we first require some basic facts about the closure properties of the contingent cone (i.e. the set of all sub-tangent vectors to a set at a given point).

Proposition 14. Let S 1 , S 2 ⊆ R n , then for all x ∈ S we have

K x (S 1 ) ∪ K x (S 2 ) ⊆ K x (S 1 ∪ S 2 ). Proof. Since dist(S, •) ≥ 0 and S 1 ⊆ S 1 ∪ S 2 , we have 0 ≤ inf x∈S 1 ∪S 2 x -x 0 ≤ inf x∈S 1
xx 0 for any x 0 , and

0 ≤ dist(S 1 ∪ S 2 , x 0 ) ≤ dist(S 1 , x 0 ) by definition.
Substituting x 0 + tv for x 0 and dividing by t > 0 we get

0 ≤ dist(S 1 ∪ S 2 , x 0 + tv) t ≤ dist(S 1 , x 0 + tv) t
and by assumption

0 ≤ lim inf t→0 + dist(S 1 ∪ S 2 , x 0 + tv) t ≤ lim inf t→0 + dist(S 1 , x 0 + tv) t = 0. from which it follows that if v is sub-tangential to S 1 at x 0 , then it is also sub-tangential to S 1 ∪ S 2 . Thus, K x (S 1 ) ⊆ K x (S 1 ∪ S 2 ) for all x ∈ S 1 ; by the same argument one shows K x (S 2 ) ⊆ K x (S 1 ∪ S 2 ) for all x ∈ S 2 , from which one concludes that the inclusion K x (S 1 ) ∪ K x (S 2 ) ⊆ K x (S 1 ∪ S 2 ) holds for all x ∈ S 1 ∪ S 2 . Proposition 15. Let S 1 , S 2 ⊆ R n , then in general K x (S 1 ) ∩ K x (S 2 ) K x (S 1 ∩ S 2 ). Proof. Consider S 1 ≡ {x | x 2 + x 2 1 = 0} and S 2 ≡ {x | x 2 -x 2 1 = 0}.
The two sets intersect at 0 ∈ R 2 . At the origin, the intersection of the contingent cones is given by the real line, i.e. K 0 (S 1 ) ∩ K 0 (S 2 ) = {x | x 2 = 0}, whereas the contingent cone to the intersection of the two sets is given by the zero vector, K 0 (S 1 ∩ S 2 ) = {0}. See Figure 2 for an illustration and [START_REF] Wu | Tangent cone and contingent cone to the intersection of two closed sets[END_REF] for an overview this problem.

In general, given a closed set S which is presented as a finite union of intersections of closed sets S ij , i.e.

k i=1 m(i) j=1 S ij , one would like to determine if p(x) ∈ K x (S) by only checking p(x) ∈ K x (S ij ). If one has k i=1 m(i) j=1 K x (S ij ) ⊆ K x ( k i=1 m(i) j=1 S ij ). ( 10
)
for all x on the boundary of S, then Nagumo's criterion for vector field membership in the contingent cone for the whole set can be applied component-wise, i.e. the condition becomes It is possible to formulate inference rules based on Nagumo's theorem which allow one to prove positive invariance of a large class of closed semi-algebraic sets. This has previously been investigated in [START_REF] Taly | Deductive verification of continuous dynamical systems[END_REF], where a number of inference rules are presented for checking positive invariance of closed sets of the form h ≥ 0. For instance, it is shown that the following is a sound inference (similar to Lie):

∀x ∈ bdr   k i=1 m(i) j=1 S ij   . p(x) ∈ k i=1 m(i) j=1 K x (S ij ). x 1 x 2 (a) x 2 + x 2 1 = 0 ∧ x 2 -x 2 1 = 0 x 1 x 2 (b) ẋ1 = 1, ẋ2 = 0
h = 0 → L p (h) ≥ 0 ∧ ∇h = 0 h ≥ 0 → [ ẋ = p] h ≥ 0 ,
along with other rules with more general premises, all of which seek to check membership of p(x) in the contingent cone K x (h ≥ 0). The lifting of the conditions to formulas with boolean connectives (leading to a potential proof rule for closed semi-algebraic sets) described in (Taly and Tiwari, 2009, p. 393) essentially requires each S ij to be of the form h ij ≥ 0 and assumes the soundnesscritical property (10). Soundness issues may arise when this assumption fails to hold (as in Fig. 2). This deficiency can be fixed by e.g. requiring the matrix of partial derivatives of active components on the boundary to be full rank, i.e. rk(∇h 1 , ∇h 2 , . . . , ∇h k ) = k whenever the polynomials h 1 , h 2 , . . . , h k evaluate to 0 on the boundary (this need only apply to conjunctive components). A number of other possible sufficient conditions for removing this source of unsound-ness has been studied in non-smooth analysis [START_REF] Wu | Tangent cone and contingent cone to the intersection of two closed sets[END_REF] (see also practical sets in (Blanchini and Miani, 2008)). However, in practice, even ensuring the fullrank property for a matrix with polynomial entries is computationally expensive. Furthermore, even with conditions for soundness in place, the result may not be applied to reason about positive invariance of semi-algebraic sets that are neither closed nor open.

Liu, Zhan & Zhao Decision Procedure

In [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF], it was shown that checking whether a given semi-algebraic set is positively invariant under the flow of a polynomial vector field is decidable. The conditions one is required to check are phrased in terms of set inclusion of semi-algebraic sets, which can be determined using a decision procedure for real arithmetic. The result builds on ideas described earlier in [START_REF] Taly | Deductive verification of continuous dynamical systems[END_REF] and crucially depends on the property of solutions to differential equations with analytic right-hand sides being themselves analytic. In the remainder of this section, we rephrase and provide a detailed illustration of the main components of the result presented in [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF].

Theorem 16. Let h : R n → R be an analytic function and ẋ = p be an analytic system of ODEs. If x 0 ∈ R n is such that h(x 0 ) = 0, then one has three possibilities at x 0 :

1. ∃ N > 0. L (N ) p (h) < 0 N -1 i=1 L (i) p (h) = 0, 2. ∃ N > 0. L (N ) p (h) > 0 N -1 i=1 L (i) p (h) = 0, 3. ∀ N > 0. N i=1 L (i)
p (h) = 0. If x(0) = x 0 , then in case 1 one has h(x(t)) < 0 for all t ∈ (0, ) for some > 0; case 2 is analogous, but with h(x(t)) > 0 for all t ∈ (0, ). In case 3, one is guaranteed that h(x(t)) = 0 for all t ∈ (0, ).

Proof. Since both h and the solution to the analytic ODE are analytic functions, the Taylor series expansion of h(ϕ t (x 0 )) around t = 0 is given by

h(x 0 ) + ∞ i=1 t i i! • d i h dt i x 0 = ∞ i=1 t i i! • L (i) p (h) x 0
and converges on some non-empty open interval of t containing zero. Thus, the most significant term to become sign-definite will determine the sign of the entire sum on some sufficiently small interval. See (Liu et al., 2011, Proof of Proposition 9). See also [START_REF] Taly | Deductive verification of continuous dynamical systems[END_REF], Proof of Theorem 7), which employed very much the same ideas as [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF].

The following theorem is a simple corollary to (Liu et al., 2011, Theorem 19).

Theorem 17 [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF]). Given a polynomial system ẋ = p(x), and a semi-algebraic set S ⊆ R n , define

In p (S) ≡ {x ∈ R n | ∃ > 0. ∀ t ∈ (0, ). x(t) ∈ S}, In (-p) (S) ≡ {x ∈ R n | ∃ > 0. ∀ t ∈ (0, ). x(-t) ∈ S},
where x(t) is the solution to the initial value problem ( ẋ = p(x), x(0) = x 0 ) at time t. The set S is positively invariant under the flow of the system if and only if the inclusions In (-p) (S) ⊆ S ⊆ In p (S) hold, which implies soundness (and relative completeness) of the following rule of inference:

(LZZ) In (-p) (S) → S ∧ (S → In p (S)) S → [ ẋ = p] S .
To develop some intuition for the construction of In p (S), let us first consider the case where S is characterized by a single non-strict inequality h ≤ 0. Whenever h is an analytic function, one may use Theorem 16 to give a characterization of In p (h ≤ 0) as the set of states in R n that satisfy the following infinite set of conditions (cf. (Taly and Tiwari, 2009, Theorem 7, Theorem 8)):

h < 0 ∨ (h = 0 ∧ L p (h) < 0) ∨ (h = 0 ∧ L p (h) = 0 ∧ L (2) p (h) < 0) ∨ (h = 0 ∧ L p (h) = 0 ∧ L (2) p (h) = 0 ∧ L (3) p (h) < 0) ∨ . . .
The decidability of checking the conditions in Proposition 17 (i.e. the premise of LZZ) hinges on the ability to construct semi-algebraic sets In p (S) whenever S is semi-algebraic. In [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF] the authors make the crucial observation that whenever h is a polynomial and ẋ = p(x) is a system of polynomial ODEs, then the Lie derivatives L (i) p (h) up to any order i are also polynomials. Using the fact that the ring of multivariate polynomials with coefficients in some Noetherian ring is also Noetherian (by Hilbert's basis theorem), the set In p (h ≤ 0) can be characterized by a finite disjunction [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF]:

h < 0 ∨ (h = 0 ∧ L p (h) < 0) ∨ (h = 0 ∧ L p (h) = 0 ∧ L (2) p (h) < 0) ∨ . . . (h = 0 ∧ L p (h) = 0 ∧ L (2) p (h) = 0 ∧ • • • ∧ L (N -1) p (h) < 0) ∨ (h = 0 ∧ L p (h) = 0 ∧ L (2) p (h) = 0 ∧ • • • ∧ L (N -1) p (h) = 0 ∧ L (N ) p (h) ≤ 0).
The ascending chain property of Noetherian rings guarantees that there is a finite positive integer N such that for all N > N we have the following ideal membership:

L (N ) p (h) ∈ h, L p (h), . . . , L (N )
p (h) . The integer N may be found using Gröbner bases to successively check for ideal membership of L (N ) p (h) in the ideal generated by the Lie derivatives of orders lower than N for N = 1, 2, 3, . . . until the ideal saturates (as with DRI). Once N is found, if the formula

(h = 0 ∧ L p (h) = 0 ∧ L (2) p (h) = 0 ∧ • • • ∧ L (N -1) p (h) = 0 ∧ L (N )
p (h) = 0) holds, then for any N ≥ N we have

(h = 0 ∧ L p (h) = 0 ∧ L (2) p (h) = 0 ∧ • • • ∧ L (N -1) p (h) = 0 ∧ L (N ) p (h) = 0 ∧ • • • ∧ L (N ) p (h) = 0),
which removes the need to consider disjuncts with Lie derivatives of orders higher than N , as all the (infinitely many) formulas

(h = 0 ∧ L p (h) = 0 ∧ L (2) p (h) = 0 ∧ • • • ∧ L (N -1) p (h) = 0 ∧ L (N ) p (h) = 0 ∧ • • • ∧ L (N ) p (h) < 0),
with N > N are guaranteed to be false.

Remark 18. The ascending chain property is crucial in making it possible to reason about sign conditions of infinitely many higher-order Lie derivatives by only considering a finite number of sign conditions. The same idea was independently pursued in (Ghorbal and Platzer, 2014) to give a necessary and sufficient criterion for invariance of real algebraic sets under the flow of polynomial ODEs (summarized in the proof rule DRI; discussed earlier).

Thus, by computing N for a given polynomial h and a system ẋ = p(x), one may construct a semi-algebraic set In p (h ≤ 0). In Fig. 3d we detail the computation for N = 3 and depict the different "pieces" involved to form In p (h ≤ 0), which is, in this particular case, the same as h ≤ 0 as shown in Fig. 4b.

Likewise in the case of strict polynomial inequalities h < 0, the set In p (h < 0) is semi-algebraic and is characterized by the following formula: In order to construct In p (•) for semi-algebraic sets with boolean structure, an important distribution property, proved in (Liu et al., 2011, Theorem 20), is required. For convenience, the property is stated below.

h < 0 ∨ (h = 0 ∧ L p (h) < 0) ∨ (h = 0 ∧ L p (h) = 0 ∧ L (2) p (h) < 0) ∨ . . . (h = 0 ∧ L p (h) = 0 ∧ L (2) p (h) = 0 ∧ • • • ∧ L (N -1) p (h) < 0) ∨ (h = 0 ∧ L p (h) = 0 ∧ L (2) p (h) = 0 ∧ • • • ∧ L (N -1) p (h) = 0 ∧ L (N ) p (h) < 0). x 1 x 2 (a) L (0) p (h) < 0 (i.e. h < 0) x 1 x 2 (b) h = 0 ∧ L p (h) < 0 x 1 x 2 (c) h = L p (h) = 0 ∧ L (2) p (h) < 0 x 1 x 2 (d) h = L p (h) = L (2) p (h) = 0 ∧ L (3) p (h) ≤ 0
Theorem 19 ( [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF]). Given a polynomial system ẋ = p(x) and a semi-algebraic set S ≡ k i=1 m(i) j=1 h ij ∼ 0 where ∼∈ {<, ≤}, we have

In p (S) ≡ k i=1 m(i) j=1 In p (h ij ∼ 0).
Finally, In (-p) (S) is constructed in exactly the same way as In p (S), except the Lie derivatives are computed with respect to the vector field induced by the system in which time is reversed, i.e. ẋ = -p(x). This is possible because

d dt x(-t) = -p(x(-t)),
and the solution to ẋ = -p(x) is given by x(-t), where x(t) is the solution to ẋ = p(x). Once all the semi-algebraic sets in the premise of LZZ are constructed, the validity of the premise can be decided using a decision procedure for real arithmetic [START_REF] Tarski | A decision method for elementary algebra and geometry[END_REF].

Hierarchy

In this section, we compare the deductive power of the existing (Fig. 1) as well as the newly-introduced proof rules (Lie • and Lie * in Section 4, and NSSBC in Section 5.2) for checking the invariance of algebraic and semi-algebraic sets. This study should be complemented by another comparison that considers the interaction between the different proof rules in the context of a formal proof system in a similar vein to (Platzer, 2012b). We leave this for future work.

Given two proof rules R 1 and R 2 of the form

(R 1 ) P 1 (S 1 : T 1 ) -→ [ ẋ = p](S 1 : T 1 ) (R 2 ) P 2 (S 2 : T 2 ) -→ [ ẋ = p](S 2 : T 2 )
(11) where P i refers to the premise of the proof rule R i , and the conclusion has the form (S 1 : T 1 ) -→ [ ẋ = p](S 1 : T 1 ), where S i : T i denotes that the set S i is of type T i (the typical types we are considering in this work are algebraic and semi-algebraic sets).

Definition 20 (Partial order over proof rules). Let R 1 and R 2 be two proof rules of the form of Eq. (11). We say that R 2 generalizes R 1 and write R 2 R 1 (or R 1 R 2 ), if the premise of R 1 implies the premise of R 2 (P 1 → P 2 ), and T 1 is a subtype of T 2 (for instance, the type algebraic set is a subtype of the type semi-algebraic set).

Intuitively, if the proof rule R 1 proves that S 1 : T 1 is an invariant for the vector field p, then R 2 can be also applied to discharge the invariance of S 1 . If R 1 R 2 and R 1 R 2 , we say that R 1 and R 2 are equivalent, and denote this by R 1 ∼ R 2 . Observe that two equivalent proof rules operate necessarily on equivalents type of sets so T 1 and T 2 are equivalent. In a similar vein, R 1 R 2 (or R 2 R 1 ) denotes that R 1 is not generalized by R 2 . So in the absence of other rules, a proof rule that operates on algebraic sets cannot generalize a proof rule for semi-algebraic sets. Finally, we also write

R 1 ≺ R 2 when R 1 R 2 and R 1 R 2 . That is, the rule R 2 increases the deductive power of R 1 .
It is easy to see that the order is a partial order (with ∼ acting as equality): it is reflexive, R R (the premise of R implies itself); it is anti-symmetric (by definition), and transitive: if R 1 R 2 and R 2 R 3 , then the premise of R 1 implies the premise of R 3 by transitivity of the implication, so R 1 R 3 . Finally, if R 1 R 2 and R 1 R 2 , we will write R 1 ≺ R 2 and say that the proof rules R 1 and R 2 are incomparable. This means that for both R 1 and R 2 there are problems that one rule can prove and the other cannot. Notice that a proof rule for invariance of a certain class of semi-algebraic sets does not automatically generalize a proof rule for invariance of algebraic sets, even though the subtype condition is satisfied. Such proof rules are likely to be incomparable.

In what follows we use the partial order ( ) to illustrate the lattice structure of the proof rules under consideration. We use to compare the deductive power of the proof rules. On one hand, the proof rules for algebraic sets:

{FI, C-c, P-c, Lie, Lie • , Lie * , DRI},
and, on the other hand, the proof rules for semi-algebraic sets: {NSSBC, Nagumo, DI, LZZ} .

For convenience, the propositions of this section are summarized in the comparison matrices in Fig. 6 and Fig. 8. For instance, Prop. 25 proves that FI ≺ Lie. Cells without numbers are proved by transitivity of the partial order. For instance, FI ≺ DRI can be proved using FI ≺ C-c (Prop. 21) and C-c ≺ P-c (Prop. 22) and P-c ≺ DRI (Prop. 24). The Hasse diagram (Fig. 5) gives the lattice structure where arrows represent strictly increasing deductive power; every missing edge in the graph represents ≺ , as shown in the comparison matrix.

Proof Rules for Algebraic Sets

We begin by comparing Darboux-based proof rules, i.e. {FI, C-c, P-c} and then proceed to the Lie-based proof rule family, i.e. {Lie, Lie • , Lie * }. Next, we demonstrate the deductive superiority of the necessary and sufficient conditions in the premise of the proof rule DRI. Finally, we show that Darboux-based proof rules and Lie-based proof rules form two distinct proof rule families; that is, any proof rule from one family is deductively incomparable to any proof rule from the other family.

Proposition 21. FI ≺ C-c.
Proof. The premise of the rule C-c requires the existence of some λ ∈ R, such that L p (h) = λh. In particular, λ = 0 gives the premise of FI. Thus, FI C-c. To see that FI C-c, consider the one-dimensional vector field p = (x), we have L p (x) = 1x, and hence C-c (λ = 1) concludes that x = 0 is an invariant. However, FI cannot prove the invariance of x = 0 because x is not a conserved quantity in the system. Proof. The premise of the rule P-c requires the existence of some α ∈ R[x], such that L p (h) = αh (equivalently, L p (h) ∈ h ). In particular, the constant polynomial gives the premise of C-c. Thus, C-c P-c. To prove that C-c P-c, consider the two-dimensional vector field p = (xy, x), we have L p (x) = xy (or equivalently L p (x) ∈ x ⊂ R[x, y]) and hence conclude, using P-c, that x = 0 is an invariant. However, C-c fails to prove this invariant as the required cofactor is not a scalar.

Proposition 23. Lie ≺ Lie • and Lie • ≺ Lie * .
Proof. We already established that Lie Lie • (Prop. 8) and Lie • Lie * (Prop. 7); we give two counterexamples to establish the strict inclusion. (I) Lie Lie • . Whenever the variety has a singularity, the proof rule Lie will fail. Lie • is tailored to prove invariance of equilibrium points in addition to regular points of the variety. For instance, for p = ((-1 + x 1 )x 2 , x 2 (1 + x 2 )), Lie fails to prove that h = (-1 + x 1 ) 2 + (1 + x 2 ) 2 = 0 is invariant as the gradient ∇h vanishes at (1, -1) and h((1, -1)) = 0. However, at (1, -1) we also have p 1 = p 2 = 0, and hence the premise of Lie • is satisfied, and h = 0 is proved to be an invariant under the flow of p. (II) Lie • Lie * . In addition to equilibria, Lie * goes one step further and handles all singular points, x, where the vector x + λp is in the variety V R (h) for all λ ∈ R (that is h(x + λp) = 0, for all λ). For instance, consider the polynomial h = x 1 x 2 x 3 , its singular locus is given by the three axes x 1 = x 2 = 0, x 1 = x 3 = 0 and x 2 = x 3 = 0. For the vector field p = (x 1 , x 2 , x 3 ), the equilibrium point is at the origin (0, 0, 0), which obviously does not contain the entire singular locus of h. Thus, Lie • fails but Lie * succeeds because h(x + λp) = 0 when x is a point of one of the axes.

Proposition 24. P-c ≺ DRI and Lie * ≺ DRI.

Proof. DRI is both necessary and sufficient (Ghorbal and Platzer, 2014), so we know that P-c DRI and Lie * DRI. To prove the claim it is left to show that (I) P-c DRI. Consider the following two-dimensional vector field: p = ((-1 + x 1 )(1 + x 1 ), (-1 + x 2 )(1 + x 2 )). The candidate invariant (given by the roots of the Motzkin polynomial) h = 1 -3x 2 1 x 2 2 + x 4 1 x 2 2 + x 2 1 x 4 2 = 0 cannot be proved using P-c, as L p (h) ∈ h . However, the invariance property may be proved using DRI. For this, we need to consider the second-order Lie derivative of h and we prove that L

(2) p (h) ∈ h, L p (h) . Thus, the premise of DRI holds for N = 2. (II) Lie * DRI. Consider the following three-dimensional vector field p = (-

x 2 + x 1 (1 -x 2 1 -x 2 2 ), x 1 + x 2 (1 -x 2 1 -x 2
2 ), x 3 ). We want to prove that h = (-1 + x 2 1 + x 2 2 ) 2 + x 2 3 = 0 is an invariant. In this case, the variety V R (h) is exactly equal to the singular locus of h which is the two-dimensional unit circle -1 + x 2 1 + x 2 2 = 0. However, at all points of this unit circle, the vector field p is equal to (-x 2 , x 1 , 0) = 0, which prevents us from using Lie * (because h((x 1 , x 2 , 0) + λ(-x 2 , x 1 , 0)) = 0 for some λ ∈ R). The rule DRI proves the invariance of h = 0 with N = 2.

To appreciate the difference between FI and Lie, let us note that while the condition in the premise of FI may seem strong (i.e. too conservative), singularities in the invariant candidate do not present a problem for FI, whereas the premise of Lie rules out such candidates altogether (see Fig. 7). Indeed, the proof rule Lie cannot prove that 0 = 0 (the whole space is invariant), whereas this is the most trivial case for FI. Proposition 25 (FI and Lie are incomparable.). FI ≺ Lie.

x 1 x 2 (a) Positive invariance of the variety V R (x 2 1 + x 3 1 -x 2 2 ) provable using FI (but not Lie since (0, 0) is a singular point). x 1 x 2 (b) Smooth invariant limit cycle V R (x 2 1 + x 2 2 -1) provable using Lie (but not FI since x 2 1 + x 2 2 -1 is not an invariant function).
Proof. (I) FI Lie. For the vector field p = (-2x 2 , -2x 1 -3x 2 1 ), the equation x 2

1 + x 3 1 -x 2 2 = 0 is provable with FI but not Lie, see Fig. 7 (left). (II) FI Lie. For the vector field p = (x Remark 31. Provided that the invariant candidate has no singular points, Lie's criterion is known to be both necessary and sufficient to prove invariance properties of level sets (Olver, 2000, Theorem 2.8). Also, FI characterizes invariant functions (Platzer, 2012a) but not all invariant equations. On the other hand, for algebraic differential equations, the differential radical criterion in DRI fully characterizes all invariant algebraic sets (Ghorbal and Platzer, 2014). Thus, as established in Prop. 24, DRI increases the deductive power of both Darbouxbased rules {FI, C-c, P-c} and Lie-based rules {Lie, Lie • , Lie * }, which form different families.

1 -x 3 1 -x 2 -x 1 x 2 2 , x 1 + x 2 -x 2 1 x 2 -x 3 2 ), the invariance

Proof Rules for Semi-Algebraic Sets

In this section, we compare the deductive power of the proof rules {NSSBC, Nagumo, DI, LZZ}, as well as their relationships to the proof rules for checking the invariance of algebraic sets.

Proposition 32. NSSBC ≺ Nagumo.

Proof. The Nagumo theorem characterizes closed positively invariant sets under the flow of locally Lipschitz ODEs. In particular, this covers closed semi-algebraic sets and polynomial ODE. Hence NSSBC Nagumo. To see why the inequality is strict, consider any vector field with an invariant algebraic set (recall that algebraic sets are special closed semi-algebraic sets with empty interior). The proof rule NSSBC cannot work for such invariant sets precisely because it requires L p (h) < 0 whenever h = 0. In fact, h = 0 → L p (h) = 0 is a necessary condition for any invariant algebraic set.

Proposition 33. Nagumo ≺ LZZ and DI ≺ LZZ.

Proof. For semi-algebraic sets, the proof rule LZZ characterizes (arbitrary) invariant semi-algebraic sets for polynomial ODE. The Nagumo theorem only characterizes closed semi-algebraic sets. Hence the strict inequality. Similarly, DI gives only a sufficient condition and is therefore strictly less powerful than LZZ.

Proposition 34. NSSBC ≺ DI.

Proof. DI NSSBC. Consider the system

p(x) = -x 3 1 + x 2 2 x 1 -x 1 -x 2 , -x 3 2 + x 2 1 x 2 -x 2 + x 1 and let S 1 ≡ x 1 -1 3 2 + x 2 2 -2 ≤ 0 ∧ x 1 + 1 3 2 + x 2 2 -2 ≤ 0
, which is a positively invariant set under the flow of the system (see Fig. 9a). The invariance property cannot be proved using the rule DI, but is easily proved using NSSBC (and LZZ). NSSBC DI. Consider the system p(x) = (x 2 2 , 2) and let S 2 ≡ x 2 ≥ 0 ∧ x 1 ≥ 0. Positive invariance of S 2 is proved easily using either DI (and LZZ), but cannot be proved using NSSBC. Intuitively, this can be seen because at the origin the vector p(0) does not point strictly into the interior of S 2 ≡ max(-x 2 , -x 1 ) ≤ 0, since L p (-x 1 ) = -x 2 2 | 0 = 0 (see Fig. 9b).

x 1 x 2 (a) S 1 ≡ x 1 -1 3 2 + x 2 2 -2 ≤ 0 ∧ x 1 + 1 3 2 + x 2 2 -2 ≤ 0 x 1 x 2 (b) S 2 ≡ x 2 ≥ 0 ∧ x 1 ≥ 0 Figure 9:
Positive invariance of the semi-algebraic set S 1 (left) provable using NSSBC (but not DI) and a positive invariant S 2 (right) provable using DI (but not NSSBC).

Proposition 35. Nagumo ≺ DI.

Proof. By Prop. 34 and Lem. 26, Nagumo DI. In addition, the proof rule DI cannot be generalized by Nagumo since it can be applied to sets that are not necessarily closed or open, which is not the case with Nagumo.

In Fig. 5, one can see that the proof rules for algebraic sets are incomparable with NSSBC. This is precisely because invariant algebraic sets are ruled out all together by the premise of NSSBC which requires the vector field to point inward on the boundaries. Furthermore, because only algebraic sets are allowed in the conclusion of those proof rules, they cannot generalize NSSBC nor DI which can be apply more generally. Thus: The generalization FI ≺ DI is a straightforward consequence of DI: in fact, by definition, the proof rule DI lifts, in a conservative way, the simplest condition for a differentiable function to be positive or negative-namely by checking if its derivative is positive or negative respectively-to a finite boolean formula of such functions. Said differently, the premise of FI is identical to the premise of DI when used for an atomic formula of the form h = 0.

Remark 38. The premises of the proof rules for algebraic sets could be used to work with a larger class of invariant sets, namely those of the form h ≥ 0 in addition to algebraic sets. For instance, if L p (h) ∈ h , then necessarily h ≥ 0 is an invariant of the system. In fact, the invariance of h = 0 implies the invariance of h 0 for ∈ {≤, <, ≥, >}. Such extra proof rules do not bring any additional insight to the realm of proof rules depicted in Fig. 5 and are therefore not represented.

Square-free Reduction

In this section we assess the utility of performing square-free reduction of invariant candidates as a means of (i) increasing the deductive power of certain proof rules to be identified and (ii) simplifying problems passed to decision procedures for real arithmetic. Our results are summarized in Fig. 10 for convenience.

Square-free Reduction with Lie-based Proof Rules

While Lie uses a powerful criterion that captures a large class of practically relevant invariant sets, it will fail for some seemingly simple invariant candidates. For instance, the condition in the premise of Lie will not hold when the goal is to prove that h = x 2 -6x + 9 = 0 is invariant, no matter what vector field one considers. The reason for this is simple: x 2 -6x + 9 factorizes into (x -3) 2 . The problem here lies in the polynomial h itself, rather than the real variety V R (h). In fact, V R (h) is exactly the singular locus of h and the proof rule Lie fails because all points inside V R (h) are singular points. More generally, the chain rule implies ∇h k • p = kh k-1 ∇h • p, which has the consequence that any polynomial h which is not square-free will have vanishing gradient at the real roots of factors with multiplicity greater than 1.

One can eliminate such annoying instances by reducing h to square-free form, which is a basic pre-processing step used in computer algebra systems. The square-free reduction of a polynomial h may be computed as follows:

SF(h) = h gcd h, ∂h ∂x 1 , . . . , ∂h ∂xn . (12)
Intuitively, in performing square-free reduction we hope to shrink the singular locus of the original polynomial. If SL(SF(h)) is the empty set (which is the case for h = x 2 -6x + 9 in the example given above), the proof rule Lie applies to SF(h) but not to h. In general, SF(h) may satisfy the assumptions of the proof rules Lie • or Lie * , where h fails to do so. It is always sound to conclude that h = 0 is invariant from the knowledge that SF(h) = 0 is invariant, since real varieties remain unaltered under square-free reduction of their defining polynomials [START_REF] Cox | Ideals, Varieties, and Algorithms -an introduction to computational algebraic geometry and commutative algebra[END_REF], i.e. V R (h) ≡ V R (SF(h)). Thus, replacing h with SF(h) in the premise of Lie, Lie • and Lie * does not compromise soundness (it us a use of the generalization proof rule [START_REF] Platzer | Differential dynamic logic for hybrid systems[END_REF]) and enlarges the class of polynomials that these proof rules can work with.

Proposition 39. For all ∈ {Lie, Lie • , Lie * }, ≺ SF .

This result is unsurprising when one understands that Lie-based proof rules use geometric concepts to prove invariance properties of sets. In fact, the squarefree reduction removes some purely algebraic oddities that prevent the geometric condition from holding true when checked syntactically by a machine.

In addition to increasing the deductive power, the square-free reduction reduces the total degree of the polynomial in the invariant candidate and hence serves to reduce the complexity of deciding the conditions in the premise (cf. discussion in Section 8). In our implementation, we adopt the convention that invariant candidates supplied to Lie and its generalizations are square-free reduced in a pre-processing step.

Square-free Reduction with Darboux-based proof rules

Unlike Lie-based proof rules, it is perhaps surprising that using square-free reduction as a pre-processing step for the proof rules FI and C-c, denoted SFFI and SFC-c respectively, does not, in general, increase the deductive power and may even lead to properties that are no longer provable.

Proposition 40. FI ≺ SFFI.

Proof. (I) FI ≺ SFFI. The polynomial h = x 2 y is an invariant function for the vector field p = ( ∂h ∂y , -∂h ∂x ) = (x 2 , -2xy), thus FI proves the invariance of h = 0. However, SF(h) is not an invariant function for the same vector field, since L p (SF(h)) = L p (xy) = -x 2 y = 0, thus SFFI fails to prove the invariance of h = 0. (II) SFFI ≺ FI. Similarly, the polynomial h = xy is an invariant function for the vector field p = ( ∂h ∂y , -∂h ∂x ) = (x, -y), thus SFFI proves the invariance of x 2 y = 0, since SF(x 2 y) = h. However, FI fails to prove the invariance of x 2 y = 0, because L p (x 2 y) = x 2 y = 0.

Prop. 40 may at first seem counter-intuitive. However, the criterion in the premise of FI is different as it proves that the candidate h is an invariant function. In performing square-free reduction on h, one in general obtains a different function, SF(h), which need not be conserved in the system if h is conserved or, conversely, may be conserved even if h is not.

The same observation holds for C-c as the SF reduction does not preserve the constant rate exponential decrease (or increase).

Proposition 41. C-c ≺ SFC-c. Proof. (I) C-c ≺ SFC-c. The proof rule C-c proves the invariance of h = x 2 y = 0 for the vector field p = (x 2 , y(1 -2x)) as L p (h) = 1h. However, C-c cannot prove SF(h) = 0, since L p (SF(h)) = L p (xy) = (1 -x) SF(h). (II) SFC-c ≺ C-c.
For the same h, C-c proves the invariance of SF(h) = 0 for the vector field p = (x 2 , y(1 -x)) as L p (SF(h)) = L p (xy) = 1 SF(h). However, without the SF reduction C-c alone fails to prove the invariance of h = 0 for the considered p, as L p (h) = (x + 1)h.

After Prop. 40 and 41, one expects P-c to be incomparable with its squarefree counterpart. Surprisingly, the proof rules P-c and SFP-c (which applies P-c after the square-free reduction) are in fact equivalent. This follows from the fact that a polynomial is Darboux for a vector field p if and only if all its factors are also Darboux for the same vector field. Our findings are stated in Prop. 42 and its corollary Prop. 43. 5Proposition 42. Let h = q m 1 1 • • • q mr r denote the decomposition of the polynomial h into irreducible (over the reals) factors, q i . Then, h is Darboux for p if and only if, for all i, q i is Darboux for p.

Proof. If, for all i, the polynomial q i is Darboux for p, then q i divides L p (q i ), i.e.

Lp(q i ) q i ∈ R[x 1 , . . . , x n ].
Therefore, using the chain rule,

L p (h) = L p (q m 1 1 • • • q mr r ) (13) = r i=1 m i L p (q i )q m i -1 i j =i q m j j (14) = r i=1 m i L p (q i )q m i -1 i h q m i i (15) = h r i=1 m i L p (q i ) q i (16) ∈ h , ( 17
)
and h is also Darboux for p.

If h is Darboux for p, then h divides L p (h) and Lp(h) h is a polynomial. Recall that SF(h) = q 1 • • • q r . Using Eq. ( 16), one gets

L p (h) h SF(h) = r i=1 m i L p (q i ) q i SF(h) . (18)
For a fixed i, q i divides SF(h), it thus divides the left hand side of Eq. ( 18). Moreover, q i divides SF(h) q j , for all j = i. It thus necessarily divides m i SF(h)

q i L p (q i ). If q i divides SF(h)
q i , then there exists j = i such that q i divides q j , which contradicts the fact that all factors q 1 , . . . , q r are irreducible. Thus, q i divides L p (q i ) and L p (q i ) ∈ q i . Proposition 43. P-c ∼ SFP-c.

Proof. The proof rule P-c proves the invariance of h = 0 for p if and only if the polynomial h is Darboux. However, by Prop. 42, h is Darboux if and only if SF(h) is also Darboux. Therefore, SFP-c could be used equivalently to prove the invariance of h = 0.

Remark 44. The condition L p (h) ∈ SF(h) -which is weaker than L p (h) ∈ h -is not sufficient to prove the invariance of h = 0. It is therefore an unsound proof rule. Consider the polynomial h = (-1 + x 2 ) 2 and the 1-dimensional vector field ẋ = x. Although L p (h) = 4(-1 + x 2 )x 2 ∈ -1 + x 2 = SF(h) , the equation h = 0 is not invariant, however, because x(t) = ±e t . Notice that the proof rule P-c (with or without the square-free reduction) is unable to prove or disprove the invariance of h = 0.

Square-free Reduction On Differential Radical Invariants (DRI)

Square-free reduction cannot increase the deductive power of the proof rule DRI because its premise is necessary and sufficient to prove invariance of real algebraic sets, which is unaffected by applying SF reduction. However, the computational impact of using square-free reduction with DRI remains an interesting question. Empirically, we observed a better performance of DRI when the SF reduction is applied first. In addition to lowering the degrees of the involved polynomials (as it did for Lie-based proof rules), we observed that the order N SF for SF(h) is always lower than the order N for h. We, therefore, conjecture N SF ≤ N . However, we identified an example (cf. Ex. 45 below) for which square-free reduction resulted in a significant (×100) computational overhead due to the ideal membership checking (which we perform using Gröbner bases with reverse lexicographic monomial ordering). In our implementation of DRI, called DRI opt in the sequel, we use the square-free reduction only as a pre-processing step for the quantifier elimination problems in the premise of DRI.

Order parity decomposition

Similar to square-free reduction for invariant polynomial equations, one may sometimes remove roots of multiplicities greater than 1 from polynomial inequalities p ≤ 0, thereby simplifying their description and removing singularities on their boundary. To do this, we will require some definitions, due to Dolzmann and Sturm (see [START_REF] Dolzmann | Simplification of quantifier-free formulas over ordered fields[END_REF]).

Definition 47 (Square-free decomposition [START_REF] Dolzmann | Simplification of quantifier-free formulas over ordered fields[END_REF]). Given a polynomial h ∈ Z[x 1 , . . . , x n ], the square-free decomposition is given by

(h 1 , . . . , h n ) s.t. n i=1 h i i = h,
where all h i are square-free and relatively prime, i.e. gcd(h i , h j ) = 1.

Note that while superficially similar to square-free reduction, the square-free decomposition is quite different. To see this, note that the exponent in the product matches the index. Thus, the order in a square-free decomposition encodes the exponent to which the factor h i is raised in the original polynomial h, i.e. the factors raised to odd powers will have odd index in the decomposition; respectively for even exponents.

Definition 48 (Parity decomposition [START_REF] Dolzmann | Simplification of quantifier-free formulas over ordered fields[END_REF]). Given a polynomial h ∈ Z[x 1 , . . . , x n ] with square-free decomposition (h 1 , . . . , h n ), the parity decomposition is given by

odd i h i , even i h i .
Proposition 49 (Square-free equivalent [START_REF] Dolzmann | Simplification of quantifier-free formulas over ordered fields[END_REF]). Let h ∈ Z[x 1 , . . . , x n ] and let (h o , h e ) be the parity decomposition of h. Then the following equivalences hold: approach [START_REF] Prajna | A framework for worst-case and stochastic safety verification using barrier certificates[END_REF] breaks down completely, i.e. no barrier certificate exists for showing positive invariance of this set.

1. h = 0 ≡ R SF(h) = 0, 2. h = 0 ≡ R SF(h) = 0, 3. h > 0 ≡ R h o h 2 e > 0 ≡ R h o > 0 ∧ h e = 0, 4. h ≥ 0 ≡ R h o h 2 e ≥ 0 ≡ R h o ≥ 0 ∨ h e = 0, 5. h < 0 ≡ R h o h 2 e < 0 ≡ R h o < 0 ∧ h e = 0, 6. h ≤ 0 ≡ R h o h 2 e ≤ 0 ≡ R h o ≤ 0 ∨ h e = 0.
It is perhaps remarkable is that the output of SFEQ(h) ≤ 0 yields two subproblems, both of which we can solve using only sufficient proof rules: one is a non-strict inequality x 2 1 + x 2 2 -1 2 ≤ 0 for which one can apply the method of strict barrier certificates to prove its positive invariance; the other is a polynomial equality defining a smooth invariant curve x 2 1 + x 2 2 -1 = 0, which can also be handled (using e.g. the proof rule Lie).

By performing the above steps one proves that both disjuncts are positively invariant under the flow, and hence their disjunction is also positively invariant, concluding the proof that h ≤ 0 describes a positively invariant set. A formal proof of this property within a proof calculus needs an inference rule such as NSSBC, some appropriate rule for equational invariants, such as e.g. Lie, P-c or DRI, as well as the following special case of the generalization rule [START_REF] Platzer | Differential dynamic logic for hybrid systems[END_REF]:

(Inv ∨ ) S 1 → [ ẋ = p(x)] S 1 S 2 → [ ẋ = p(x)] S 2 S 1 ∨ S 2 → [ ẋ = p(x)] (S 1 ∨ S 2 )
. Proof. Nagumo is necessary and sufficient for proving positive invariance of closed sets and SFEQ returns a description of an equivalent set (over the reals). Thus, a closed set S is positively invariant using Nagumo if and only if an equivalent closed set SFEQ[S] is positively invariant using Nagumo.

Theorem 54. SFEQ LZZ ∼ LZZ.

Proof. Elementary, since LZZ is necessary and sufficient for proving positive invariance and SFEQ[S] gives an equivalent set in R n .

Experimental Comparison

To complement the theoretical deductive power comparison with a practical provability study, we empirically compare the running time performance of all the proof rules discussed in this paper on a heterogeneous collection of benchmarks (76 for algebraic sets and 20 for semi-algebraic sets).

Many premises of the considered proof rules are universally quantified sentences over the theory of real arithmetic. The purely existential fragment of real quantifier elimination has been shown to exhibit singly exponential time complexity in the number of variables (Basu et al., 1996). However, in practice this has not yet led to an efficient decision procedure, so typically it is much more efficient to use CAD [START_REF] Collins | Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition[END_REF][START_REF] Collins | Partial cylindrical algebraic decomposition for quantifier elimination[END_REF], which has doublyexponential running time in the number of variables. Theoretically, the upper bound on the complexity of deciding a sentence in the universal theory of R is given by (sd) O(n) , where s is the number of polynomials in the formula, d their maximum degree and n the number of variables (Basu et al., 1996).

Notice, in addition, that the proof rules, C-c, P-c, DRI and LZZ involve reasoning about multivariate polynomial ideal membership, which is an EXPSPACEcomplete problem over Q [START_REF] Mayr | Membership in polynomial ideals over Q is exponential space complete[END_REF]. Gröbner basis algorithms allow us to perform membership checks in ideals generated by multivariate polynomials. Significant advances have been made in algorithms for computing Gröbner bases [START_REF] Faugère | A new efficient algorithm for computing Gröbner bases without reduction to zero (F5)[END_REF] which in practice can be expected to perform very well. Our experimentation relies on the implementation of the CAD algorithm in Mathematica (version 10.0.1).

The examples we used originate from a number of sources-many come from textbooks on Dynamical Systems; some from the literature on formal verification of hybrid systems; others have been hand-crafted to tease out sweetspots of certain proof rules. The most interesting experimental question we seek to address here is whether the greater generality of the more deductively powerful proof rules also comes at a substantially higher computational cost when assessed across the entire spectrum of examples. As a complement to the theoretical deductive power relationships between the different proof rules (Section 6), we also seek to identify some nuances in the complexity of the conditions in the premises, which the coarse-grained complexity bounds miss, being highly sensitive to the number of variables.

The proof rule Nagumo is intractable since it requires computing the contingent cone to a given semi-algebraic set. All algebraic sets are of the form h = 0, for which LZZ and DRI will ultimately result in the same conditions; only DRI and its optimized implementation DRI opt (see Section 7.3) will be considered in the benchmarks. 6 We have also established that NSSBC cannot discharge any invariant algebraic set and that DI applied to candidates of the form h = 0 is equivalent to FI. Thus, two comparisons are of interest: the set of proof rules for algebraic sets (Section 8.1) and the set of poof rules for semi-algebraic sets (Section 8.2).

From our experiments it emerges that the proof rules exhibit different (and at times surprising) trade-offs between generality and efficiency.

Running Time Performance for Algebraic Sets

In this section, the prefix SF is implicit for all Lie-based proof rules. We consider 4 equally sized classes of invariant sets: (1) 24 smooth invariants, where Lie is both necessary and sufficient, (2) 17 isolated equilibria as trivial (for humans, not machines) equational invariants for which both Lie • and Lie * provide necessary and sufficient conditions, (3) 17 other singularities and high integrals, (4) 18 functional invariants, where FI is necessary and sufficient. Figure 12 compares the number of invariant varieties that each rule could prove within 60 seconds. The vertical axis shows cumulative time spent on the problems. All runs were performed on an Intel Core i5 1.7GHz machine with 4Gb RAM. Generally, we observe DRI performing very well across the entire spectrum of problem classes. This is very encouraging, but also at first sight appears to defy intuition since it implies that one does not necessarily sacrifice performance when opting to use a more deductively powerful rule. In this graph, we also see that overall Lie • appears to offer an interesting compromise between deductive power and efficiency-it is able to prove a significant body of problems that are out of scope for Lie, while avoiding the complexity penalty which affects Lie * (due to introducing an extra variable).

A more careful analysis of the benchmarks reveals interesting relationships that are obscured in the "big picture"; to see them, one needs to consider the individual classes of invariants for which some of the sufficient conditions in the rules are in fact necessary and sufficient. Together with DRI, this yields two decision procedures for each class and allows us to focus only on running time performance and assess the practicality of each proof rule. In Fig. 13, we observe the rules Lie • and Lie * performing very well in proving invariance of isolated equilibria. This is to be expected as Lie • in particular was formulated with this problem class in mind. It is interesting that DRI remains highly competitive here; though its performance is slightly worse in our set of benchmarks.

It is clear that because proof rules Lie • and Lie * generalize Lie, they will be able to prove every problem in the smooth invariant benchmarks. The running time performance of the three rules is almost identical, with Lie offering a slight speed-up over its generalizations. The premises of Lie • and Lie * impose condi- tions on states in the singular locus, which is the empty set for smooth invariants; this, in practice, appears to be slightly more expensive than checking an equivalent property that the gradient is non-vanishing on the variety (as in the premise of Lie).

The proof rules FI and P-c, corresponding to conditions with historical origins in the study of integrability of dynamical systems, can be seen to perform very well in proving functional invariants, while performing very poorly in benchmarks for isolated equilibria. In proofs of smooth invariants their behaviour is radically different, with FI proving only a handful of examples and P-c succeeding in proving most of the problems very efficiently. This can be explained by the fact that P-c generalizes FI and is therefore more deductively powerful. P-c appears slightly slower at proving functional invariants, but shows very impressive running time performance for some problems from the smooth invariant bench-marks, where it is the fastest proof rule for many of problems where it succeeds. Comparing running time performance with DRI, we see that DRI is only slightly slower at proving functional invariants than FI and P-c. Again, the performance gap between DRI and the two rules appears to be insignificant for most problems. Theoretically, when P-c proves an invariant, DRI applies conditions that are identical to the premise of P-c. Hence, although DRI is a generalization, this does not come at a significant extra cost for the classes where P-c shows good running time performance. The slightly greater running time of DRI compared to that of P-c can be accounted for by the fact that in our implementation DRI computes the Gröbner basis for every order N including for N = 1 where such computation is unnecessary.

For functional invariants, FI (i.e. the equality fragment of DI) benefits from the fact that the condition in its premise, which requires to show that the Lie derivative evaluates to zero everywhere, is equivalent to showing that the Lie derivative is the zero polynomial, which can be checked very efficiently by symbolic computation, without a decision procedure for real arithmetic.

In the examples featuring singularities and high integrals in the benchmarks we see DRI as the clear winner, simply because there was no other rule that was tailored to work on this class. Indeed, the structure of these invariant sets can be rather involved, making it difficult to characterize in a single proof rule; however, sometimes it is possible to exploit the structure of high integrals inside a proof system and arrive at efficient proofs that outperform DRI (Ghorbal et al., 2014).

It is not surprising that DRI should ultimately overtake all the other rules in terms of deductive power (it is, after all, necessary and sufficient); what is remarkable is that the performance we observe for DRI is often very competitive to that of the sufficient rules when they also succeed at a proof. This observation suggests a possible strategy for proof search in a proof system: give precedence to DRI and switch to other sufficient rules if DRI takes longer than some time-out value. The rationale behind this decision is our empirical observation that DRI performs consistently well on all problem classes we considered, but it is also sometimes possible to save time by using a proof rule which is less deductively powerful. It is important to note here that the overall proof system benefits from including the sufficient proof rules, rather than relying solely upon DRI.

Running Time Performance for Semi-algebraic Sets

In Fig. 14 we compare the running time performance of the proof rule LZZ versus the sufficient conditions DI (Fig. 14a) and NSSBC (Fig. 14b). Two different sets of 10 benchmarks each were selected to exploit the sweetspots of DI and NSSBC respectively. We observe that whenever DI can prove invariance in the problem at hand, it is much faster than LZZ. This is expected: the quantifier elimination problems required by the proof rule LZZ are much more involved than those found in the premise of DI. This should be balanced by the fact that DI is more restrictive. In the set of benchmarks for NSSBC, one can observe that DI does not prove any of the problems. In Fig. 14b, one can also notice that LZZ still performs well compared to NSSBC. Indeed, the premise of the proof rule NSSBC can involve complicated real arithmetic problems that are sometimes even more difficult than those appearing in the premise of the proof rule LZZ. Generally, the size of the conditions in the premise of NSSBC grows rapidly with the size of the formula describing the invariant candidate. The distribution property in Theorem 19 avoids this problem in LZZ.

Conclusion

This article investigated an important aspect of deductive safety verification of continuous and hybrid dynamical systems. Namely, given the abundance of existing sufficient conditions for invariant checking and the recently developed necessary and sufficient conditions for real algebraic (Ghorbal and Platzer, 2014) and semi-algebraic [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF] invariants, it is crucial to know whether the gains in deductive power come at the price of greater computational complexity and poor running time performance that would hinder practical applications. The work presented in this article leads us to arrive at the following conclusions:

• Empirically, we observe that the deductively powerful rule for algebraic invariants (DRI) performs very well in checking invariance of polynomial

Figure 1 :

 1 Figure 1: Proof rules for checking the invariance of h = 0 w.r.t. p: FI, C-c and P-c (Sankaranarayanan et al., 2008, Lemma 2), Lie (Olver, 2000, Theorem 2.8), DRI (Ghorbal and Platzer, 2014, Theorem 2)

Figure 2 :

 2 Figure 2: Closure properties of the contingent cone at an intersection of two closed sets. The intersection of the contingent cones to the two sets is shown in red. The contingent cone to the intersection itself is {0}.

Figure 3 :Figure 4 :

 34 Figure 3: Sign conditions on Lie derivatives in the construction of In p (h ≤ 0) with N = 3.

Figure 5 :

 5 Figure 5: Hasse diagram. An arrow R 1 → R 2 means R 1 ≺ R 2 ; absence of connecting arrow(s) means (≺ ).

FIFigure 6 :

 6 Figure 6: Comparison matrix for proof rules for algebraic sets (the numbers refer to the respective propositions).

Figure 7 :

 7 Figure 7: Invariant functions and invariant equations.

Proposition 36 .

 36 Let ∈ {FI, C-c, P-c, Lie, Lie • , Lie * , DRI}, then ≺ NSSBC and DI. The proof rule DI cannot generalize C-c, P-c, Lie ,Lie • , Lie * , and DRI. For the same reason FI cannot generalize those proof rules (cf. Section 6.1). Thus: Proposition 37. Let ∈ {C-c, P-c, Lie, Lie • , Lie * , DRI}, then ≺ DI.

Figure 10 :

 10 Figure 10: Square-free Reduction (Summary)

Figure 11 :

 11 Figure 11: Positively invariant set given by h ≤ 0 (in red).

Theorem 52 .

 52 SFEQ DI ≺ DI Proof. Corollary to Proposition 40, since FI is a special case of DI and SFEQ[h = 0] ≡ SF(h) = 0. Theorem 53. SFEQ Nagumo ∼ Nagumo.

FIFigure 12 :

 12 Figure 12: Experimental performance of proof rules: problems solved per time (log scale)

FIFigure 13 :

 13 Figure 13: Number of problems solved per class (log scale).

Figure 14 :

 14 Figure 14: Number of problems solved in each class (times on log scale).

That is explicitly given in terms of elementary functions and usual operators.

That is, the rate of change of the system over time explicitly depends only on the system's state, not on time. Non-autonomous polynomial systems with time-dependence can be made autonomous by extending the state of the system with an extra clock variable that reflects the progress of time and replacing every instance of the time variable with the new clock variable.

The border of a set S is often denoted by ∂S. We will use bdr(S) instead to avoid confusion with partial derivatives.

We used the notation DI = for the same proof rule in[START_REF] Ghorbal | A hierarchy of proof rules for checking differential invariance of algebraic sets[END_REF].

See(Dumortier et al., 2006, Proposition 8.4) for a similar proposition over the complex numbers.

We refer the reader to(Ghorbal et al., 2014) for a more detailed discussion of the differences and similarities between the Liu, Zhan & Zhao characterization[START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF] and the differential radical characterization(Ghorbal and Platzer, 2014).

Acknowledgments. The authors would like to thank Dr. Ashish Tiwari at SRI International for his kind and informative response to our technical query and extend special thanks to Dr. Paul B. Jackson at the LFCS, University of Edinburgh, for his valuable help in improving the manuscript. Basu, S., Pollack, R., Roy, M.-F., 1996. On the combinatorial and algebraic complexity of quantifier elimination. J. ACM 43 (6), 1002-1045. Blanchini, F., Miani, S., 2008. Set-Theoretic Methods in Control. Systems & Control : Foundations & Applications. Birkhäuser.

$ This material is based upon work supported by the National Science Foundation (NSF) under NSF CAREER Award CNS-1054246, NSF EXPEDITION CNS-0926181, NSF CNS-0931985, by DARPA under agreement number FA8750-12-2-029, as well as the Engineering and Physical Sciences Research Council (UK) under grant EP/I010335/1.

of the limiting cycle x 2 1 + x 2 2 -1 = 0 is provable with Lie but not FI, see Fig. 7 (right).

We now prove that Lie-based proof rules {Lie, Lie • , Lie * }, and Darboux-based proof rules {FI, C-c, P-c} are two distinct families of proof rules; that is, any Liebased proof is deductively incomparable to any Darboux-based proof rule. The following lemma follows from the transitivity of the partial order.

Proof. Consider three proof rules R 1 , R 2 and R 3 . If R 2 R 3 , using R 1 R 2 , one gets by transitivity R 1 R 3 , which contradicts the assumption R 3 ≺ R 1 . The following example proves that FI Lie * : Consider the three-dimensional vector field p = (x 2 , -x 1 , 0). The invariance of the equation x 2 3 +(-1+x 2 1 +x 2 2 +x 2 3 ) 2 = 0 cannot be established using Lie * (the singular locus is a circle in R 3 ), but is easily provable using FI as L p (h) vanishes. Proof. To complete the proof, we still need an example showing that Lie P-c. Consider the vector field p = (3(-4 + x 2 ), 3 + xy -y 2 ), the proof rule Lie fails to prove that the equation h = -3+x 2 +2xy +6y 2 +2xy 3 +y 4 = 0 is invariant as the singular locus of h contains (-2, 1) and (2, -1). However, L p (h) = (6x -4y)h and therefore P-c proves that h = 0 is an invariant equation.

The remaining cases follow from the results established above.

Example 45. Consider the following vector field p:

and let

Attempting to prove that h = 0 is invariant under the flow of this system using DRI we observe running time of under 2 seconds. Reducing h to be square-free results in DRI running for over 8 minutes before it is able to prove the result. In this case, square-free reduction introduces a performance penalty when checking for polynomial ideal membership (which is performed using Gröbner bases with reverse lexicographic monomial ordering). We see that one needs to be careful when using square-free reduction with DRI because even though it is reasonable to expect better performance due to lower degrees in square-free reduced polynomials, performing this step may make the Gröbner basis computation more difficult for some problems.

Remark 46. Notice that Prop. 42 does not have an analogue for DRI. In other words, if a polynomial equation h = 0 is invariant for p, its irreducible factors need not define invariant equations themselves. Geometrically, this means that if a variety is invariant under the flow of p, its irreducible components need not be invariants under the flow of p. For instance, consider the irreducible polynomials q 1 = y -1 and q 2 = x 2 + (y -1) 2 . The equation q 1 q 2 = 0 which is equivalent to y = 1, is invariant for p = (1, 0), since the premise of the proof rule DRI holds true for N = 3. However, the equation q 2 = 0, which is equivalent to x = 0 ∧ y = 1, is not an invariant equation for p. The reason for the invariance of q 1 q 2 = 0, which is equivalent to q 1 = 0 ∨ q 2 = 0, stems from q 1 not from q 2 . The resulting (rightmost) equivalent formulas are guaranteed to only feature square-free polynomials and are called square-free equivalents.

For a semi-algebraic set S given by a quantifier-free formula of real arithmetic, we define SFEQ[S] to be the square-free equivalent formula obtained by applying the equivalences in Proposition 49 to each atomic formula in S. Using the SFEQ reduction as a pre-processing step for the proof rule NSSBC is denoted SFEQ NSSBC and accordingly for SFEQ DI and SFEQ Nagumo.

Theorem 50. SFEQ NSSBC NSSBC.

Proof. If L p (h) < 0 is true when h is an active component (h = 0), it is necessarily the case that h is square-free. Thus SFEQ(h) = h (which then equals SF(h)) and, therefore, SFEQ NSSBC NSSBC. Let ẋ = p(x) = (-x 1 , -x 2 ) and consider the set S ≡ (x 2 1 + x 2 2 -1) 3 ≤ 0. Applying NSSBC fails to prove the positive invariance property. Computing the order parity decomposition, we get SFEQ(S) ≤ 0 ≡ (x 2 1 + x 2 2 -1) ≤ 0, for which positive invariance under the flow of p(x) is proved easily using NSSBC.

Example 51 (Positive invariant defined by polynomial inequality). Let us consider a system with an unstable limit cycle around a stable origin:

Suppose we wanted to show that the set of states satisfying the following inequality is positively invariant:

Let us refer to this set as h ≤ 0. As can be seen from the phase portrait in Figure 11, the set h ≤ 0 is indeed positively invariant under the flow; however, h is not square-free, but h ≤ 0 has the following square-free equivalent:

This is an example of a positively invariant set described by a non-strict polynomial inequality where applying NSSBC will fail. In fact, the barrier certificate equalities.

• P-c is made redundant by DRI (DRI strictly increases the deductive power of P-c while being equally efficient).

• Reducing polynomials to square-free form is always beneficial to the proof rule Lie and its generalizations, where it yields improvements in both the deductive power and the running time performance.

• Using the square-free reduction with the proof rules FI and C-c yields new incomparable proof rules, whereas SF with P-c is as powerful as P-c alone.

• Performing square-free reduction of an invariant candidate may introduce a performance penalty for DRI and therefore cannot be regarded as an optimization, even though there are instances for which it yields a speed-up. The same can be said of order parity decomposition applied to an invariant candidate supplied to LZZ.

• Sufficient rules DI and NSSBC can afford a speed-up on certain problems, but the overall running time performance of the decision procedure LZZ is observed to be good.

• Using a decision procedure LZZ appears to be more efficient than using the sufficient condition NSSBC when the positively invariant candidate set is described by a large formula.

Our next step is to use these highlighted insights to build efficient proof strategies that intelligently combine different proof methods to efficiently construct formal proofs, e.g., by favoring the most deductively complete rules that come without significant practical performance penalties on the most common cases of invariants.