A Method for Invariant Generation for Polynomial Continuous Systems

Abstract

This paper presents a method for generating semi-algebraic invariants for systems governed by non-linear polynomial ordinary differential equations under semi-algebraic evolution constraints. Based on the notion of discrete abstraction, our method eliminates unsoundness and unnecessary coarseness found in existing approaches for computing abstractions for non-linear continuous systems and is able to construct invariants with intricate boolean structure, in contrast to invariants typically generated using template-based methods. In order to tackle the state explosion problem associated with discrete abstraction, we present invariant generation algorithms that exploit sound proof rules for safety verification, such as differential cut (${\text {DC}}$), and a new proof rule that we call differential divide-and-conquer (${\text {DDC}}$), which splits the verification problem into smaller sub-problems. The resulting invariant generation method is observed to be much more scalable and efficient than the naïve approach, exhibiting orders of magnitude performance improvement on many of the problems.

This material is based upon work supported by the UK Engineering and Physical Sciences Research Council (EPSRC) under grants EP/I010335/1 and EP/J001058/1, the National Science Foundation by NSF CAREER Award CNS-1054246, NSF EXPEDITION CNS-0926181, CNS-0931985 and DARPA FA8750-12-2-0291.

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

1 Introduction

Establishing safe operation of embedded systems arising in modern engineering increasingly involves reasoning about the behaviour of hybrid dynamical systems that combine discrete and continuous state evolution. Continuous dynamics is typically specified by ordinary differential equations (ODEs). Non-linear ODEs afford the engineer the means of modelling rich dynamic behaviour that cannot possibly occur in linear systems [12], but are also notoriously difficult to analyse because they rarely possess solutions that can be expressed in closed form.

This paper is concerned with the problem of automating safety verification for continuous systems modelled by non-linear ODEs under evolution constraints, which is a problem of broader interest to automating safety verification for hybrid dynamical systems. To solve the verification problem, one requires a proof that a given continuous system does not evolve into an unsafe state at any future time from some given initial configuration while obeying its evolution constraint. Additionally, given that solutions are rarely available, it is highly desirable to arrive at such a proof by working with the ODEs directly, i.e. without solving the initial value problem.

Traditionally, two popular techniques have been used for proving safety properties without computing solutions or putting a finite bound on the duration of evolution in continuous systems: one based on first soundly abstracting the continuous system and performing reachability analysis in the resulting discrete transition system, and a deductive verification approach that works by reasoning about appropriate invariants in the continuous system.

Deductive verification tools for hybrid systems crucially rely on (i) the ability to prove invariance assertions about continuous systems (which was solved for the case of semi-algebraic¹ invariants and polynomial ODEs in [14]) and (ii) having the means of automatically generating continuous invariants sufficient to prove safety assertions about continuous systems. In practice, this latter point is often the main bottleneck when verifying safety of hybrid systems in which the continuous dynamics are non-linear.

Existing automatic procedures for generating invariants for use in deductive frameworks only make limited use of the boolean structure in invariants. Approaches based on abstraction, in computing reachable sets of discrete systems, (implicitly) create invariants with more intricate boolean structure; their limitations currently stem from the conservative nature of the discrete models, whose transition behaviour is often a very coarse over-approximation of the evolution taking place in the continuous system.

A number of approaches have been proposed for generating invariants for continuous systems [8, 11, 14, 16, 24, 27, 28, 38, 44], which either put serious restrictions on the form of the invariant or rely on the user pre-defining a template and then attempt to find an instantiation of the parameters in the template that yields an invariant. In this paper we pursue an alternative approach that automatically generates semi-algebraic continuous invariants from discrete semi-algebraic abstractions of continuous systems. Our rationale is that recent advances in semi-algebraic invariant checking for polynomial ODEs [14] allow deductive provers to work with arbitrary semi-algebraic invariants, yet few methods for invariant generation are able to synthesize interesting invariants with boolean structure that one might find in reachable sets of discrete abstractions. At the same time, discrete abstraction approaches do not take full advantage of the results on invariant checking in constructing the transition relation for the discrete transition system. We seek to address both of these issues.

Currently available methods for creating semi-algebraic abstractions of non-linear polynomial systems [36, 37] result in abstractions that are unsound for certain degenerate cases and unnecessarily coarse even in very simple scenarios. Additionally, discrete abstraction is known to scale poorly owing to (in the worst case) an exponential increase in the number of discrete states as the continuous state space is partitioned [37], making it very difficult to refine abstractions. To ameliorate this situation, we give a method for constructing semi-algebraic abstractions that are sound and only as coarse as the partitioning of the continuous state space into discrete regions itself. We then employ ideas from deductive verification to give more scalable and efficient algorithms for generating semi-algebraic invariants for polynomial continuous systems.

Contributions. In Sect. 3 of this paper we (I) introduce a method for constructing semi-algebraic abstractions of polynomial continuous systems in which transitions between the discrete states occur if and only if a corresponding continuous evolution is possible in the continuous system. In Sect. 4 we give an algorithm for generating semi-algebraic invariants for polynomial continuous systems by efficiently extracting reachable sets from these abstractions. In Sect. 5 we (II) introduce a sound proof rule ${\text {DDC}}$ (differential divide-and-conquer) which works to split the safety verification problem into smaller sub-problems by exploiting properties of invariant real algebraic sets and (III) give more scalable invariant generation algorithms employing sound proof rules differential weakening (${\text {DW}}$) [19] and differential cut (${\text {DC}}$) [19, 21] together with the new rule ${\text {DDC}}$ to address the discrete state explosion problem associated with computing abstractions. In Sect. 6 we (IV) evaluate our techniques on a collection of 100 safety verification problems featuring predominantly non-linear ODEs.

2 Preliminaries

