Khalil Ghorbal
email: khalil.ghorbal@inria.fr

Andrew Sogokon
email: a.sogokon@soton.ac.uk

Characterizing Positively Invariant Sets: Inductive and Topological Methods

Keywords: Ordinary differential equations, dynamical systems, positively invariant sets, polynomial vector fields, decision procedures

. The procedure ESE, introduced in this article, works by splitting the problem, in a principled way, into simpler sub-problems that are easier to check, and is shown to exhibit substantially better performance compared to LZZ on problems featuring semi-algebraic sets described by formulas with non-trivial Boolean structure.

Introduction

Positive invariance is an important concept in the theory of dynamical systems and one which also has practical applications in areas of computer science, such as formal verification, as well as in control theory. Informally, a set is positively invariant if it is preserved under the evolution of the system according to the dynamics as time advances. A considerable amount of literature is dedicated to this subject [START_REF] Blanchini | Set invariance in control[END_REF], and great progress has been made in understanding positively invariant sets in continuous dynamical systems.

In computer science, the notion of an inductive invariant is analogous to that of a positively invariant set. It has relatively recently become the focus of considerable research interest, especially in the area of so-called hybrid systems, which studies systems that combine discrete and continuous dynamics. Significant progress has been made over the past decade in the methods for algorithmically checking inductive invariants of ODEs (i.e. deciding whether a given set is positively invariant); these methods provide powerful tools for reasoning about the temporal behaviour of ODEs without the need to explicitly solve them. For example, one may use an inductive invariant to prove that a system cannot evolve from a given set of initial conditions into a state which is deemed undesirable or unsafe (e.g. if the ODEs describe the motion of physical objects, one may wish to know that there can be no collisions between these objects in the future).

Contributions. This article presents a self-contained development of two characterizations of positively invariant sets of continuous systems (in Theorem 6 and Theorem 23). In the case of semi-algebraic sets and polynomial ODEs, the two characterizations lend themselves to two alternative decision procedures for checking set positive invariance, both of which are described in detail.

Section 3 is entirely devoted to the first characterization (Theorem 6), which relies on the concept of inward sets (see Zhan et al., 2017, Def. 9.4) and is very closely related to a theorem (Zhan et al., 2017, Thm. 9.1) which originally appeared in [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF]; we show how real induction, via equivalent, yet subtly different formulations, can be used to give clean proofs of this known result and of Theorem 6. The section then describes a robust implementation of the associated decision procedure (LZZ, after Liu, Zhan and Zhao), along with our improvements to the original method.

Section 4 presents the second characterization (Theorem 23), which is based on Conley's notion of exit sets [START_REF] Conley | Isolated Invariant Sets and the Morse Index[END_REF]. We give a direct proof for this new result while formally establishing the relationship between exit sets and inward sets. Section 4.3 presents a new algorithm (ESE, which stands for Exit Set Emptiness) that can more efficiently decide positive invariance of semialgebraic sets described by formulas with non-trivial Boolean structure. The procedure works by splitting the problem into simpler sub-problems that are easier to check, reminiscent of divide-and-conquer algorithms.

Our implementations of the two decision procedures LZZ and ESE are empirically evaluated on a number of positive invariance checking problems where semi-algebraic sets are described by non-atomic formulas in Section 5, with ESE exhibiting substantially better performance.

Preliminaries

A system of autonomous ordinary differential equations (ODEs) has the form:

x 1 = f 1 (x 1 , . . . , x n ) , . . .

x n = f n (x 1 , . . . , x n ) ,
where x i stands for the time derivative dxi dt and f = (f 1 , f 2 , . . . , f n ) is a vectorvalued continuous function (which defines a vector field on R n ); we will write such a system more concisely as x = f (x). We will denote by ϕ(•, x) the solution to the initial value problem x = f (x), with initial value x ∈ R n . We will only consider systems in which solutions to initial value problems always exist (at least locally) and are unique (e.g. local Lipschitz continuity of f is sufficient to guarantee this property). When we quantify solutions over time t, we only consider t in the maximal interval of existence I x , which in our case exists for any x and contains 0. In order to simplify our presentation, we will quantify over "all forward time" by writing ∀ t ≥ 0 with the understanding that ϕ(•, x) may only be defined for t ∈ I x . We refer to the mapping ϕ as the (local) flow of the vector field f . Definition 1 (Positively invariant set). Given a system of ODEs x = f (x), a set S ⊆ R n is positively invariant if and only if no solution starting inside S can leave S in the future, i.e. just when the following holds: ∀ x ∈ S. ∀ t ≥ 0. ϕ(t, x) ∈ S .

One analogously arrives at a definition of negatively invariant sets in which no solution starting inside the set S is permitted to be outside the set in the past. Basic results in the theory of dynamical systems establish that a set S is positively invariant precisely when its complement S c is negatively invariant (Bhatia and Szegő, 1970, Thm. 1.4), and that the closure of a positively invariant set is also positively invariant (Alongi and Nelson, 2007, Prop. 1.4.5); this property also holds for the set's interior (Bhatia and Szegő, 1970, Thm. 1.7).

Remark 2. Some authors [START_REF] Blanchini | Set-Theoretic Methods in Control[END_REF] favour a definition of positively invariant sets in which the solutions ϕ(t, x) are explicitly required to exist for all time t ≥ 0, by imposing a global Lipschitz continuity requirement on the vector field f , whereas others [START_REF] Redheffer | The theorems of Bony and Brezis on flow-invariant sets[END_REF] simply require that solutions emanating from the set S remain inside S for as long as they exist in the future (Definition 1 is stated in this spirit).