To simplify our presentation, we will use the notation for sets and formulas characterizing those sets interchangeably in this paper, e.g. H will denote both a semi-algebraic set $H \subseteq \mathbb {R}^n$ and a formula H in the first-order theory of real arithmetic with free variables in $x_1,\dots ,x_n$ that characterizes this set. In what follows, we shall restrict our attention to autonomous² systems of polynomial ordinary differential equations under semi-algebraic evolution domain constraints³, i.e. systems of the form:

$$ \dot{x}_i = f_i(\mathbf {x}), \quad \mathbf {x} \in H \subseteq \mathbb {R}^n, $$

where $f_i \in \mathbb {R}[x_1,\dots ,x_n]$ for $1 \le i \le n$ and the evolution domain constraint H is semi-algebraic. We will write this concisely using vector notation as $\dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H$.

One may wonder at this stage whether restricting attention to polynomial systems represents a severe limitation; after all, non-linearities involving transcendental functions such as $\sin , \cos , e, \ln$, etc., are not uncommon in systems of practical interest. Fortunately, it is often possible to transform such systems into (larger) polynomial systems by introducing fresh variables and eliminating non-polynomial non-linearities in a rather general technique [23], which is known in various scientific communities as recasting [17, 30] or differential axiomatization [19]. Furthermore, it has been shown that such a transformation can be mechanised for a broad class of non-polynomial systems using a terminating algorithm [15]. Likewise, no generality is lost by only considering autonomous systems because any system with explicit time dependence $\dot{\mathbf {x}} = f(\mathbf {x}, t) \ \& \ H$ can be transformed into an autonomous system by introducing a fresh variable to model time evolution, e.g. if we add $\dot{x}_{n+1} = 1$ to the system and replace every instance of t in the system with $x_{n+1}$.

To state the safety verification problem for continuous systems in full generality we require a set of initial states for the system, which we denote by $\psi \subseteq \mathbb {R}^n$, and a set of safe states denoted $\phi \subseteq \mathbb {R}^n$. The problem is to prove that starting inside $\psi$, the system $\dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H$ cannot leave $\phi$ by evolving inside the evolution domain constraint H. We will only consider semi-algebraic $\psi$ and $\phi$ in this paper and will state the safety property formally, using notation from differential dynamic logic ($\mathrm {d}\mathcal {L}$) [18], as follows:

$$ \begin{aligned} \psi \rightarrow [ \dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H ] \ \phi . \end{aligned}$$

The above formula asserts that, starting in any state satisfying the pre-condition ($\psi$), the system will necessarily (box modality $[\ ]$) satisfy the post-condition ($\phi$) when following the system $\dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H$ for any amount of time.⁴ The semantic definition of the $\mathrm {d}\mathcal {L}$ assertion above is given in terms of the solution, which precisely describes how continuous states evolve over time. A solution to the initial value problem for the system $\dot{\mathbf {x}} = f(\mathbf {x})$ with initial value $\mathbf {x}_0 \in \mathbb {R}^n$ is a differentiable function $\varphi _t(\mathbf {x}_0) : (a,b) \rightarrow \mathbb {R}^n$ defined for t in some non-empty interval of existence $(a,b) \subseteq \mathbb {R} \cup \{ \infty , -\infty \}$ including zero and such that $\frac{d}{dt}\varphi _t(\mathbf {x}_0) = f(\varphi _t(\mathbf {x}_0))$ for all $t \in (a,b)$. Formally, the $\mathrm {d}\mathcal {L}$ continuous safety assertion above is valid if the following is true:

$$\begin{aligned} \forall ~\mathbf {x}_0 \in \psi . \ \forall ~\tau \ge 0.~(\forall ~t \in [0, \tau ]~.\varphi _t(\mathbf {x}_0) \in H) \rightarrow \varphi _\tau (\mathbf {x}_0) \in \phi . \end{aligned}$$

In practice, solutions to non-linear ODEs are almost never available in closed form (by which we understand a finite expression in terms of polynomials and elementary functions); even when they are, the resulting sentences often belong to an undecidable theory [26] due to transcendental functions in the closed form expression. Alternatively, the safety verification problem can sometimes be solved directly in a deductive framework. This involves finding an appropriate set $I \subseteq \mathbb {R}^n$, called a continuous invariant [22], that satisfies the three premises (above the bar) of the following rule of inference:

$$ ( Safety )\ \frac{ H \wedge \psi \rightarrow I \quad I \rightarrow [ \dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H ] \, I \quad I \rightarrow \phi }{\psi \rightarrow [ \dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H ] \, \phi } $$

to conclude (below the bar) that the system is safe. Continuous invariants generalize positively invariant sets [6] to systems under evolution constraints.

Definition 1

(Continuous Invariant [22]). For a continuous system $\dot{\mathbf {x}} = f(\mathbf {x})\ \& \ H$, a set $I \subseteq \mathbb {R}^n$ is a continuous invariant if and only if

$$\begin{aligned} \forall ~\mathbf {x}_0 \in I. \ \forall ~\tau \ge 0.~(\forall ~t \in [0,\tau ].~&\varphi _t(\mathbf {x}_0) \in H) \rightarrow \varphi _t(\mathbf {x}_0) \in I. \end{aligned}$$

Intuitively, a continuous invariant is any set of states I such that any motion initialized inside I that respects the evolution constraint H is guaranteed to remain inside I.

When H and I are semi-algebraic and $f_i$ are polynomial, a decision procedure for checking whether I is a continuous invariant was reported in [14], enabling us to decide $\mathrm {d}\mathcal {L}$ assertions of the form $I \rightarrow [ \dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H ] \ I$. The decision procedure involves computing higher-order Lie derivatives and exploits the ascending chain property of Noetherian rings. The interested reader is invited to consult [14] for a detailed description of the procedure and also [8], where similar ideas were employed. As a direct consequence, every premise of the rule $( Safety )$ is known to be decidable, since $\psi$, $\phi$ and H are also assumed to be semi-algebraic, the goals $H \wedge \psi \rightarrow I$ and $I \rightarrow \phi$ can be passed to a decision procedure for real arithmetic [35]. The challenge in applying the rule now lies in finding an appropriate continuous invariant I.

3 Discrete Abstraction of Continuous Systems

In a certain sense, with discrete abstraction one seeks to approximate continuous systems by finite discrete transition systems. Such a transformation makes it possible to perform reachability analysis and verify safety properties in the simpler discrete model. The approach works by ensuring that the set of behaviours of the discrete (abstract) system over-approximates the set of behaviours of the continuous (concrete) system; this is known as sound abstraction. If the discrete abstraction is sound, then any violation of the safety property in the continuous system is necessarily reproduced by the abstract discrete transition system. Conversely, an abstraction is complete (with respect to the safety property) when any violation of the safety property in the abstraction is reproduced by the concrete continuous system.

Discrete abstraction of continuous systems was previously studied in [2, 3] (for linear systems) and [36, 37] (for more general non-linear systems), where a simple method for constructing abstractions was proposed but results in discrete systems that may feature transitions between discrete states that are impossible in the continuous system. In this section we describe the process of constructing sound and exact abstractions of non-linear continuous systems. That is, the resulting abstraction will feature a discrete transition between two abstract states if and only if a corresponding continuous trajectory is possible in the concrete system. The method we use is fundamentally different from [36, 37] in computing the discrete transition relation using a decision procedure for continuous invariant assertions [14].

3.1 Constructing the Discrete State Space

In this section we describe a way of partitioning the evolution domain constraint H in the continuous system $\dot{\mathbf {x}}= f(\mathbf {x}) \ \& \ H$ using a set of polynomial functions.

Definition 2

(Semi-algebraic Decomposition). A semi-algebraic decomposition of a semi-algebraic set $H \subseteq \mathbb {R}^n$ by a set of m polynomials $A \subset \mathbb {R}[x_1, \dots , x_n]$ is a partition of H into $k \le 3^m$ regions giving all the non-empty intersections of the form $H \cap p_1 \sim _1 0 \cap \cdots \cap p_m \sim _m 0$ where $p_i \in A$ and $\sim _i \in \{<,=,>\}$ for $1 \le i \le m$.

Computing the semi-algebraic decomposition of the evolution domain constraint H for a finite set of polynomials A can be achieved using a simple procedure that we will call $SemiAlgDecomp$. The decomposition defines a partition of H into k non-empty regions, each corresponding to a single discrete state, which we denote by $\mathbf {s}_i$, where $1 \le i \le k$. We will denote by S the set of all discrete states obtained from the semi-algebraic decomposition, i.e. $S \equiv \{ \mathbf {s}_i \mid 1 \le i \le k \}$.

3.2 Constructing the Transition Relation

We now apply the decision procedure for semi-algebraic continuous invariant assertion checking reported in [14] to exactly determine the transition relation $T \subset S \times S$, enabling us to construct exact discrete abstractions, which we denote by the pair (S, T). We will write $\mathbf {s}_i \longrightarrow \mathbf {s}_j$ for $(\mathbf {s}_i,\mathbf {s}_j) \in S \times S$, the discrete transition from state $\mathbf {s}_i$ to $\mathbf {s}_j$.

We begin with a transition relation $S \times S$ in which every state is reachable from every other state (including itself) in a single discrete transition. First, let us observe that a continuous solution of the differential equation cannot pass from a discrete state where $p>0$ (for some polynomial $p \in A$) to a state where $p<0$ without passing through $p=0$ first, nor vice versa. Using this intuition, we can give a general definition of what it means for two discrete states to be neighbouring (or adjacent [34]).

Definition 3

Let S be the set of discrete states constructed from a semi-algebraic decomposition of H by a finite set of polynomials $A \subset \mathbb {R}[x_1, \dots , x_n]$. Two discrete states $\mathbf {s}_i, \mathbf {s}_j \in S$, where $i \ne j$, are neighbouring if there are no points $\mathbf {x}_1,\mathbf {x}_2 \in \mathbf {s}_i \cup \mathbf {s}_j$ such that $p(\mathbf {x}_1)<0$ and $p(\mathbf {x}_2)>0$ for any p in A.

We can now construct a neighbouring transition relation $T_n \subseteq S \times S$ in which only the neighbouring states are reachable in a single transition (note that a state cannot be its own neighbour using our definition). Intuitively, in the neighbouring transition relation one cannot “jump across” $p=0$ in a single discrete transition; at the same time, any state is reachable from any other state. An abstraction which results from $(S,T_n)$ is still maximally coarse and therefore not very useful (illustrated in Fig. 1).

Fig. 1.

Semi-algebraic decomposition of $\mathbb {R}^2$ by $A=\{p_1,p_2\}$ resulting in 9 discrete states $S \subset 2^{\mathbb {R}^2}$ and the neighbouring transition relation $T_n \subset S \times S$.

We are only interested in retaining those discrete transitions for which the corresponding continuous transitions are possible in the original continuous system. In order to eliminate impossible discrete transitions we need to decide an invariance assertion:

$$ \begin{aligned} \mathbf {s}_i \rightarrow [ \dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ (\mathbf {s}_i \vee \mathbf {s}_j) ] \; \mathbf {s}_i , \end{aligned}$$