The first necessary and sufficient condition (i.e. characterization) for positive invariance of closed sets in systems of ODEs with unique solutions (but without requiring knowledge of the solutions ϕ) was given by [START_REF] Nagumo | Über die Lage der Integralkurven gewöhnlicher Differentialgleichungen[END_REF], 1 and was later independently found by numerous other mathematicians (the interested reader is invited to consult [START_REF] Blanchini | Set invariance in control[END_REF], (Blanchini and Miani, 2008, Ch. 4, §4.2), and (Walter, 1998, Ch. III, §10, XV, XVI) for more details about Nagumo's theorem and its multiple rediscoveries). Informally, Nagumo's theorem states that a closed set S is positively invariant if and only if at each point x on the boundary of S the vector f (x) points into the interior of the set or is tangent to it. The theorem may be easily applied in cases where the set S is a sub-level set of a differentiable real-valued function g, i.e. a set defined as {x ∈ R n | g(x) ≤ 0}, provided that the gradient vector ∇g(x) is non-vanishing (i.e. non-zero) whenever g(x) = 0 (intuitively this ensures that the boundary of S is smooth): in this special case Nagumo's theorem says that S is positively invariant if and only if g (x) ≤ 0 for all x such that g(x) = 0, where g denotes the (first) Lie derivative of g with respect to the vector field f , which is defined by: 2

g def = ∇g • f = n i=1 ∂g ∂x n f i .
Remark 3. Applying Nagumo's theorem in practice becomes problematic when the boundary of S is not smooth, e.g. when the set {x ∈ R n | g(x) = 0} contains singularities (points x where the gradient vanishes, i.e. ∇g(x) = 0); these issues have been explored by [START_REF] Taly | Deductive verification of continuous dynamical systems[END_REF]. In order to apply the theorem more generally to sets that are intersections of sub-level sets, i.e. {x ∈ R n | g i (x) ≤ 0, i = 1, . . . , k}, one likewise needs to be very careful. The concept of practical sets was introduced specifically to deal with these issues (see Blanchini and Miani, 2008, Ch. 4, Def. 4.9).

In the following sections we will be concerned with characterizations of positive invariance that are of a very different nature to that of Nagumo's result (which provides a characterization only for closed sets obtained using the tools of real analysis and is without effective computational means of applying it). As we shall see, these alternative characterizations can be effectively applied using tools from commutative algebra and real algebraic geometry.

Characterizing Positive Invariance Through Inward Sets

Let us consider the following construction of the so-called inward set for a given set S ⊆ R n and a system of ODEs x = f (x) for which a unique (local) solution to the initial value problem exists for any x ∈ R n , following (Zhan et al., 2017, Def. 9.4):

In f (S) def = {x ∈ R n | ∃ ε > 0. ∀ t ∈ (0, ε). ϕ(t, x) ∈ S} .
1 Nagumo's result was in fact a little more general in that it did not require unique solutions and focused on so-called weak positive invariance, which is identical to positive invariance when solutions are unique.

2 The Lie derivative of g is sometimes also denoted by L f (g) instead of g .

When time/flow is reversed, one can likewise construct the inverse inward set:

In -f (S) = {x ∈ R n | ∃ ε > 0. ∀ t ∈ (0, ε). ϕ(-t, x) ∈ S} .
It is useful to intuitively think of these as sets of states from which the system will evolve inside S for some non-trivial time interval "immediately in the future" and, respectively, has evolved inside S for some non-trivial time interval "immediately in the past". We observe that, although according to the statement of In f (S), x can be any point in R n , it is in fact restricted to the closure of S.

Lemma 4. For S ⊆ R n , the set In f (S) is a subset of the closure of S.

Proof. We show by contradiction that In f (S) ∩ (S c ) • is empty. Let x be an element of the intersection. Since x ∈ (S c ) • , there exists an open neighbourhood U ⊂ (S c ) • of x and ρ > 0 such that ϕ(t, x) ∈ U ⊂ S c for all t ∈ (0, ρ) (by continuity of ϕ(•, x)). But if x ∈ In f (S), then there exists ε > 0 such that ϕ(t, x) ∈ S for all t ∈ (0, ε). So ϕ(t, x) is in both S c and S for all t ∈ (0, min{ρ, ε}), a contradiction.

Remark 5. Notice that the interior of S is always contained inside In f (S) (by definition) and the inclusion S ⊆ In f (S) therefore holds trivially whenever S is an open set (for any f ). A quick glance at the definitions These constructions can be used to state the following characterization of positively invariant sets. Theorem 6. A set S ⊆ R n is positively invariant under the flow of the system x = f (x) if and only if S ⊆ In f (S) and S c ⊆ In -f (S c ).

In f (S c ) = {x ∈ R n | ∃ ε > 0. ∀ t ∈ (0, ε). ϕ(t, x) ∈ S} , In f (S) c = {x ∈ R n | ∀ ε > 0. ∃ t ∈ (0, ε). ϕ(t, x) ∈ S} ,
Theorem 6 can be understood and proved using induction over the nonnegative real numbers. Though there are many different variations of induction over the reals (e.g. see [START_REF] Clark | The instructor's guide to real induction[END_REF], this method of proof appears to be far less well known than standard mathematical induction over the natural numbers. We state below a version of real induction that is well suited to directly prove the theorem.

Lemma 7 (Real induction). A predicate P (t) holds for all t ≥ 0 if and only if:

1. P (0) , 2. ∀ t ≥ 0. ¬P (t) → ∃ ε > 0. ∀ T ∈ (t -ε, t). ¬P (T ) , 3. ∀ t ≥ 0. P (t) → ∃ ε > 0. ∀ T ∈ (t, t + ε). P (T ) .
Proof. Necessity is obvious. Sufficiency is easy to show by considering (for contradiction) that there exists t ≥ 0 such that ¬P (t) and defining the time t * = inf{t ≥ 0 | ¬P (t)} (which exists as the set is assumed to be non-empty, is bounded from below, and the reals are complete). By 1. and 3. we have that t * = 0, so t * must be positive, but in this case P (t) holds for all t ∈ [0, t * ) (by definition). If P (t * ) holds, then t * cannot be an infimum (by 3.), and if ¬P (t * ) then (by 2.) we have that ¬P (t) holds for all t ∈ (t * -ε, t * ) for some ε > 0; a contradiction.

Using the above real induction principle, the proof of Theorem 6 is immediate if one takes "ϕ(t, x) ∈ S" to be the predicate P (t) in Lemma 7. We remark that (unlike Nagumo's theorem), Theorem 6 makes no assumptions about the set S being closed, or open. As such, Theorem 6 is very general and applies to all sets and systems of ODEs with locally unique solutions.

Theorem 6 is closely related to (Zhan et al., 2017, Thm. 9.1) where the authors require

S c ⊆ In -f (S) c instead of S c ⊆ In -f (S c ). 3 Despite the fact that, in general, In -f (S) c = In -f (S c ) (cf. counterexample 19
), the conditions in Theorem 6 and (Zhan et al., 2017, Thm. 9.1) are in fact equivalent. We show this equivalence by appealing again to real induction: we first state a slightly different real induction principle that is more suited to prove (Zhan et al., 2017, Thm. 9.1), providing thereby a new simpler proof for this known result, and then show that both principles are in fact equivalent. 4Lemma 8 (Real induction (Jackson)). A predicate P (t) holds for all t ≥ 0 if and only if:

1. P (0), 2'. ∀ t > 0. ∃ ε ∈ (0, t]. ∀ T ∈ (t -ε, t). P (T ) → P (t) , 3. ∀ t ≥ 0. P (t) → ∃ ε > 0. ∀ T ∈ (t, t + ε). P (T ) .
Notice that condition 2'. could be equivalently replaced by its contrapositive form

2". ∀ t > 0. ¬P (t) → ∀ ε ∈ (0, t]. ∃ T ∈ (t -ε, t). ¬P (T ) .
Proof. Necessity is obvious. Sufficiency is easy to show by considering (for contradiction) the time t * = inf{t ≥ 0 | ¬P (t)}. By 1. and 3. we have that t * = 0, so t * must be positive, but in this case P (t) holds for all t ∈ [0, t * ) (by definition) and by 2'. we have that P (t * ) holds; a contradiction. Remark 9. For completeness, we include below a statement of Hathaway's continuity induction [START_REF] Hathaway | Using continuity induction[END_REF], which is very similar to the notion of real induction in [START_REF] Clark | The instructor's guide to real induction[END_REF]. A predicate P (t) holds for all t ∈ [0, T ], where T > 0, if and only if:

1. P (0) holds , 2. ∀ τ ∈ (0, T ]. ∀ τ ∈ [0, τ ). P (τ ) → P (τ ) , 3. ∀ τ ∈ [0, T ). ∀ τ ∈ [0, τ ]. P (τ ) → ∃ > 0. ∀ τ ∈ (τ, τ + ). P (τ ) .
The proof is essentially identical to that of Lemma 8.

The proof of (Zhan et al., 2017, Thm. 9.1) now becomes immediate using real induction as it is stated in Lemma 8. The following lemma establishes an equivalence between the two formulations of real induction.

Lemma 10. Let P (t) denote a predicate defined for all t ≥ 0. If 1. P (0) , and

3. ∀ t ≥ 0. P (t) → ∃ ε > 0. ∀ T ∈ (t, t + ε). P (T ) hold , then 2. ∀ t ≥ 0. ¬P (t) → ∃ ε > 0. ∀ T ∈ (t -ε, t). ¬P (T ) , if and only if 2". ∀ t > 0. ¬P (t) → ∀ ε ∈ (0, t]. ∃ T ∈ (t -ε, t). ¬P (T ) .
Proof. The implication from 2. to 2". is obvious (in this sense, one may consider Lemma 7 weaker than Lemma 8). To prove the converse, suppose (for contradiction) that 2". and ¬2. both hold. More explicitly:

¬2. ≡ ∃ t ≥ 0. ¬P (t) ∧ ∀ ε > 0. ∃ T ∈ (t -ε, t). P (T ) .
Let τ > 0 be the point at which ¬P (τ ) holds in ¬2. (τ cannot be 0 by 1.) Then for all ε 0 > 0, there exists some T 0 ∈ (τ -ε 0 , τ ) such that P (T 0 ) holds. Consider the interval I 0 = [T 0 , τ ]. At T 0 , since P (T 0 ) holds, we have (by 3.) that P (t) holds for all t in the interval I 1 = [T 0 , T 0 + ε 1 ) for some ε 1 > 0. If T 0 + ε 1 ≥ τ , we obtain a contradiction (because ¬P (τ ) is assumed to hold); otherwise we have

I 1 = [T 0 , T 0 + ε 1 ) ⊂ [T 0 , τ ].
If at the endpoint of I 1 we have that ¬P (T 0 + ε 1 ) holds, we obtain a contradiction (by 2".), and if P (T 0 + ε 1 ) holds we have (by 3.) that for some ε 2 > 0, P (t) holds for all t ∈ I 2 = [T 0 , T 0 + ε 1 + ε 2 ). Repeating the argument, we obtain a sequence I k of intervals of strictly increasing length where P (t) holds. The right endpoints of the intervals in this sequence cannot converge within (T 0 , τ ] because this would yield a contradiction (by 2".). The right endpoints thus go beyond τ , which again yields a contradiction.

The equivalence stated in Lemma 10 is somewhat abstract and it may not be immediately clear how this equivalence is relevant with regard to inward sets. To make this more apparent, we prove below a lemma which can be used to establish the equivalence between Theorem 6 and (Zhan et al., 2017, Thm. 9.1) without appealing to real induction directly in the proof, although following a similar line of argument as that employed in the proof of Lemma 10.

Lemma 11. Let S ⊆ R n . If S ⊆ In f (S) then In -f (S) = In -f (S c ) c .
Proof. The inclusion In -f (S) ⊆ In -f (S c ) c holds in general by definition as already stated. Let x ∈ In -f (S c ) c and let ε 0 > 0. Then, by definition, there exists t 0 ∈ (0, ε 0 ), such that x 0 := ϕ(-t 0 , x) ∈ S c , or equivalently x 0 ∈ S. Since S ⊆ In f (S), x 0 ∈ In f (S) and there exists γ 0 > 0, such that for all s 0 ∈ (0, γ 0 ), ϕ(s 0 , x 0 ) ∈ S. If -t 0 + γ 0 < 0, then the same arguments with ε 1 := t 0 -γ 0 lead to the existence of t 1 , γ 1 > 0 such that for all s 1 ∈ (0, γ 1 ), ϕ(s 1 , x 1 ) ∈ S where x 1 := ϕ(-t 1 , x). We can thus construct a (strictly) increasing sequence -t 0 + γ 0 , -t 1 + γ 1 , . . . . Two cases may occur:

(i) If the sequence crosses zero after finitely many steps, that is there exists n ≥ 0 such that -t n + γ n ≥ 0, then this means that for all t ∈ (0, t n ), ϕ(-t, x) ∈ S thereby proving that x ∈ In -f (S) since -t n < -t < 0 ≤ -t n + γ n .

(ii) If the sequence is upper bounded by 0, then it has a limit -t l + γ l ≤ 0. The case -t l + γ l < 0 is impossible since we can perform one more step to get -t l + γ l < -t l + γ l ≤ 0. Thus -t l + γ l = 0 and one gets ϕ(-t, x) ∈ S for all t ∈ (0, t l ) leading, as in case (i), to x ∈ In -f (S).

Remark 12. The statement of the characterization in Theorem 6 enjoys some rather nice properties when compared to that of (Zhan et al., 2017, Thm. 9.1). It is in particular symmetric in the sense that the set inclusions in the theorem are preserved when one simultaneously replaces S with its complement S c and f with the reversed dynamics -f . This allows for instance to immediately prove the well-known result in dynamical systems which states that a set is positively invariant if and only if its complement is negatively invariant (Bhatia and Szegő, 1970, Thm. 1.4). One sees that by syntactically replacing S with S c and f with -f in the conditions of Theorem 6, one obtains S c ⊆ In -f (S c ) and S ⊆ In f (S), i.e. equivalent conditions, using only the set-theoretic fact that (S c ) c = S. On the other hand, applying the same transformation to the conditions S ⊆ In f (S) and S c ⊆ In -f (S) c required in (Zhan et al., 2017, Thm. 9.1), one does not immediately obtain the same conditions; instead, one obtains S c ⊆ In -f (S c ) and S ⊆ In f (S c ) c . In order to show that the original inclusions hold one needs to use the fact that In -f (S c ) ⊆ In -f (S) c for the first inclusion, and then use Lemma 11 for the second inclusion, which is somewhat more involved than using Theorem 6 to prove the same fact.

The main practical difficulty in applying Theorem 6 (or equivalently (Zhan et al., 2017, Thm. 9.1)) lies in the fact that inward sets In f (S) and In -f (S c ) are defined in terms of solutions to a system of differential equations; the theorem says nothing about our ability to construct these sets or reason about their inclusion. The following section will elucidate how this problem is addressed using tools from algebraic geometry in the important case where the set S is semi-algebraic and the right-hand side of the system x = f (x) is polynomial.

A Decision Procedure for Checking Positively Invariant Sets

In this section we describe a procedure for deciding whether a given set is positively invariant or not. For this we first require a few basic results. Let g : R n → R denote a real-valued function. The zero-th Lie derivative of g is g itself, the first order Lie derivative g def = ∇g•f corresponds to the total derivative of t → g(ϕ(t, x)) with respect to time t, and higher-order Lie derivatives are defined inductively, i.e. g = (g ) ; the k-th order Lie derivative of g will be denoted by g (k) . We will require the fact that unique solutions to real analytic systems of ODEs are also real analytic (Chicone, 2006, Thm 1.3). Whenever g is a real analytic function, its Taylor series expansion

g(ϕ(t, x)) = g(x) + g (x)t + g (x) t 2 2! + • • • converges in some time interval ( l , u ), where l < 0 < u . The set of states {x ∈ R n | g(x) = 0}
, simply denoted by g = 0 in the sequel, remains invariant under the flow for some non-trivial forward time interval if and only if all Lie derivatives g (k) , k ≥ 1, vanish whenever g(x) = 0.

Remark 13. We will abuse notation slightly in this article by interchangeably using sets and formulas characterizing those sets. For example, we will use formulas in the arguments to In f and In -f (from Theorem 6). However, when describing sets we will use set-theoretic symbols ∪ and ∩ for set union and intersection, respectively, and will let S c denote the complement of S; when we are working with formulas, we will instead employ the corresponding logical symbols ∨ and ∧ for disjunction and conjunction, and ¬ for negation. The set R n (resp. ∅) will be syntactically represented by the symbol T (resp. F).

We thus have the inward set of g = 0 given by

In f (g = 0) = g = 0 ∩ g = 0 ∩ g = 0 ∩ g = 0 ∩ • • • ,
which is characterized by the following infinite "formula"5

" In f (g = 0) ≡ g = 0 ∧ g = 0 ∧ g = 0 ∧ g = 0 ∧ • • • " .
For sets of states satisfying inequalities {x ∈ R n | g(x) < 0}, which we also concisely denote by the formula g < 0, the situation is similar with the following infinite construction:

" In f (g < 0) ≡ g < 0 ∨ (g = 0 ∧ g < 0) ∨ (g = 0 ∧ g = 0 ∧ g < 0) ∨ (g = 0 ∧ g = 0 ∧ g = 0 ∧ g < 0) . . . " .
Intuitively, the first non-zero Lie derivative of g needs to be negative at a point x satisfying g(x) = 0 in order for the flow ϕ(t, x) to enter the set g < 0 from that point and remain within this set throughout some time interval (0, ), for some positive .

Remark 14. One may draw physical analogies here, e.g. to the motion of a vehicle: if the velocity is 0, then it is the sign of the acceleration term that determines whether the vehicle will move forward in the next time instant; if both the velocity and the acceleration are 0, it is the sign of the derivative of the acceleration (i.e. the sign of the jerk term), and so forth.

The decision procedure developed by [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF] rests on the fact that for a polynomial function p and a polynomial system of ODEs x = f (x), the formulas characterizing In f (p = 0) and In f (p < 0) are indeed finite. To see why this is true, note that whenever p and f 1 , f 2 , . . . , f n that make up f are polynomials, all the formal Lie derivatives p , p , • • • are also guaranteed to be polynomials. Let us now recall the ascending chain property of ideals in the polynomial ring R[x 1 , . . . , x n ] -a consequence of Hilbert's basis theorem and the fact that the ring R is Noetherian (Cox et al., 2015, Ch. 2, Thm. 7).

Lemma 15. Let p ∈ R[x 1 , . . . , x n ], then the ascending chain of ideals p ⊆ p, p ⊆ p, p , p ⊆ • • •
is finite, i.e. there exists a k ∈ N such that p, p , . . . , p (k) = p, p , . . . , p (K) for all K ≥ k.

For a given p, we denote the smallest k in the above lemma by ord f (p) and say that it defines the order of p with respect to the system of polynomial ODEs x = f (x). In practice, we can always compute ord f (p) by simply computing successive formal Lie derivatives of p and successively checking whether p (k+1) ∈ p, p , p , . . . , p (k) holds for k = 1, 2, 3, . . . , until the membership check succeeds, which would imply that the ideal chain has stabilized (the fact that this process terminates is guaranteed by Lemma 15). 6 The ideal membership check can be easily performed by reducing the polynomial p (k+1) by the Gröbner basis of {p, p , . . . , p (k) } for each successive k and checking whether the remainder is 0. An upper bound on the length of the ascending chain of ideals generated by successive Lie derivatives of p was obtained in (Novikov and Yakovenko, 1999, Thm. 4); this bound is doubly-exponential in the number of variables, however, in practice one typically observes the ideals stabilizing after only a few iterations.

As a direct consequence of Lemma 15, whenever p, p , . . . , p (ord f (p)) are all simultaneously 0, all higher derivatives must also evaluate to 0. More formally:

p = 0 ∧ p = 0 ∧ p = 0 ∧ • • • ∧ p (ord f (p)) = 0 → ∀ K > ord f (p). p (K) = 0 .
Using this fact one can construct perfectly legitimate formulas that provide a finite characterization of In f (p = 0) and In f (p < 0), given as follows:

In f (p = 0) ≡ p = 0 ∧ p = 0 ∧ p = 0 ∧ • • • ∧ p (ord f (p)) = 0 , In f (p < 0) ≡ p < 0 ∨ (p = 0 ∧ p < 0) ∨ (p = 0 ∧ p = 0 ∧ p < 0) . . . ∨ (p = 0 ∧ p = 0 ∧ p = 0 ∧ • • • ∧ p (ord f (p)) < 0) .
Notice that in the construction of In f (p < 0) the saturation of the chain of ideals guarantees that all further terms in the disjunction, i.e.

p = 0 ∧ p = 0 ∧ p = 0 ∧ • • • ∧ p (ord f (p)) = 0 ∧ • • • ∧ p (K) < 0
where K > ord f (p), are False and therefore unnecessary.

Improving the Construction of In

f (p = 0) and In f (p < 0)
One may work naïvely with ideals generated by the successive Lie derivatives p, p , p , . . . , p (k) and construct In f (p = 0) and In f (p < 0) using these derivatives directly (as above), following [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF]. However, this construction can be improved if one realizes that only the remainders of the Lie derivatives are needed for this construction, as will be shown in the following lemma. The practical advantage afforded by doing this is the degree of the remainder polynomials, which is typically lower than the degree of the Lie derivatives themselves.

Lemma 16. Given a polynomial p and a system of polynomial ODEs x = f (x), let rem 0 = p and let rem i+1 be defined inductively as the remainder obtained from polynomial reduction (i.e. multivariate polynomial division) of the Lie derivative rem i by the polynomials {rem 0 , rem 1 . . . , rem i }. Then for all i ≥ 0

rem i = p (i) - i-1 j=0 α ij p (j)
where α ij are polynomials.

Proof. By induction. Base case: rem 0 = p = p (0) . For an inductive hypothesis, assume that rem k = p (k) -k-1 j=0 α kj p (j) holds for all k ≤ n. Since rem n+1 is the remainder upon the reduction of rem n by {rem 0 , . . . , rem n }, we have rem n+1 = rem n -n i=0 β i rem i , where β 0 , . . . , β n are polynomials. From our inductive hypothesis and by applying the product rule for differentiation we have

rem n = p (n+1) -   n-1 j=0 α nj p (j)   = p (n+1) - n j=0 γ j p (j) , (1)
where γ 0 , . . . , γ n are polynomials, and

rem n+1 = rem n - n i=0 β i rem i [from the definition] =   p (n+1) - n j=0 γ j p (j)   - n i=0 β i rem i [from (1)] , =   p (n+1) - n j=0 γ j p (j)   - n i=0 β i p (i) - i-1 l=0 α il p (l) [by hypothesis] ,
from which it is apparent that rem n+1 has the required form:

rem n+1 = p (n+1) - n j=0 α n+1j p (j) .
Lemma 17. Let rem i be defined as in Lemma 16. Then the inward sets can be characterized as follows:

In f (p = 0) ≡ (rem 0 = 0 ∧ rem 1 = 0 ∧ rem 2 = 0 ∧ • • • ∧ rem ord f (p) = 0)
and

In f (p < 0) ≡ rem 0 < 0 ∨ (rem 0 = 0 ∧ rem 1 < 0) ∨ (rem 0 = 0 ∧ rem 1 = 0 ∧ rem 2 < 0) . . . ∨ (rem 0 = 0 ∧ rem 1 = 0 ∧ rem 2 = 0 ∧ • • • ∧ rem ord f (p) < 0) .
Proof. For In f (p = 0), we show by induction that

∀ n ≥ 0. n i=0 rem i = 0 = n i=0 p (i) = 0 .
Base case: rem 0 = p (0) = p by definition. For the inductive hypothesis, let us assume that

k i=0 rem i = 0 = k i=0 p (i) = 0
holds for some k ≥ 0. Then from the hypothesis we have that

k+1 i=0 rem i = 0 = k i=0 p (i) = 0 ∩ rem k+1 = 0 .
By Lemma 16 we have rem k+1 = p (k+1) -k j=0 α k+1j p (j) and hence k+1 i=0

rem i = 0 =   k i=0 p (i) = 0 ∩ p (k+1) - k j=0 α k+1j p (j) = 0   = k i=0 p (i) = 0 ∩ p (k+1) = 0 .
The proof for In f (p < 0) follows a similar inductive argument.

Remark 18. Using the remainders instead of the higher-order Lie derivatives of p for constructing In f (p = 0) and In f (p < 0) is pragmatically often a good choice. For a concrete example, consider the Van der Pol oscillator whose dynamics is given by x = y and y = -x -y(x 2 -1), and let p = x 2 + y 2 -1.

The ascending chain of ideals

rem 0 ⊆ rem 0 , rem 1 ⊆ rem 0 , rem 1 , rem 2 ⊆ • • •
stabilizes at rem 0 , . . . , rem 6 , which is x 2 +y 2 -1, 2y 4 , -8xy 3 , 24y 2 , -48xy, 48 .

In contrast, if one uses the actual higher-order Lie derivatives, the 6 generators of the ideal p, p , . . . , p (6) are too large to all fit on this page, with p (6) having total degree 12. We should however note that in certain cases it may be more expensive to compute the ideal rem 0 , rem 1 , . . . , rem ord f (p) than it is to compute p, p , . . . , p (ord f (p)) because the potential gain in lowering the total degree of the ideal generators can be outweighed by the computational overhead arising from the size of the coefficients of the intermediate polynomials. This is a well-known phenomenon when computing Gröbner bases (Cox et al., 2015, Ch. 2, p.116).

Distributive Properties of In f

Viewed as a set operator, In f distributes over set intersections. For any sets S 1 , S 2 ⊆ R n , one has:

In f (S 1 ∩ S 2 ) = In f (S 1 ) ∩ In f (S 2 ) .
The operator In f does not, however, distribute over set union; only the following set inclusion is guaranteed to hold in general:

In f (S 1 ∪ S 2 ) ⊇ In f (S 1 ) ∪ In f (S 2 ) .
Counterexample 19. To see why the converse inclusion does not hold, consider the simple 1-dimensional system x = 1 and the set

S = x ∈ R | x ≤ 0 ∨ x > 0 ∧ sin x -1 = 0 .
The point 0 ∈ R cannot be an element of In f (S) because ϕ(t, 0) = t and for any positive there exists a t ∈ (0, ) such that sin t -1 = 0 and therefore ϕ(t, 0) ∈ S. In other words, 0 belongs to In f (S) c . At the same time, 0 cannot be in In f (S c ) either because the flow cannot move from the point at x = 0 without crossing one root of sin t -1 = 0. Thus

In f (S ∪ S c ) = In f (R n ) = R n = In f (S) ∪ In f (S c ) .
The example also shows that in general

In f (S c ) is not equal to In f (S) c since 0 ∈ In f (S) c while 0 ∈ In f (S c ). 7
For semi-analytic sets the In f operator does distribute over set unions. In particular, for semi-algebraic sets (a special class of semi-analytic sets) given by

S = l i=1   mi j=1 p ij < 0 ∩ Mi j=mi+1 p ij = 0   ,
where p ij are polynomials, one has:

In f (S) = l i=1   mi j=1 In f (p ij < 0) ∩ Mi j=mi+1 In f (p ij = 0)   .
A proof of this property for semi-algebraic sets (Liu et al., 2011, Lemma 20) was generalized to semi-analytic sets in (Platzer and Tan, 2020, §6.1.2). These results in particular mean that, if one restricts attention to these classes of sets, the equality In f (S) c = In f (S c ) holds (making the equivalence of Theorem 6 and (Zhan et al., 2017, Thm. 9.1) immediate, contrary to the general setting where this equality does not hold and where Lemma 11 is required to prove the equivalence).

The LZZ Decision Procedure Based on Theorem 6

Given a quantifier-free formula describing a semi-algebraic set

S ≡ l i=1   mi j=1 p ij < 0 ∧ Mi j=mi+1 p ij = 0   ,
and a polynomial system of ODEs x = f (x), in order to decide whether S is a positively invariant set, a basic decision procedure using the characterizations based on inward sets (Theorem 6 and (Liu et al., 2011, Thm. 19)), which we term LZZ, after the authors in [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF], can be implemented by performing the following steps:

1. Compute In f (p ij ij 0), where ij ∈ {=, <} appearing in S (formulas p < 0 and p = 0, where p is a polynomial, will be referred to as atomic formulas), and from these construct

In f (S) ≡ l i=1   mi j=1 In f (p ij < 0) ∧ Mi j=mi+1 In f (p ij = 0)   ,
following the distributive property of In f for semi-algebraic sets S. 2. Construct In -f (S c ) following the same process as in step 1, but using the complement S c and the reversed system x = -f (x). 3. Check the semi-algebraic set inclusions S ⊆ In f (S) and S c ⊆ In -f (S c ) from Theorem 6 using e.g. the CAD algorithm of [START_REF] Collins | Partial cylindrical algebraic decomposition for quantifier elimination[END_REF].

Remark 20. One can alternatively construct In -f (S) in step 2 and check the inclusions S ⊆ In f (S) and S c ⊆ In -f (S) c in step 3, following the original method of [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF], rather than the characterization in Theorem 6.

A basic implementation of the LZZ decision procedure thus requires an algorithm for computing Gröbner bases (to compute the inward sets in step 1 and step 2) and a decision procedure for the universally (or existentially) quantified fragment of real arithmetic (to check the semi-algebraic set inclusions in step 3).

In practice, the syntactic description of S may feature atomic formulas that are not of the form p < 0 or p = 0, e.g. S may feature the comparison operators >, ≥, ≤, and may have atomic formulas where the term on the right-hand side of the comparison operator is not 0 as assumed above. To implement step 1 and step 2 for this more general case (without tampering with the description of S) it is convenient to compute In f (S) by syntactically replacing all atomic formulas p lhs p rhs (where p lhs and p rhs are polynomials and ∈ {<, ≤, =, =, ≥, >}) appearing in the syntactic description of S, with In f (p lhs p rhs ), which can be defined for atoms in terms of the primitives In f (p < 0) and In f (p = 0) in the following way (we use ':=' to denote function definitions):

In f (T) := T , In f (F) := F ,
= 0 ∧ rem 1 = 0 ∧ rem 2 = 0 ∧ • • • ∧ rem ord f (p) = 0) , In f (p < 0) := rem 0 < 0 ∨ (rem 0 = 0 ∧ rem 1 < 0) ∨ (rem 0 = 0 ∧ rem 1 = 0 ∧ rem 2 < 0) . . . ∨ (rem 0 = 0 ∧ rem 1 = 0 ∧ rem 2 = 0 ∧ • • • ∧ rem ord f (p) < 0) .
An implementation of the LZZ decision procedure in the Wolfram Language can be achieved with fewer than 35 lines of code following the above approach.8

Characterizing Positive Invariance Through Exit Sets

In this section we develop an alternative characterization of positively invariant sets using the concept of exit set as formulated by [START_REF] Conley | Isolated Invariant Sets and the Morse Index[END_REF].

Let s ∈ I x be a point in time within the maximal interval of existence of solution ϕ from initial value x, and let I ϕ(s,x) def = {t | t + s ∈ I x }, which is simply the time interval I x offset by s (or, equivalently, the maximal interval of existence from the initial value ϕ(s, x)). The mapping ϕ defines a local flow on the topological space R n since, for all x ∈ R n , ϕ(0, x) = x, and

∀ s ∈ I x . ∀ t ∈ I ϕ(s,x) . ϕ(t, ϕ(s, x)) = ϕ(s + t, x) .
Let S be a subset of R n . Recall that a point x ∈ R n is a closure point of S if and only if every open set containing x intersects S in at least one point (not necessarily distinct from x itself if x happens to be in S). Let S • denote the interior of S. The boundary of S, denoted ∂S, is defined as S \ S • . As before, we use t > 0 as a shorthand for t ∈ I x ∩ (0, +∞) and, similarly, by t < 0 we understand t ∈ I x ∩ (-∞, 0). Definition 21 (Exit Set [START_REF] Conley | Isolated Invariant Sets and the Morse Index[END_REF]). The exit set of S ⊆ R n with respect to the local flow induced by x = f (x) is defined as follows:

Exit f (S) def = {x ∈ S | ∀ t > 0. ∃ s ∈ (0, t). ϕ(s, x) ∈ S} .
The exit set of S defines the set of points in S from which the flow cannot evolve forward in time without leaving the set S. As the name suggests, a flow starting at a point in Exit f (S) "leaves the set S immediately" (regardless of where it was before). It is intuitive that such points can only lie on the boundary of S.

Lemma 22. The set Exit f (S) is a subset of ∂S (in addition to being a subset of S, by definition).

Proof. Let x ∈ Exit f (S) ∩ S • , then there exists an open set U ⊂ S • containing x. By continuity of ϕ(•, x) with respect to time, there exists a neighbourhood I of 0 in I x such that ϕ(t, x) ∈ U for all t ∈ I. Let t ∈ I ∩ (0, +∞). Since x ∈ Exit f (S), there exists s ∈ (0, t) ⊂ I such that ϕ(s, x) ∈ S and, a fortiori, ϕ(s, x) ∈ U , which contradicts the existence of I and thus Exit f (S) ∩ S • = ∅. Since Exit f (S) ⊆ S by definition, the exit set is a subset of ∂S.

Positive invariance of a set S (as given in Definition 1) may be equivalently defined using the set of so-called escape points (also due to [START_REF] Conley | Isolated Invariant Sets and the Morse Index[END_REF]

): 9 Escape f (S) def = {x ∈ S | ∃ t > 0. ϕ(t, x) ∈ S} .
(2)

Notice the difference between the exit and escape sets: starting at an exit point, the flow immediately exits the set S, whereas for an escape point the flow may first evolve within S before leaving S at some point in time in the future (i.e., it must eventually leave S). Thus, Exit f (S) ⊆ Escape f (S). The set of escape points of S is empty precisely when S is a positively invariant set. Furthermore, this criterion can be stated entirely in terms of exit sets. Theorem 23. A set S ⊆ R n is positively invariant if and only if both Exit f (S) and Exit -f (S c ) are empty.

Proof. For necessity, it is easy to see that the set is not positively invariant whenever the exit sets are not both empty. Case (i): if Exit f (S) is non-empty, then for some point x ∈ S there exists a t > 0 such that ϕ(t, x) ∈ S. Case (ii): if Exit -f (S c ) is non-empty, then for some y ∈ S there exists a τ > 0 such that ϕ(-τ, y) ∈ S. Taking z = ϕ(-τ, y), it is clear that z ∈ S and ϕ(τ, z) ∈ S.

For sufficiency we show that whenever S is not positively invariant, the sets Exit f (S) and Exit -f (S c ) cannot both be empty. Suppose (for contradiction) that both Exit f (S) and Exit -f (S c ) are empty and that S is not positively invariant. The set of escape points of S is therefore non-empty. Consider an escape point x ∈ Escape f (S): by our hypothesis x cannot be in the empty set of exit points Exit f (S). Therefore there exists a positive t 0 ∈ I x such that for all s ∈ (0, t 0 ) one has ϕ(s, x) ∈ S, and there exists a t 1 ∈ I x such that t 0 ≤ t 1 and ϕ(t 1 , x) ∈ S (i.e. ϕ(t 1 , x) ∈ S c ). Let us define

T = {t ∈ I x ∩ (0, +∞) | ∀s ∈ (0, t), ϕ(s, x) ∈ S} .
Under our hypothesis, the set T is non-empty and has a supremum t such that t 0 ≤ t ≤ t 1 . Let us now define

T = {t ∈ I x ∩ (0, +∞) | ϕ(t, x) ∈ S} .
This set is likewise non-empty (as it contains t 1 ) and has an infimum t such that t 0 ≤ t . Every element of T is an upper bound for T (otherwise there would exist a time t ∈ T at which both ϕ(t, x) ∈ S and ϕ(t, x) ∈ S). Clearly, since t is the least upper bound for T it can act as a lower bound on T and we therefore have t ≤ t , where t is the greatest lower bound for T . Suppose the inequality is strict (t < t ), then for all r ∈ [t , t ) one has ϕ(r, x) ∈ S (otherwise t is not the greatest lower bound for T ). But then t cannot be the least upper bound for T because ϕ(s, x) ∈ S for s ∈ (t , t ). Thus t = t and we have two cases to consider: either (i) ϕ(t , x) ∈ S, in which case ϕ(t , x) ∈ Exit f (S) and Exit f (S) is therefore non-empty, or (ii) ϕ(t , x) ∈ S, in which case ϕ(t , x) ∈ Exit -f (S c ), so Exit -f (S c ) is non-empty. Both cases give us a contradiction.

Remark 24. The main technical difference between the proof of Theorem 23 and (Zhan et al., 2017, Thm. 9.1) is that the latter draws a contradiction from considering the supremum of the set T (with respect to our notations in the proof of Theorem 23) whereas we draw a contradiction by considering in addition the set T . This is to be expected as the statements of these theorems are slightly different: Theorem 23 complements S then applies the Exit -f operator to S c , whereas (Zhan et al., 2017, Thm. 9.1) applies the In -f operator to S first then complements the result. This being said, the overall structure of both proofs is however very similar and this fact is better captured by appealing to the real induction principle as a generic proof technique as detailed in Section 3.

Remark 25. Readers with a background in dynamical systems may find it a little counterintuitive that one needs to consider the flow in the reversed system to characterize positive invariance. Indeed, for closed sets S it is well known that "local invariance" under the flow ϕ (viz. emptiness of Exit f (S)) is equivalent to positive invariance (e.g. see Cârjȃ et al., 2007, Ch. 4). It is important to remember that Theorem 23 makes no assumptions about the set S being open or closed. When S is open, local invariance holds trivially because the flow may always evolve within the set for some time from any x ∈ S.

Observe that the sets Exit f (S) and Exit -f (S) are not necessarily disjoint: for example, any isolated point which is not an equilibrium would lie in both sets. Neither are they required to cover the boundary ∂S: if S is an equilibrium point, then both Exit f (S) and Exit -f (S) are empty, whereas ∂S = S.

The operators Exit f and In f respectively capturing the main underlying concepts used in Theorems 6 and Theorem 23 are intimately related.

Lemma 26. For any set S ⊆ R n , Exit f (S) = In f (S) c ∩ S. Equivalently, one has Exit f (S) c ∩ S = In f (S) ∩ S.
Proof. One has x ∈ In f (S) c ∩ S if and only if x ∈ S, and, for any positive t ∈ I x , there exists s ∈ (0, t) such that ϕ(s, x) ∈ S, otherwise ϕ(s, x) ∈ S holds for all s ∈ (0, t) which would mean that x ∈ In f (S). The latter is exactly the definition of Exit f (S).

A symmetric equality holds (only) for closed sets.

Lemma 27. For a closed set S ⊆ R n , In f (S) = Exit f (S) c ∩ S.
Proof. If S is a closed set, then the inclusion In f (S) ⊆ S holds trivially, from Lemma 26 we have Exit f (S) c ∩ S = In f (S) ∩ S and the result follows.

Remark 28. According to the above lemmas, while In f (S) is sufficient to fully recover Exit f (S) by simple set operations. The converse is not true for general sets: the bare knowledge of Exit f (S) is not enough to completely recover In f (S) unless S is closed. This might seem as a conceptual defect favouring inward sets as more fundamental than exit sets. From a computational standpoint, however, this lack of symmetry between the two concepts turns out to be powerful: intuitively one does not need the full information encoded by inward sets to decide the positive invariance of S. Exit sets, despite carrying less information, are sufficient for this purpose.

Using Lemma 26, both characterizations of positively invariant sets in Theorem 6 and Theorem 23 can be recovered from one another using the following equivalences:

∅ = In f (S) c ∩ S Exit f (S) ⇐⇒ S ⊆ In f (S) , ∅ = In -f (S c ) c ∩ S c Exit -f (S c ) ⇐⇒ S c ⊆ In -f (S c ) .
The origins of exit sets in Theorem 23 lie in topology and it is the properties of exit sets that make this characterization computationally interesting. The astute reader may remark at this point that Theorem 23 admits a shorter proof using real induction via Lemma 26. This is indeed the case; however, such a proof would not rely on the concept of exit set nor would it expose the topological insights that we wish to call upon later. As we shall see, exit sets afford a very different way of looking at the problem of checking positive invariance and their properties can be exploited to give a substantially different algorithmic solution than that offered by LZZ in Section 3.4.

Properties of Exit Sets

Let S 1 , S 2 ⊆ R n , we discuss below the distributive properties of Exit f over set intersection and union.

Lemma 29. Exit f (S 1 ∩ S 2 ) = (Exit f (S 1 ) ∩ S 2 ) ∪ (S 1 ∩ Exit f (S 2 )).

Proof. The inclusion Exit

f (S 1 ∩ S 2 ) ⊇ (Exit f (S 1 ) ∩ S 2 ) ∪ (Exit f (S 2 ) ∩ S 1 ) is immediate: if x ∈ Exit f (S 1 ) ∩ S 2 ,
then, for all positive t, there exists a positive s < t such that ϕ(s, x) ∈ S 1 and therefore ϕ(s, x) ∈ S 1 ∩ S 2 . Likewise for Exit f (S 1 ∩ S 2 ) ⊇ Exit f (S 2 ) ∩ S 1 . To prove the converse, let x ∈ Exit f (S 1 ∩ S 2 ), then x ∈ S 1 ∩ S 2 and for all positive t, there exists a positive s < t such that ϕ(s, x) ∈ S 1 ∩ S 2 which is equivalent to ϕ(s, x) ∈ S 1 or ϕ(s, x) ∈ S 2 .

Lemma 30. Exit f (S 1 ∪ S 2 ) ⊆ Exit f (S 1 ) ∩ In f (S 2 ) c ∪ In f (S 1 ) c ∩ Exit f (S 2 ) . Proof. Let x ∈ Exit f (S 1 ∪ S 2
), then by definition, for all t > 0, there exists s ∈ (0, t) such that ϕ(s, x) ∈ S 1 ∪ S 2 , which is equivalent to ϕ(s, x) ∈ S 1 and ϕ(s, x) ∈ S 2 . By hypothesis, x ∈ S 1 ∪ S 2 . If x ∈ S 1 then it has to belong to Exit f (S 1 ) as well as In f (S 2 ) c , by definition of the latter. If x ∈ S 2 , we get a symmetric formula by swapping S 1 and S 2 , namely x ∈ Exit f (S 2 ) ∩ In f (S 1 ) c . The desired formula is the union of these two cases.

Counterexample 31. The reverse inclusion of Lemma 30 does not hold in general. Consider the simple 1-dimensional system x = 1 and the sets

S 1 = {0} ∪ x ∈ R | x > 0 ∧ sin x -1 = 0 , S 2 = {0} ∪ x ∈ R | x > 0 ∧ sin x -1 = 0 .
The point 0 belongs to both Exit f (S 1 ) and Exit f (S 2 ). In addition, it does not belong to either In f (S 1 ) or In f (S 2 ). However, 0 is not in Exit f (S 1 ∪ S 2 ) as the union (x ≥ 0) is clearly a positively invariant set for the considered flow.

This simple example highlights the main reason why the inclusion in Lemma 30 cannot in general be replaced with set equality. If x ∈ Exit f (S 1 ) ∩ In f (S 2 ) c , one can only conclude that for any positive 1 , 2 , there exist t 1 ∈ (0, 1 ) and t 2 ∈ (0, 2 ) such that ϕ(t 1 , x) ∈ S 1 and ϕ(t 2 , x) ∈ S 2 ; there is nothing to suggest that t 1 should be equal to t 2 , which is required for x to belong to Exit f (S 1 ∪S 2 ). However, if one restricts attention to semi-analytic sets S (which includes semialgebraic sets) then In f (S c ) = In f (S) c (as observed in the previous section), and the inclusion of Lemma 30 becomes an equality. (Notice that semi-analyticity is only sufficient to ensure that In f (S c ) = In f (S) c . We currently lack a full characterization of the most general topological settings that respect this equality.) Lemma 32. Let S 1 , S 2 be semi-analytic sets. Then

Exit f (S 1 ∪ S 2 ) = Exit f (S 1 ) ∩ In f (S 2 ) c ∪ In f (S 1 ) c ∩ Exit f (S 2 ) . Proof. Exit f (S 1 ∪ S 2 ) = In f (S 1 ∪ S 2 ) c ∩ (S 1 ∪ S 2 ) = (In f (S 1 ) c ∩ In f (S 2 ) c ∩ S 1 ) ∪ (In f (S 1 ) c ∩ In f (S 2 ) c ∩ S 2 ) = Exit f (S 1 ) ∩ In f (S 2 ) c ∪ Exit f (S 2 ) ∩ In f (S 1 ) c .

The ESE Decision Procedure Based on Theorem 23

Given a quantifier-free formula describing a semi-algebraic set S and a polynomial system of ODEs x = f (x), Theorem 23 can be used to algorithmically decide whether S is positively invariant or not with respect to f .

A naïve approach would be to first compute E = Exit f (S) ∪ Exit -f (S c ) recursively on the Boolean structures of S and S c using Lemmas 30 and 32, then check whether E is empty or not. Such an approach would be very similar to the LZZ procedure described in section 3.4 and would therefore suffer from the same problem, namely the impossibility of the current state-of-the-art quantifier elimination algorithms to check the emptiness of E in reasonable time, even for seemingly simple planar systems (cf. section 5). Indeed, one experimentally observes that, for many interesting examples, the construction of the set E is not computationally expensive despite requiring several ideal membership tests as, often, the order (with respect to f ) of the polynomials involved remains low. An overwhelming share of the running time for a typical problem is spent on proving emptiness of E (as is the case for checking the inclusions S ⊆ In f (S) and S c ⊆ In -f (S c ) using LZZ).

We will see in this section how the concept of exit sets, and more precisely Theorem 23, can be used to overcome this bottleneck in a principled way. The main idea is to "chop the set E into smaller pieces" (chunks) on which the emptiness test can be performed in a divide-and-conquer fashion, instead of constructing a formula characterizing E first and only then checking for its emptiness. What is perhaps more interesting is that Theorem 23 suggests a natural way of splitting E into chunks in such a way that each chunk involves precisely one exit set of an atomic formula. This, in turn, allows one to exploit topological properties of atomic formulas, such as openness, in order to check for set emptiness syntactically, obviating the need for expensive computations such as real quantifier elimination.

As in the previous sections, we use the same notation for semi-algebraic sets and their formal representations as quantifier-free formulas of real arithmetic. Without loss of generality, we also restrict our attention to the atomic formulas, p < 0 and p = 0, where p is a polynomial. The formulas p ≤ 0 and p = 0, are syntactic sugar for (p < 0 ∨ p = 0) and (-p < 0 ∨ p < 0) respectively. Similarly, p > 0, p ≥ 0 can be encoded as -p < 0, -p ≤ 0 respectively.

The exit sets of F, T, and p < 0 are all empty (by Lemma 22) as the sets defined by these formulas are open. According to the same lemma, the exit set of p = 0 necessarily lies on its boundary, which is also given by p = 0. When the first Lie derivative of p does not vanish on p = 0, the flow necessarily leaves the set for some positive time. The same reasoning applies for higher-order Lie derivatives. As with the construction of In f in Section 3.4, the construction of the exit set of p = 0 is fully captured by a (finite) formula:

Exit f (p = 0) ≡ p = 0 ∧ p = 0 ∨ p = 0 ∧ p = 0 ∧ p = 0 . . . ∨ p = 0 ∧ p = 0 ∧ p = 0 ∧ • • • ∧ p (ord f (p)) = 0 .
Note that Lemma 16 also applies to Exit f (p = 0) and the remainders rem i (as defined in the lemma) can be used instead of the Lie derivatives p (i) . In summary, the exit set of atomic formulas can be constructed using a procedure

The procedure Reduce checks for emptiness of the semi-algebraic set by performing real quantifier elimination (this functionality is offered e.g. by implementations of CAD [START_REF] Collins | Partial cylindrical algebraic decomposition for quantifier elimination[END_REF]; however, there exist alternatives which are not based on CAD, e.g. RAGLib (Safey El Din, 2017)).

In a nutshell, the main purpose of NonEmpty f is to recursively check for emptiness of exit sets, as stated more formally in the following lemma.

Lemma 33. Let S and R be two formulas describing semi-algebraic sets. Then NonEmpty f (S, R) returns False if and only if Exit f (S) ∩ R is empty.

Proof. The proof is by induction on the depth of formula S. Base case: if

S ∈ {F, T, p < 0, p = 0}, then NonEmpty f (S, R) is Reduce (∃x 1 . . . . ∃x n . Exit f (S) ∧ R) ,
which is False if and only if Exit f (S) ∩ R is empty (we freely interchange ∧ and ∩ as well as the empty set and False as mentioned in Remark 13).

For the inductive hypothesis, suppose the property holds for all formulas of depth less than or equal to k and let S 1 , S 2 , and S be such formulas.

If

S = S 1 ∧ S 2 , then by definition NonEmpty f (S 1 ∧ S 2 , R) is False if and only if both NonEmpty f (S 1 , S 2 ∧ R) and NonEmpty f (S 2 , S 1 ∧ R) are False.
By the induction hypothesis, this means that both Exit f (S 1 ) ∧ (S 2 ∧ R) and Exit f (S 2 ) ∧ (S 1 ∧ R) are empty, and therefore their union is also empty. One gets the desired result by factoring out R then using Lemma 29:

∅ = (Exit f (S 1 ) ∩ (S 2 ∩ R)) ∪ (Exit f (S 2 ) ∩ (S 1 ∩ R)) = ((Exit f (S 1 ) ∩ S 2 ) ∪ (Exit f (S 2 ) ∩ S 1 )) ∩ R = Exit f (S 1 ∩ S 2 ) ∩ R .
The disjunctive case can be proved similarly using Lemma 32.

Finally, if S = ¬S , NonEmpty f (S, R) = NonEmpty f (Neg(S ), R) and one may eliminate all negations from Neg(S ) by applying De Morgan's laws and double negation elimination and finally applying Neg to any remaining negated atoms. Since the property holds for atomic formulas, conjunctions and disjunctions, it holds for S as well.

The procedure NonEmpty f can thus be used to check positive invariance as an immediate corollary of Theorem 23 and Lemma 33 by setting R to T. Theorem 34. A semi-algebraic set S is positively invariant for a system of ODEs x = f (x) if and only if ¬ NonEmpty f (S, T) ∨ NonEmpty -f (¬S, T) .

Accordingly, we define the Exit Set Emptiness (ESE) decision procedure that checks for positive invariance of S with respect to f as

ESE(S, f ) := ¬ NonEmpty f (S, T) ∨ NonEmpty -f (¬S, T) .

Complexity Analysis

For given formulas S and R, in order to check the emptiness of Exit f (S) ∩ R, the procedure NonEmpty f (S, R) performs several calls to Reduce in order to eliminate existential quantifiers. The number of such calls depends only on the Boolean structure of S, in particular, the second argument R plays no role in the way the procedure operates. In this section, we first give upper and lower bounds of the number of such calls as a measure of the impact of the encoding of S. We then discuss further decompositions of Exit f (S) as a union of basic semi-algebraic sets. Recall that a basic semi-algebraic set is a set described by a conjunction of atomic formulas i (p i i 0), where i ∈ {<, =} and p i are polynomials.

Proposition 35. Suppose the set S is characterized by a formula in disjunctive normal form (DNF)

R rs ≡ mr j=1,j =s A rj ∧ ¬In f   k i=1,i =r mi j=1 A ij   .
Proof. The form of the real quantifier elimination (QE) problems is immediate from the definition of NonEmpty f . The equivalence of R rs is obtained by using the distributive properties (over disjunctions and conjunctions) of the In f operator.

For instance, suppose S ≡ (A 11 ∧ A 12 ) ∨ A 21 ∨ A 31 (k = 3, m = m 1 = 2, m 2 = m 3 = 1). Then, in the worst case, the procedure NonEmpty f (S, T) has to call Reduce 4 times:

Reduce ∃x 1 . . . ∃x n . Exit f (A 11 ) ∧ A 12 ∧ ¬In f (A 21 ∨ A 31 ) , Reduce ∃x 1 . . . ∃x n . Exit f (A 12 ) ∧ A 11 ∧ ¬In f (A 21 ∨ A 31 ) , Reduce ∃x 1 . . . ∃x n . Exit f (A 21 ) ∧ ¬In f ((A 11 ∧ A 12 ) ∨ A 31 ) , Reduce ∃x 1 . . . ∃x n . Exit f (A 31 ) ∧ ¬In f ((A 11 ∧ A 12 ) ∨ A 21 ) .
R rs ≡ ¬In f   mr j=1,j =s A rj   ∧ k i=1,i =r mi j=1 A ij . For instance, suppose S ≡ (A 11 ∨ A 12 ) ∧ A 21 ∧ A 31 , (k = 3, m = m 1 = 2, m 2 = m 3 = 1).
Then, in the worst case, the procedure NonEmpty f (S, T) has to call Reduce 4 times:

Reduce ∃x 1 . . . ∃x n . Exit f (A 11 ) ∧ ¬In f (A 12 ) ∧ (A 21 ∧ A 31 ) , Reduce ∃x 1 . . . ∃x n . Exit f (A 12 ) ∧ ¬In f (A 11 ) ∧ (A 21 ∧ A 31 ) , Reduce ∃x 1 . . . ∃x n . Exit f (A 21 ) ∧ ((A 11 ∧ A 12 ) ∨ A 31 ) , Reduce ∃x 1 . . . ∃x n . Exit f (A 31 ) ∧ ((A 11 ∧ A 12 ) ∨ A 21 ) .
Remark 37. Suppose S ≡ k i=1 mi j=1 A ij and let S denote the same formal expression as S except that ∨ and ∧ are swapped. Then the QE problems that NonEmpty f (S , T) has to solve could be obtained syntactically from those of NonEmpty f (S, T) by swapping A ij and ¬In f (A ij ) (and leaving Exit f (A ij ) untouched).

The encoding of the set S to be checked may have a significant impact on the number of calls to Reduce in NonEmpty f (S, T). For instance, suppose S is encoded as

S 1 ≡ (A 1 ∨ (A 2 ∧ A 3 )) ∧ (A 4 ∨ (A 2 ∧ A 3 ))
where the A i are atomic formulas. Then NonEmpty f (S 1 , T) calls Reduce 6 times. In this case, none of the upper bounds of Propositions 35 nor 36 apply because S 1 is neither in DNF nor in CNF. If one uses the equivalent (DNF) encoding S 2 ≡ (A 1 ∧A 4 )∨(A 2 ∧A 3 ) for S, then NonEmpty f (S 2 , T) calls Reduce only 4 times at most. Lemma 38. The number of calls to Reduce is bounded below by the number of distinct atomic formulas in S (regardless of the encoding of S).

Proof. The procedure NonEmpty f requires one call to Reduce for each problem of the form Exit f (A) ∧ R (where A is an atomic formula), and R any arbitrary formula. Depending on the encoding of S, NonEmpty f might call Reduce once for Exit f (A)∧(R 1 ∨R 2 ), or twice for Exit f (A)∧R 1 and Exit f (A)∧R 2 separately. In the best case, the encoding of S is such that each call to Reduce features a distinct Exit f (A) (otherwise, the several calls with the same Exit f (A) can be factored out), and the result follows.

An interesting open question is whether there exists a systematic way of finding an encoding of S which always results in the minimal number of calls to Reduce that is possible. We leave this question open while observing that one can build simple examples for which neither the DNF nor the CNF encoding of S are adequate in this regard (it suffices to consider encodings with redundant atomic formulas).

The QE problems to solve in Proposition 35 can be split further (by distributivity) into

k i=1,i =r m i ≤ m k-1 "smaller" problems of the form Reduce ∃x 1 . . . ∃x n . Exit f (A rs ) ∧ mr j=1,j =s A rj ∧ k i=1,i =r ¬In f (A i i ) .
Likewise, the QE problems to solve in propositions 36 can be split further into

k i=1,i =r m i ≤ m k-1 problems of the form Reduce ∃x 1 . . . ∃x n . Exit f (A rs ) ∧ mr j=1,j =s ¬In f (A rj ) ∧ k i=1,i =r A i i .
We could further evaluate Exit f and In f for atomic formulas. To do so, one has to account for the system of ODEs x = f (x) as well as the order of the involved polynomials with respect to f . Let deg(p) denote the (total) degree of a polynomial p, and deg(f ) the maximum degree of the polynomials appearing in the right-hand side of x = f (x). Recall that the degree of p , the first (Lie) derivative of p with respect to f , has a total degree which is at most deg(p) + (deg(f ) -1), and the degree of p (s) is at most deg(p) + s(deg(f ) -1). Recall that ord f (p) denotes the order of p with respect to f . The set Exit f (p 0) is the union of ord f (p) basic semi-algebraic sets, whereas In f (p 0) is the union of ord f (p) + 1 basic semi-algebraic sets. Lemma 39. Let p i , 1 ≤ i ≤ m, and q j , 1 ≤ j ≤ k, denote some polynomials and let ρ denote the maximum of their respective order with respect to f . The expression

Exit f (p 1 1 0) ∧ m i=2 (p i i 0) ∧ k j=1
In f q j j 0 is the union of at most ρ(ρ + 1) k basic semi-algebraic sets. Each basic semialgebraic set is a conjunction of at most m -1 + (k + 1)(ρ + 1) expressions of the form p 0.

Proof. The expression is a union of at most ord f (p 1 ) k j=1 (ord f (q j ) + 1) basic semi-algebraic sets. From which one immediately deduces the ρ(ρ + 1) k upper bound. Each basic semi-algebraic set is a conjunction of at most (ord f (p 1 ) + 1) + (m -1) + k j=1 (ord f (q j ) + 1) ≤ m + k + (k + 1)ρ literals. For instance, Exit f (p 1 = 0) ∧ (p 2 < 0) ∧ In f (q < 0) where ord f (p 1 ) = ord f (q) = 2, (thus m = 2, k = 1, and ρ = 2) is the following union

p 1 = 0 ∧ p 1 = 0 ∧ p 2 < 0 ∧ q < 0 ∨ p 1 = 0 ∧ p 1 = 0 ∧ p 2 < 0 ∧ q = 0 ∧ q < 0 ∨ p 1 = 0 ∧ p 1 = 0 ∧ p 2 < 0 ∧ q = 0 ∧ q = 0 ∧ q < 0 ∨ p 1 = 0 ∧ p 1 = 0 ∧ p 1 = 0 ∧ p 2 < 0 ∧ q < 0 ∨ p 1 = 0 ∧ p 1 = 0 ∧ p 1 = 0 ∧ p 2 < 0 ∧ q = 0 ∧ q < 0 ∨ p 1 = 0 ∧ p 1 = 0 ∧ p 1 = 0 ∧ p 2 < 0 ∧ q = 0 ∧ q = 0 ∧ q < 0 .
(p rj rj 0) ∧ k i=1,i =r ¬In f (p i i i i 0) or Exit -f ¬(p rs rs 0) ∧ mr j=1,j =s In -f (p rj rj 0) ∧ k i=1,i =r ¬(p i i i i 0)
reduces to False syntactically, and the total number of basic semi-algebraic sets is therefore km k . Now, according to Lemma 39, each of the above expressions is the union of at most ρ(ρ + 1) k-1 basic semi-algebraic sets (after evaluating In f and Exit f for atomic formulas). Thus Exit f (S) ∨ Exit -f (¬S) is the union of at most km k ρ(ρ + 1) k-1 basic semi-algebraic sets, as stated. The bounds on the total number of the involved polynomials as well as their degrees are direct consequences of Lemma 39 and of the bound on the total degree of high-order Lie derivatives, namely d + ρ(deg(f ) -1).

The main conclusion from the analysis performed in this section is the following: instead of solving one large real quantifier elimination problem which results from a naïve application of Theorems 6 and 23 (coarse granularity), it is instead possible to solve exponentially many (precisely km k ρ(ρ + 1) k-1 ) smaller real quantifier elimination problems as in Theorem 40; these smaller problems furthermore only involve basic semi-algebraic sets (fine granularity).

In theory, there exist decision procedures for deciding universally (or existentially) quantified sentences of real arithmetic that have singly exponential worst case complexity (sd) O(n) , where s is the number of polynomials, d their maximum degree and n the number of variables [START_REF] Grigor'ev | Complexity of deciding Tarski algebra[END_REF]. Each of the smaller QE problems features fewer polynomials with a lower maximum degree than the original QE problem. The potential gain in complexity is however mitigated by the number of these small problems, which is exponential as stated in Theorem 40.

The procedure ESE, as defined in Section 4.2, seeks a trade-off between the fine and coarse granularities which translates into a trade-off between the computational cost of QE problems versus the number of QE problems to solve. Combined with the syntactic reductions to False of Exit f (A) whenever A is an atomic formula encoding an open set, the concept of exit sets provides a powerful tool from a computational standpoint -in addition to its ability to characterize positively invariant sets in full generality as stated in Theorem 23.

The next section provides some examples that are out of reach for LZZ (see Section 3.4) and where ESE (see Section 4.2) succeeds in deciding set positive invariance. Notice that, although one can divide the QE problem in LZZ into basic semi-algebraic sets, such an approach will not benefit from the syntactic reductions to False offered by Exit f (without paying an extra computational overhead to detect such cases).

Experiments

For checking positive invariance of sets described by a single atomic formula (e.g. p < 0), there is no discernible difference in performance between the LZZ and ESE procedures. However, there is a very palpable difference between the two procedures when checking positive invariance of sets described by more interesting formulas with non-trivial Boolean structure. The examples below serve to illustrate this difference.

Example 41. Consider the non-linear system x = -x 3 , y = -y 3 + x. To construct a semi-algebraic set with non-trivial Boolean structure, let us consider the sequence of points obtained from a rational parametrization of the unit circle x 2 + y 2 = 1, e.g. a sequence of points (x t , y t ) = ( 2t t 2 +1 , -1-t 2 t 2 +1 ) ∈ Q 2 . From the arithmetic sequence of rational numbers t 0 = -2, t n+1 = t n + 1 8 with t in the range [-2, 2], we can construct a sequence of half-planes that include the unit disc centred at the origin and are tangent to the unit circle at the points (x t , y t ). The intersection of these half-planes results in a droplet-like shape shown in Fig. 1a and is characterized by a formula S which is a conjunction of 36 linear inequalities.

By inspecting the phase portrait of the system in Fig. 1a, the set defined by this formula appears to be positively invariant, which is something we should be able to check using the procedures described in the previous sections. Checking positive invariance of S using our implementation of ESE returns False within 0.3 seconds.10 Indeed, while it is difficult to see from inspecting Fig. 1a, a closer examination (Fig. 1b) reveals that the set characterized by S is not positively invariant because the flow does in fact leave the droplet region. On the other hand, no answer to this positive invariance question could be obtained using LZZ within reasonable time (> 4 hours). Example 42. Now let us consider the system x = -x 3 , y = -y 3 and the set corresponding to the tilted Maltese cross in Figure 2a, which, unlike the previous example, is not described by a purely conjunctive formula, but is instead given by a disjunction of 4 formulas describing the arms of the cross (each arm is described by a formula of the form p

1 ≤ 0 ∧ p 2 ≤ 0 ∧ (p 3 ≤ 0 ∨ p 4 ≤ 0),
where each p i=1,2,3,4 is linear). For this example, one can verify that the set is indeed a positive invariant using ESE, which returns True within 164 seconds. Once more, no answer could be obtained using LZZ within reasonable time (> 4 hours).

- The set shown in Figure 2a is semi-linear because its formal description only features polynomials of maximum degree 1. Figure 2b illustrates a semialgebraic set which is not semi-linear, featuring quadratic polynomials in its formal description; the vector field shown in Figure 2b corresponds to x = -x 3 -y, y = -y 3 + x. Using ESE we are able to check (within 7 seconds) that the set is indeed positively invariant under the flow of the system, whereas LZZ produces the same answer in over 30 minutes.

3 -2 -1 0 1 2 3 -3 -2 -1 0 1 2 3 x y (a) Semi-linear invariant -3 -2 -1 0 1 2 3 -3 -2 -1 0 1 2 3 x y (b) Semi-algebraic invariant

Positive Invariants Under Constraints

In addition to the standard notion of set positive invariance (as given in Definition 1), more general notions have been considered. For example continuous invariance, as it is known in the formal verification literature (see e.g. [START_REF] Platzer | Computing differential invariants of hybrid systems as fixedpoints[END_REF][START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF], extends positive invariance to accommodate cases in which there is a constraint (given by some Q ⊆ R n ) imposed on the evolution of the system.

Definition 43 (Continuous invariant). A set S ⊆ R n is a continuous invariant under evolution constraint Q ⊆ R n if and only if the following holds:

∀ x ∈ S. ∀ t ≥ 0. (∀ τ ∈ [0, t]. ϕ(τ, x) ∈ Q) → ϕ(t, x) ∈ S .
Essentially, in a continuous invariant positive invariance is predicated on the constraint Q being maintained. Thus, positive invariance may be regarded as a special case of continuous invariance as defined above, i.e. the special case where the constraint Q is all of R n .

Remark 44. Readers familiar with temporal logics such as LTL may think of continuous invariance as (very loosely speaking) being in a certain sense analogous to temporal modal operators such as Weak Until (W), i.e. one may think of a continuous invariant described by formula S subject to evolution constraint described by Q as satisfying the temporal logic formula S W ¬Q. Of course, the semantics of such a formula needs to be defined over the trajectories of the continuous system rather than discrete traces, e.g. as is done in Signal Temporal Logic (STL, see [START_REF] Maler | Monitoring temporal properties of continuous signals[END_REF].

The work of [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF] was developed in this slightly more general setting of continuous invariance, rather than positive invariance. A semi-algebraic set S subject to a semi-algebraic evolution constraint Q is a continuous invariant of the system x = f (x) if and only if (Liu et al., 2011, Thm. 19

): S ∩ Q ∩ In f (Q) ⊆ In f (S) and S c ∩ Q ∩ In -f (Q) ⊆ In -f (S) c .
The ESE algorithm introduced in this article is likewise easily lifted to check continuous invariance.

Theorem 45. A semi-algebraic set S is a continuous invariant for a system of ODEs x = f (x) subject to a semi-algebraic evolution constraint Q if and only

if ¬ NonEmpty f (S, Q \ Exit f (Q)) ∨ NonEmpty -f (¬S, Q \ Exit -f (Q)) .
The main difference with respect to Theorem 34, is that instead of considering the entire space R n for both forward and backward flows, we focus on Q \ Exit f (Q)) (which is equivalent to Q ∩ In f (Q) by Lemma 26) for the forward flow and Q \ Exit -f (Q) (or equivalently Q ∩ In -f (Q)) for the backward flow. These formulations make explicit the fact that the states from which the flow exits Q (formally captured by Exit f (Q)) are not relevant for checking continuous invariance and are thus removed from Q. Said differently, by construction, the set Exit f (Q) (resp. Exit -f (Q)) is considered a positive (resp. negative) invariant set relative to Q.

Discrete Abstractions of Continuous Systems

Problems involving positive invariance checking under evolution constraints (i.e. continuous invariance in the sense of Definition 43) arise frequently in the area of formal verification. Invariants described using formulas with non-trivial Boolean structure are particularly important to verification methods based on discrete abstractions of continuous dynamical systems [START_REF] Sogokon | A method for invariant generation for polynomial continuous systems[END_REF]. Briefly, discrete abstraction involves partitioning the state space (e.g. R n ) into disjoint sets that correspond to equivalence classes representing states in a discrete transition system. For example, such a partitioning can be obtained from an algebraic decomposition of R n using a finite set of polynomials {p 1 , . . . , p k }. Each cell of this decomposition is described by a conjunction of sign conditions on these polynomials, e.g. the formula S ≡ p 1 > 0 ∧ p 2 = 0 ∧ • • • ∧ p k < 0 describes a cell (which is a basic semi-algebraic set corresponding to a single discrete state in the abstraction). Discrete abstractions of continuous systems are obtained by constructing a discrete transition relation between the discrete states. An abstraction is said to be sound if the absence of a discrete transition from the state described by S i to another state described by S j in the transition relation implies that the continuous system cannot evolve from any state within the set S i to any state within S j without leaving the union S i ∪ S j ; an abstraction is said to be exact if the presence of such a transition implies the existence of a trajectory which starts at a state within S i and reaches some state in S j without leaving the union S i ∪ S j in the process. In order to construct the transition relation for a sound and exact discrete abstraction one considers the union of neighbouring cells S i and S j in the algebraic decomposition and checks whether the set described by S j is a continuous invariant subject to the constraint S i ∨ S j . There can be no transition from cell S i to S j in the discrete transition relation if and only if S j is continuous invariant under constraint S i ∨ S j in the sense of Definition 43. Naturally, the Boolean structure of the formulas involved make the construction of discrete abstractions a potentially fruitful area of application for the ESE algorithm.

Related Work

The method of applying the ascending chain condition to ideals generated by successive Lie derivatives of polynomials in order to prove invariance of algebraic varieties in polynomial vector fields was employed by [START_REF] Novikov | Trajectories of polynomial vector fields and ascending chains of polynomial ideals[END_REF], [START_REF] Ghorbal | Characterizing algebraic invariants by differential radical invariants[END_REF], and more recently by [START_REF] Harms | Polynomial control systems: invariant sets given by algebraic equations/inequations[END_REF]. [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF] were the first to address positive invariance of semi-algebraic sets using techniques described in Section 3 of this article. [START_REF] Dowek | Preliminary investigations on induction over real numbers[END_REF] investigated the use of real induction to solve kinematic problems involving ODEs.

Platzer and Tan (2020) recently developed a system of formal axioms (one of which formalizes the real induction principle) for reasoning about continuous invariants in differential dynamic logic. This axiomatization is complete in the sense that a formal proof of continuous invariance of a semi-analytic set represented by a formula S can be derived in differential dynamic logic from the axioms whenever this invariance property holds, and a refutation can be derived whenever it does not.

Among characterizations of positive set invariance in a less general setting than that considered in this article, we note the work of [START_REF] Castelan | On invariant polyhedra of continuous-time linear systems[END_REF], who reported necessary and sufficient conditions for positive invariance of convex polyhedra in linear vector fields.

Conclusion

This article describes two alternative characterizations of positively invariant sets for systems of ODEs with unique solutions.

The first characterization, along with its associated LZZ decision procedure for checking positive invariance of semi-algebraic sets in poylnomial vector fields, is closely related to the work by [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF]. While the relationship between the work of [START_REF] Liu | Computing semi-algebraic invariants for polynomial dynamical systems[END_REF] and the principle of real induction has been known informally to a number of researchers, this important link has not been adequately elaborated in existing literature. One of our aims in writing this article has been to make this relationship more widely appreciated and also to create an accessible account of the original LZZ decision procedure, along with our own improvements to this method (Section 3.2) and nuances in its practical implementation informed by our experience (Section 3.4).

The second part of the article contributes an alternative characterization of set positive invariance and is based on the notion of exit sets [START_REF] Conley | Isolated Invariant Sets and the Morse Index[END_REF]. The topological origins of this notion afford certain computational vistas that suggest a very different approach to developing a decision procedure for checking positive invariance than that of LZZ. The ESE procedure developed in Section 4.2 is, to the authors' knowledge, entirely novel. Its main advantage over LZZ lies in its efficient handling of formulas with non-trivial Boolean structure (a class of problems where the LZZ procedure generally performs poorly). The complexity analysis undertaken in Section 4.3 sheds some light on the computational advantages of using ESE, which is empirically confirmed in a number of examples in Section 5.

Important topics not touched upon in this article include robustness of positively invariant sets under small perturbations of the system dynamics; indeed, in practical applications, the system of ODEs is often only known approximately and invariants that are not robust are in a certain sense unphysical. In the future we hope to build upon the present work to address these considerations.

  reveals the following inclusion In f (S c ) ⊆ In f (S) c for any set S. Whenever S is a closed set (S c is open), we therefore have that S c ⊆ In f (S c ) ⊆ In f (S) c or, if we prefer, In f (S) ⊆ S.

  In f (p lhs = p rhs ) := In f (p lhs -p rhs = 0) , In f (p lhs < p rhs ) := In f (p lhs -p rhs < 0) , In f (p lhs > p rhs ) := In f (p rhs -p lhs < 0) , and, using the fact that In f (S c ) = In f (S) c for semi-algebraic sets S, In f (p lhs = p rhs ) := ¬ In f (p lhs -p rhs = 0) , In f (p lhs ≤ p rhs ) := ¬ In f (p rhs -p lhs < 0) , In f (p lhs ≥ p rhs ) := ¬ In f (p lhs -p rhs < 0) . The primitives In f (p = 0) and In f (p < 0) are defined following Lemma 17 as In f (p = 0) := (rem 0

  ij , where A ij are atomic formulas. Let m = max i m i . Then the recursion depth of NonEmpty f (S, T) is bounded by k + m and the number of calls to Reduce is k i=1 m i ≤ km, each of which has the form Reduce ∃x 1 . . . ∃x n .Exit f (A rs ) ∧ R rs , where

Proposition 36 .

 36 Suppose the set S is characterized by a formula in conjunctive normal form (CNF) k i=1 mi j=1 A ij where A ij are atomic formulas, and let m = max i m i . Then the recursion depth of NonEmpty f (S, T) is bounded by k + m and the number of calls to Reduce is k i=1 m i ≤ km, each of which has the form Reduce ∃x 1 . . . ∃x n .Exit f (A rs ) ∧ R rs , where

Theorem 40 .

 40 Let S be a semi-algebraic set encoded either as ij ij 0) (CNF) for some polynomials p ij . Letm = max i m i , d = max i,j deg(p ij ), and ρ = max i,j ord f (p ij ). Then Exit f (S) ∨ Exit -f (¬S) is a union of at most km k ρ(ρ + 1) k-1 basic semi-algebraic sets q 1 1 0 ∧ . . . ∧ q s s 0 , where s ≤ m -1 + k(ρ + 1) and deg(q j ) ≤ d + ρ(deg(f ) -1). Proof. Suppose S ≡k i=1 mi j=1 (p ij ij 0) (the same reasoning applies when S is in CNF). Thus ¬S ≡ k i=1 mi j=1 ¬(p ij ij 0). According to Propositions 35 and 36, Exit f (S) is a union of at most km k basic semi-algebraic sets, each involving Exit f (p ij ij 0), whereas Exit -f (¬S) is the union of at most km k basic semi-algebraic sets, each involving Exit -f ¬(p ij ij 0). If p ij ij 0 encodes a closed set, then its negation encodes an open set (and vice versa). Thus at least one of the expressions Exit f (p rs rs 0) ∧ mr j=1,j =s

Figure 1 :

 1 Figure 1: Checking positive invariance

Figure 2 :

 2 Figure 2: Positive invariants

The set inclusions required in(Zhan et al., 2017, Thm. 9.1) can be alternatively phrased as In -f (S) ⊆ S ⊆ In f (S).

The idea of using real induction to prove(Zhan et al., 2017, Thm. 9.1) was first suggested by Paul B. Jackson and Kousha Etessami (School of Informatics, University of Edinburgh) in private communication with the second author.

Technically, a formula can only be finite, hence the quotes for such hypothetical objects.

Using terminology from differential algebra[START_REF] Ritt | Differential Algebra[END_REF] one may say that the ideal p, p , . . . , p (ord f (p)) defines a differential ideal.

Recall from Remark 5 that In f (S c ) ⊆ In f (S) c holds for any set S. The above counterexample demonstrates that the converse inclusion does not hold generally.

Our implementation is available from[START_REF]Implementation and examples (requires Wolfram Mathematica[END_REF]

The set of escape points is fundamental to the Ważewski principle. See[START_REF] Conley | Isolated Invariant Sets and the Morse Index[END_REF] where it is denoted as W • for a set W .

Using Mathematica 12.0, running on a machine with an Intel Core i5-7300U CPU clocked at 2.6GHz with 16GB of RAM.

Acknowledgement. The authors are indebted to Dr Paul B. Jackson and Dr Kousha Etessami at the University of Edinburgh for their insights into the real induction principle underpinning the work of Liu, Zhan and Zhao, and extend special thanks to Yong Kiam Tan at Carnegie Mellon University for suggesting improvements to the writing in an early draft of this work (and for bringing the authors' attention to the article (Clark, 2019) of which they were previously unaware); his formal development of an invariant checking procedure in differential dynamic logic appeared in (Platzer and Tan, 2018) and (Platzer and Tan, 2020). The authors would also very much like to thank the anonymous reviewers for their careful reading and valuable suggestions for improving the article.

Exit f which is defined as follows:

Thus, the only non-trivial exit set for atomic formulas is the exit set of an equality as it is the only (atomic) closed set.

We next define a recursive procedure called NonEmpty f , parametrized by the vector field f , and which takes as its arguments two quantifier-free real arithmetic formulas describing semi-algebraic sets S and R. It is defined as follows (A denotes an atomic formula):

NonEmpty f (¬S, R) := NonEmpty f (Neg(S), R) .

In addition to Exit f , NonEmpty f relies on three other procedures: In f (already defined in Section 3.4), Neg, and Reduce. The procedure Neg applies negation ¬ to the formula it receives as its argument (but does not recursively apply negation to the sub-formulas). For atomic formulas, Neg simply negates the formula, expressing the result in terms of only the basic forms of atomic formulas (T, F, p < 0, and p = 0):