for each pair of neighbouring discrete states $(\mathbf {s}_i, \mathbf {s}_j) \in T_n$; we will proceed to remove transitions $\mathbf {s}_i \longrightarrow \mathbf {s}_j$ from $T_n$ if and only if the decision procedure for continuous invariance assertions returns $\mathrm {True}$. This process can be mechanized in a terminating abstraction algorithm that we call $ExactAbstraction$. The result is a discrete transition system (S, T) with a transition relation $T \subseteq T_n$ that does not feature discrete transitions that are impossible; we will state this property formally.

Proposition 4

Abstractions (S, T) are exact with respect to the discretization, i.e. $\mathbf {s}_i \longrightarrow \mathbf {s}_j$ is in T if and only if

$$\begin{aligned} \exists \ \mathbf {x}_0 \in \mathbf {s}_i. \ \exists \ \tau >0&. \ \varphi _{0}(\mathbf {x}_0) \in \mathbf {s}_i \ \wedge \ \varphi _{\tau }(\mathbf {x}_0) \in \mathbf {s}_j \quad \text {and} \quad \forall \ t \in [0,\tau ].\ \varphi _t(\mathbf {x}_0) \in \mathbf {s}_i \cup \mathbf {s}_j, \end{aligned}$$

that is, if and only if the system may evolve continuously from state $\mathbf {s}_i$ into a neighbouring state $\mathbf {s}_j$ without leaving their union $\mathbf {s}_i \cup \mathbf {s}_j$. The abstraction is exactly as coarse as the partition of the evolution constraint H into regions corresponding to discrete states.

One can view the process of removing impossible discrete transitions as a sound refinement of the neighbouring transition relation to $T \subseteq T_n$. In the worst case, using a set of m polynomials for the semi-algebraic decomposition of H will result in $3^m$ discrete states and a neighbouring transition relation $T_n$ with a total of $7^m - 3^m$ discrete transitions that need to be checked. In practice, both the number of discrete states and the number of transitions in $T_n$ will typically be much lower than the pessimistic worst case bound. Furthermore, removing impossible transitions from $T_n$ is a massively parallel problem, allowing one to exploit multi-core parallelism instead of iterating through the transitions sequentially.

3.3 Sound and Exact Abstraction

We will now discuss some important differences between earlier work and our approach. The discrete abstraction method reported in [37] is fundamentally different in the way it constructs the transition relation (let us call it $T_\sim \subseteq S \times S$), which is described in [37, Sect. 3.2.2]. In essence, the method imposes conditions for removing transitions from the neighbouring transition relation $T_n$ in the following way: given two neighbouring states $\mathbf {s}_i$ and $\mathbf {s}_j$, it removes the transition $\mathbf {s}_i \longrightarrow \mathbf {s}_j$ from $T_n$ if any of the following conditions are satisfied for any $p \in A$:

• 1. $\mathbf {s}_i$ has $p<0$ and $\mathbf {s}_j$ has $p=0$ and $\mathbf {s}_i \rightarrow \frac{d p}{dt} \le 0$ is true,

• 2. $\mathbf {s}_i$ has $p>0$ and $\mathbf {s}_j$ has $p=0$ and $\mathbf {s}_i \rightarrow \frac{d p}{dt} \ge 0$ is true,

• 3. $\mathbf {s}_i$ has $p=0$ and $\mathbf {s}_j$ has $p<0$ and ($\mathbf {s}_i \rightarrow \frac{d p}{dt} = 0 \vee \mathbf {s}_i \rightarrow \frac{d p}{dt} > 0$) is true,

• 4. $\mathbf {s}_i$ has $p=0$ and $\mathbf {s}_j$ has $p>0$ and ($\mathbf {s}_i \rightarrow \frac{d p}{dt} = 0 \vee \mathbf {s}_i \rightarrow \frac{d p}{dt} < 0$) is true.

Remark 5

The abstraction method in [37] also considers so-called stuttering (also self-looping [34]) transitions $\mathbf {s}_i \longrightarrow \mathbf {s}_i$, which we disregard here (already in the way we define $T_n$). This discrepancy makes no practical difference to safety verification as stuttering transitions have no effect on the reachable sets of discrete abstractions.

The approach described in [37] is not (in general) sound when the polynomials in A are allowed to be non-linear. To see this, consider the simple system with constant derivatives $\dot{x}_1 = 1, \dot{x}_2=0$ and let $A= \{ x_1^2+x_2, x_2-x_1^2 \}$. The abstraction one obtains (Fig. 2) suggests that the state $x_1^2+x_2=0 \wedge x_2-x_1^2 =0$ (equivalent to $x_1=0 \wedge x_2=0$) is invariant under the flow of the system, which is incorrect. The nature of this problem was studied in non-convex analysis; a solution would require reasoning about the contingent cone [42], which is not in general computable. A sound and exact abstraction using our approach is shown in Fig. 3.

Fig. 2.

Abstraction $(S, T_\sim )$ generated using method from [37].

Fig. 3.

Sound abstraction (S, T) generated by $ExactAbstraction$.

The abstraction method in [37] additionally suffers from coarseness, because it can introduce discrete transitions that correspond to evolutions that are impossible in the concrete continuous system (the abstraction is therefore inexact). For instance, consider a planar system of non-linear ordinary differential equations featuring a stable limit cycle in the form of a unit circle enclosing an equilibrium at the origin:

$$\begin{aligned} \dot{x}_1 =-x_1^3-x_2^2 x_1+x_1+x_2, \\ \dot{x}_2 = -x_2^3-x_1^2 x_2+x_2-x_1. \end{aligned}$$

Fig. 4.

Inexact abstraction $(S, T_\sim )$ generated using method from [37].

Fig. 5.

Exact abstraction (S, T) generated by $ExactAbstraction$.

Let the system evolve under no evolution constraints and consider a simple discretization by the axes polynomials, i.e. take $A= \{ x_1, x_2 \}$. The discrete abstraction $(S, T_\sim )$ generated using the method from [37] is shown in Fig. 4. An exact abstraction (S, T) without impossible transitions generated using our approach is shown in Fig. 5. Abstraction $(S, T_\sim )$ considers the origin reachable, while (S, T) does not.

4 Extracting Continuous Invariants from Discrete Abstractions

If one constructs a (sound) discrete abstraction of some system $\dot{\mathbf {x}}= f(\mathbf {x}) \ \& \ H$ using some finite set of polynomials A, one may verify safety properties by showing that they hold in the abstraction. For this, one needs to check whether an unsafe abstract state (i.e. one which contains a state that satisfies the formula $\lnot \phi$) is reachable by following the discrete transitions starting from the set of initial abstract states (those defining regions where $\psi$ is satisfiable). If none of the unsafe abstract states are reachable from the initial states in the abstraction, one can conclude that the continuous system is safe.

By computing the forward-reachable set from the set of the initial states $\psi$ in the abstraction, which we denote by $Reach _A^{\rightarrow }(\psi ,H) \subseteq H$, one generates a continuous invariant. Provided the abstraction is exact, this is the smallest continuous invariant with respect to the discretization by the polynomials in A and is furthermore semi-algebraic. Formally, we define

where $\longrightarrow ^*$ represents the reachability relation; that is, $\mathbf {s}_i \longrightarrow ^* \mathbf {s}_j$ if state $\mathbf {s}_j$ is reachable from $\mathbf {s}_i$ in zero or more discrete transitions in the exact abstraction (S, T), obtained from the discretization by polynomials in A. Thus, $I \equiv Reach _A^{\rightarrow }(\psi ,H)$ is a semi-algebraic set that is (by construction) guaranteed to include the initial set (i.e. $\psi \rightarrow I$) and is a continuous invariant for the system (i.e. $I \rightarrow [ \dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H]~I$). If it is also true that I does not include any unsafe states (i.e. $I \rightarrow \phi$), then I is sufficient to conclude that the system is safe using the proof rule $( Safety )$ from Sect. 2.

For invariant generation we are merely interested in extracting a semi-algebraic continuous invariant containing the initial set of states $\psi$ from the abstraction, not the full abstraction (S, T) itself. We now give a simple worklist procedure that we call $LazyReach$ (Algorithm 1) for constructing the set $Reach _{A}^{\rightarrow }(\psi ,H)$ lazily (on demand), i.e. without eagerly constructing the exact abstraction (S, T) first.

Although the worst-case running time of $LazyReach$ is exponential in $m=|A|$, in practice employing Algorithm 1 is often far more efficient than computing the exact abstraction (S, T) in full and then extracting $Reach _{A}^{\rightarrow }(\psi , H)$.

5 Tackling Discrete State Explosion

Discrete abstractions of continuous systems suffer from the discrete state explosion problem, i.e. the number of discrete states in the abstraction grows exponentially with the number of polynomials $m=|A|$ used for the discretization.

If one is to consider each individual polynomial $p \in A$, it is intuitive that if one can show that

• 1. for the initial set of states $\psi$, the polynomial p is sign-invariant, i.e. $p(\psi ) \sim 0$ where $\sim \in \{ <, =, > \}$, and

• 2. that this sign condition defines a continuous invariant for the system, i.e. $p \sim 0 \rightarrow [ \dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H]\ p \sim 0\ ,$

then one can refine the evolution constraint to $H \wedge p \sim 0$ and remove the polynomial p from A and obtain an abstraction by the polynomials $B \equiv A \setminus \{ p \}$ which has the property that

$$ Reach _{B}^{\rightarrow }(\psi ,H \wedge p\sim 0) \equiv Reach _{A}^{\rightarrow }(\psi ,H). $$

The number of discrete states generated using B for the semi-algebraic decomposition of $H \wedge p \sim 0$ is at most $3^{m-1}$ and the process can be repeated for other polynomials that remain in B. This section will explore approaches to tackling the discrete state space explosion based on this observation without making the abstraction unnecessarily coarse. For this purpose we will use sound proof rules differential cut and differential divide-and-conquer.

5.1 Differential Cut

Platzer and Clarke [22] explored an approach to safety verification based on iteratively refining the evolution constraint H with differential invariants (a subset of continuous invariants, see [19]). Such a sound refinement of the evolution domain is possible using an inference rule called differential cut [21] (henceforth DC). Differential cuts are used repeatedly in a process called differential saturation (see [22, Proposition 2]). The DC rule formalizes the idea that it is always sound to restrict the evolution domain H by some continuous invariant F, provided that it includes the initial set $\psi$, i.e.

$$ ({\text {DC}})\frac{\psi \rightarrow [\dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H] F \quad \psi \rightarrow [\dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H \wedge F] \, \phi }{ \psi \rightarrow [ \dot{\mathbf {x}} = f(\mathbf {x}) \ \& \ H]\ \phi } $$

the original rationale being that it is easier to prove the safety property in the more restricted system in the right premise.

5.2 Differential Divide-and-Conquer

We now introduce a new proof rule, akin to ${\text {DC}}$, that goes further and exploits a property of sets that are continuous invariants in both positive and negative time directions to split the continuous system into smaller continuous sub-systems between which there is no continuous evolution.

Proposition 6

The proof rule ${\text {DDC}}$ given below (with five premises) is sound.

$$ ({\text {DDC}}) \frac{\begin{array}{c} p=0 \rightarrow [\dot{\mathbf {x}}=f(\mathbf {x})~ \& ~H]\, p=0 \\ p=0 \rightarrow [\dot{\mathbf {x}}=-f(\mathbf {x})~ \& ~H]\, p=0 \\ \\ \psi \wedge p > 0\rightarrow [\dot{\mathbf {x}}=f(\mathbf {x}) \ \& \ H \wedge p > 0]\ \phi \\ \psi \wedge p = 0\rightarrow [\dot{\mathbf {x}}=f(\mathbf {x}) \ \& \ H \wedge p = 0]\ \phi \\ \psi \wedge p < 0\rightarrow [\dot{\mathbf {x}}=f(\mathbf {x}) \ \& \ H \wedge p < 0]\ \phi \end{array} }{\psi \rightarrow [\dot{\mathbf {x}}=f(\mathbf {x}) \ \& \ H]\ \phi } $$

Proof

For a continuous function p, no continuous trajectory inside H can cross from a region where $p>0$ to a region where $p<0$ without first crossing $p=0$. If the first two premises hold, then $p=0$ cannot be left inside H in either positive or negative time, i.e. there are no solutions entering or leaving $p=0$ inside H. The reachable sets of the system initialized in $\psi \wedge p > 0$, $\psi \wedge p = 0$ and $\psi \wedge p < 0$ are thus disjoint and confined to regions of H where $p>0$, $p=0$ and $p<0$ respectively. The union of these sets constitutes the reachable set of the system initialized in $\psi$ and the result follows.    $\square$

Informally, the rule allows one to split the original system into three dynamically disconnected regions, that is disjoint regions that are not connected by a continuous flow of the system⁵. Note that unlike ${\text {DC}}$, the rule ${\text {DDC}}$ does not require the initial set $\psi$ to be wholly contained inside $p>0$, $p=0$ or $p<0$. Instead, ${\text {DDC}}$ splits the initial set of states into three disjoint initial subsets $\psi \wedge p>0$, $\psi \wedge p=0$ and $\psi \wedge p<0$. The rule ${\text {DDC}}$ thus decomposes the original safety assertion into three independent safety assertions about smaller sub-systems, allowing the user to work on these separately. ${\text {DDC}}$ is of practical interest in cases when two or more of the sets $\psi \wedge p>0$, $\psi \wedge p=0$ and $\psi \wedge p<0$ are non-empty (otherwise, $\psi$ lies entirely within $p>0$, $p=0$ or $p<0$ and ${\text {DC}}$ may be applied to refine the constraint).

We now turn to applying the rules ${\text {DC}}$ and ${\text {DDC}}$ to tackle the state space explosion problem. In Algorithm 2 we give a procedure for refining the evolution domain constraint and removing polynomials from A, whenever this is possible, using the proof rules ${\text {DC}}$ and ${\text {DDC}}$. We call this procedure $DWC$ as it also exploits the sound reasoning principle of differential weakening ${\text {DW}}$ [19], i.e.

$$ ({\text {DW}})~\frac{H \rightarrow \phi }{\psi \rightarrow [\dot{\mathbf {x}} = f(\mathbf {x})~ \& ~H]~\phi }, $$

which simply requires that the evolution domain be contained within the post-condition to conclude that the system is safe.

On lines 3 and 4, $DWC$ applies the rule ${\text {DW}}$ as a sufficiency check for termination. On lines 7, 9 and 11 the procedure discards those p for which $p>0$, $p<0$ or $p=0$ describe a continuous invariant containing the initial set $\psi$ (conditionals on lines 6, 8 and 10). This step corresponds to an application of the rule DC with $F\equiv p>0$, $F\equiv p<0$ and $F\equiv p=0$ which, if the rule application is successful, are used to refine the evolution constraint H in the recursive call. If $p=0$ is an invariant in both positive and negative time and does not contain all the initial states $\psi$, one can use the proof rule ${\text {DDC}}$ to work with 3 smaller sub-systems of the original system whose reachable set may be constructed by combining the reachable sets of these smaller systems. This idea is implemented on lines 13-17 of Algorithm 2, where $DWC$ recurses on the 3 smaller sub-systems and removes the polynomial p (used to divide the system) from A. The over-approximations of reachable sets obtained using these 3 recursive calls are then combined into a union (line 17), which gives an over-approximation of the reachable set for the original system. Finally, when no further progress can be made, the procedure returns the evolution constraint H (line 18). Because the procedure only involves applying sound proof rules, one may view $DWC$ as a proof strategy that can be implemented in a theorem prover. Indeed, if the procedure returns a result while there are still polynomials remaining in A, one has a proof of safety involving only the proof rules ${\text {DW}}$, ${\text {DC}}$ and ${\text {DDC}}$.

Unlike $LazyReach$, the invariant generation procedure $DWC$ will not (in general) always be able to find a sufficiently strong continuous invariant to prove the safety property, even if one exists in the semi-algebraic abstraction by the polynomials A. The invariants $DWC$ is able to generate are thus generally coarser than those generated using $LazyReach$. However, we observe that in the worst case the running-time of $DWC$ is only quadratic in the number of polynomials $m=|A|$, i.e. $\mathcal {T}_{ DWC }(m) = O(m^2)$, compared the exponential time complexity of $LazyReach$.

We now combine the procedure $DWC$ together with the $LazyReach$ algorithm by replacing $\varvec{r}\mathrm {eturn} \ H$ on the final line (18) in $DWC$ with

$$ \begin{aligned} \varvec{r}\mathrm {eturn} \, LazyReach (\psi , \dot{\mathbf {x}} = f(\mathbf {x}) \, \& \ H, A). \end{aligned}$$

We call the resulting new invariant generation procedure $DWCL$. Instead of returning H when no further progress can be made with $DWC$, $DWCL$ falls back to using the more expensive $LazyReach$ algorithm with the remaining polynomials. This combined procedure is theoretically as powerful as $LazyReach$, i.e. is capable of extracting the exact reachable set $Reach _{A}^{\rightarrow }(\psi ,H)$ if necessary, but in practice also as fast as $DWC$, although theoretically the running time of $DWCL$ remains exponential in m.

Example 7

(Invariant generated using $DWCL$ ). Consider the non-linear planar system from [7, Ex. 10.7, p. 281] (with $H= \mathbb {R}^2$):

$$\begin{aligned} \dot{x}_1&= 2 x_1 \left( x_1^2-3\right) \left( 4 x_1^2-3\right) \left( x_1^2+21 x_2^2-12\right) , \\ \dot{x}_2&= x_2 \big (35 x_1^6+105 x_2^2 x_1^4-315 x_1^4-63 x_2^4 x_1^2 +378 x_1^2+27 x_2^6-189 x_2^4+378 x_2^2-216\big ), \end{aligned}$$

As an initial set, take $\psi \equiv \left( x_1-1\right) {}^2+x_2^2<\frac{1}{4}$ and let $\phi \equiv x_1^2+x_2^2<8$ be the post-condition. Consider an abstraction of this system using the irreducible polynomial factors of the right-hand side of the system of ODEs and the post-condition, i.e. let

$$\begin{aligned} A = \{&x_1, x_1^2-3, 4 x_1^2-3, x_2, x_1^2+x_2^2-8, x_1^2+21 x_2^2-12, \\&35 x_1^6+105 x_2^2 x_1^4-315 x_1^4-63 x_2^4 x_1^2\!+\!378 x_1^2+27 x_2^6 -189 x_2^4+378 x_2^2-216\}. \end{aligned}$$

There are 7 abstraction polynomials in total, which in the worst case could lead to $3^7 = 2187$ discrete states and $7^7 - 3^7 = 821356$ discrete transitions in the neighbouring transition relation $T_n$. In practice, applying $LazyReach$ to generate the reachable set $Reach _A^\rightarrow (\psi , H)$ for this problem takes an unreasonable amount of time. The procedure $DWC$ takes significantly less time to run, but is unable to find a suitable invariant using ${\text {DW}}$, ${\text {DC}}$ and ${\text {DDC}}$ alone. Our implementation of the combined procedure $DWCL$ is able to generate the following continuous invariant $I\subset \phi$ in 104 s:⁶

$$\begin{aligned}&\Bigg (\Big ( 35 x_1^6+105 \left( x_2^2-3\right) x_1^4+27 \left( x_2^6-7 x_2^4+14 x_2^2-8\right) <63 x_1^2 \left( x_2^4-6\right) \vee x_2=0 \Big ) \\&\wedge 4 x_1^2=3\wedge x_1>0 \Bigg ) \vee \left( x_2=0\wedge \Big (0<x_1<\frac{\sqrt{3}}{2}\vee \frac{\sqrt{3}}{2}<x_1<\sqrt{3}\Big )\right) \\&\vee \Bigg (35 x_1^6+105 \left( x_2^2-3\right) x_1^4+27 \left( x_2^6-7 x_2^4+14 x_2^2-8\right) <63 x_1^2 \left( x_2^4-6\right) \\&\wedge x_1^2+21 x_2^2<12 \wedge \Big (0<x_1<\frac{\sqrt{3}}{2}\vee \big (2 x_1>\sqrt{3}\wedge x_1^2<3\wedge x_2\ne 0\big )\Big )\Bigg ). \end{aligned}$$

For this problem, the procedure $DWCL$ makes repeated use of both ${\text {DC}}$ and ${\text {DDC}}$ (each is used 4 times in total) before falling back to $LazyReach$, which in every instance is given 3 polynomials that remain to perform the abstraction (down from 7 in the original list A).

Fig. 6.

Phase portrait, unsafe states $\lnot \phi$ (red), initial set $\psi$ (green) and a generated continuous invariant $I \subset \phi$ (blue) (Color figure online).

5.3 Sources of Polynomials for Abstraction

Discrete semi-algebraic abstraction relies on the user supplying a set of polynomials A to construct the set of discrete states through semi-algebraic decomposition of the evolution constraint. The verification problem itself is often a good source of polynomials; e.g. they could come from the description of the (semi-algebraic) post-condition $\phi$, the pre-condition $\psi$, or indeed from the right-hand side of the (polynomial) system of ODEs, i.e. the polynomials $f_1, f_2, \dots , f_n$, their irreducible factors, etc. The use of Lie derivatives as a source of polynomials for abstraction was previously investigated in [37] (see also [39] for related work). In [43] abstraction is explored using Darboux polynomials (see [9, 10]), whose real roots are invariant under the flow of the system. Recent results on real algebraic invariant checking [8] enable us to consider a more general class of polynomials that share this property but are not necessarily Darboux (Fig. 6).

6 Practical Evaluation

In this section we compare the performance of our invariant generation algorithms $LazyReach$, $DWC$ and $DWCL$ on a set of 100 safety verification problems for continuous systems. The differential equations used in these problems are predominantly non-linear and originate from examples found in texts on dynamical systems [4, 5, 7, 10, 33, 41], papers on the qualitative theory of ODEs and safety verification of continuous and hybrid systems [11, 25, 31, 32, 40].⁷

The running time performance⁸ of the algorithms is summarised in Fig. 7. In the graphs, the vertical axis gives the dependent time variable (in seconds on a $\log$ scale) and the horizontal axis denotes the number of problems that could be solved in under the time given by the curve for each algorithm. By solved we understand that a semi-algebraic continuous invariant has been successfully generated and that it implies the postcondition, i.e. is sufficient to prove the safety assertion.

Fig. 7.

Safety verification performance.

In our experiments we:

• 1. use polynomial factors of the right-hand side of the ODEs together with the factors of the polynomials appearing in the postcondition $\phi$ to create the set of polynomials A for the semi-algebraic decomposition (Fig. 7a),

• 2. extend the set A generated as in (1.) with Lie derivatives of every polynomial in A (Fig. 7b), and

• 3. explore the utility of using polynomials whose real roots are invariant real algebraic sets by extending the list of polynomials generated in (1.) and (2.) with polynomials generated using a method presented in [8] (Fig. 7c and d respecitvely).

In our results we observe that the $DWC$ algorithm is significantly faster than $LazyReach$, confirming our hopes for gains in efficiency. We observe that, when using polynomial factors of the ODEs and the postcondition to abstract the system, $LazyReach$ was able to prove as many problems as $DWC$ (43), although the set of problems solved is different. This is not surprising, since a proof strategy involving ${\text {DW}}$, ${\text {DC}}$ and ${\text {DDC}}$, while very efficient, cannot in general be used to extract reachable sets of exact abstractions like the more expensive $LazyReach$. The combined method $DWCL$ (using ${\text {DW}}$, ${\text {DC}}$, and ${\text {DDC}}$ before falling back to $LazyReach$) is seen to be both as practically efficient as $DWC$ and able to solve more problems (50) than $LazyReach$ under a 600 s timeout; of course, given enough time, $DWCL$ and $LazyReach$ will both succeed at solving exactly the same problems (with $LazyReach$ taking significantly more time).

Adding the first Lie derivatives of the polynomial factors of the ODE and the postcondition effectively doubles the size of the list A which, unsurprisingly, leads to diminished performance of $LazyReach$ (only 25 problems solved) because it is heavily affected by the discrete state explosion problem. However, $DWC$ is seen to perform slightly better than it did without the Lie derivatives in the list, solving a total of 46 safety verification problems. The $DWCL$ algorithm succeeds at proving safety in 52 of the problems.

We observe that adding algebraic invariants to the list of polynomial factors of the ODE and the postcondition resulted in a palpable improvement in the number of problems that could be solved. This is very clearly visible in the case of $DWC$, which is guaranteed to process every algebraic invariant by applying the proof rules ${\text {DC}}$ and ${\text {DDC}}$. Overall, for this choice of polynomials we see $LazyReach$ solving 46, $DWC$ solving 52, and $DWCL$ solving 60 problems out of 100 (see Fig. 7c). Likewise, by adding algebraic invariants to the list of polynomial factors and their Lie derivatives (as in 2.) we were able to solve 26, 53 and 59 problems using $LazyReach$, $DWC$ and $DWCL$ respectively (Fig. 7d).

Overall, in every set of benchmarks we observe only one problem for which the algorithm $DWC$ times out after 600 s, whereas $LazyReach$ times out for many of problems (e.g. in the experiments shown in Fig. 7d $LazyReach$ timed out on 59 of the problems and was unable to produce a suitable invariant within the time limit in only 15 instances). The procedure $DWCL$ generally times out more often than $DWC$, but significantly less frequently than $LazyReach$ (e.g. 25 problems from Fig. 7d resulted in a timeout, and 16 could not be solved using the resulting invariant).

These results are very encouraging as they demonstrate that the discrete state explosion problem can, to a certain extent, be addressed using algorithms such as $DWCL$ and that methods for automatic algebraic invariant generation (such as that in [8]) can be used to generate polynomials that will often improve the quality of the resulting abstractions.

It is perhaps surprising to see that many of the atomic predicates featuring irreducible factors of polynomials harvested from the problem define continuous invariants. As such, these polynomials are eminently suitable for processing using our algorithms $DWC$ and $DWCL$ without incurring the performance penalty associated with building finer abstractions using the conventional approach.

7 Related Work

In [44], the authors apply their earlier results about checking semi-algebraic continuous invariants to address the invariant generation problem using approaches such as pre-defining parametric templates and restricting attention to classes of invariants (such as polyhedra), as well as using qualitative analysis techniques to suggest invariant templates. Our approach is different in that we do not rely on parametric templates and put no restrictions on the form of the semi-algebraic invariant which may be generated. Discrete abstraction of linear systems using linear polynomials to discretize the state space was investigated in [2, 3]. A method for abstracting non-linear systems using non-linear polynomials was studied in [36, 37], but results in abstractions that are inexact; the fundamental differences between this approach and our work is discussed at length in Sect. 3. A powerful technique called relational abstraction was introduced in [29]. With relational abstraction one aims to over-approximate the finite time reachability relation between states in a continuous system. Computing relational abstractions requires searching for appropriate invariants in a larger auxiliary continuous system; once a relational abstraction is available, one may use it to extract a continuous invariant containing any given initial state of the system. Computing good relational abstractions for non-linear systems is in practice expensive because it involves searching for invariants in continuous systems with double the original number of state variables.

8 Conclusion

This paper presented a powerful method for automatically discovering continuous invariants that can be used in a formal deductive system to prove safety assertions about continuous systems. We removed some important theoretical limitations (unsoundness and coarseness) in existing methods for constructing discrete abstractions of non-linear continuous systems and presented scalable and efficient algorithms for continuous invariant generation that combine discrete semi-algebraic abstraction with sound proof rules for deductive safety verification. Verification of hybrid systems constructively reduces to proving properties of differential equations [18, 20], which provides a wider context for the future development of our work. The results we observe are highly encouraging, but much further work remains before safety verification (in the continuous fragment) of hybrid systems can enjoy a high level of automation. For instance, now that issues associated with inexact abstractions have been removed, the (difficult [39]) problem of finding a good choice of polynomials for constructing the semi-algebraic predicates is the only factor that determines the success of our approach. We observed that polynomials whose real roots themselves define invariants [8] can often be used to improve the quality of abstractions; however the broader problem of choosing the right polynomials leaves many interesting questions for future research.