Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems

Abstract

Semi-algebraic abstraction is an approach to the safety verification problem for polynomial dynamical systems where the state space is partitioned according to the sign of a set of polynomials. Similarly to predicate abstraction for discrete systems, the number of abstract states is exponential in the number of polynomials. Hence, semi-algebraic abstraction is expensive to explicitly compute and then analyze (e.g., to prove a safety property or extract invariants).

In this paper, we propose an implicit encoding of the semi-algebraic abstraction, which avoids the explicit enumeration of the abstract states: the safety verification problem for dynamical systems is reduced to a corresponding problem for infinite-state transition systems, allowing us to reuse existing model-checking tools based on Satisfiability Modulo Theory (SMT). The main challenge we solve is to express the semi-algebraic abstraction as a first-order logic formula that is linear in the number of predicates, instead of exponential, thus letting the model checker lazily explore the exponential number of abstract states with symbolic techniques. We implemented the approach and validated experimentally its potential to prove safety for polynomial dynamical systems.

1 Introduction

Non-linear dynamical systems are characterized by continuous evolution resulting from ordinary differential equations containing non-linear polynomials. Proving safety properties for non-linear dynamical systems is extremely challenging, and several approaches have been proposed. Semi-automatic deductive verification techniques based on theorem proving include proving hybrid programs using differential dynamic logic [27] or hybrid Cyber Physical System (CPS) using Hybrid Hoare Logic (HHL) [21]). Among various automatic techniques (e.g., [30]), an important line of work applies symbolic model checking to abstractions of hybrid systems, both with, using qualitative predicate abstraction [34]. Unfortunately, the problem with the above techniques is twofold. On one side, the abstractions are often unable to precisely lift important information, thus resulting in an abstract system that is not strong enough to prove the property. On the other side, the abstraction computation may be too expensive to compute, especially in the non-linear case.

To tackle the first problem, we consider the semi-algebraic decomposition for dynamical systems of [32]. The idea is to build an abstraction from a given set of polynomials, partitioning the concrete state space according to the sign of each polynomial. The abstraction is exact: there is a transition from an abstract state to another abstract state if and only if there is (at least) a concrete transition from the two concretizations of the abstract states. Semi-algebraic decomposition is also appealing because it can be made more precise adding new polynomials.

The abstraction can be computed by means of logical operations (by repeatedly checking the satisfiability of quantifier-free formulas interpreted over the reals). However, the second problem remains: the explicit computation of the abstraction is extremely costly, since it requires the enumeration of all possible transitions between abstract states, which are exponential in the number of considered polynomials.

Interestingly, an effective use of abstraction is at the core of the most successful verification techniques for discrete infinite-state transition systems. The technique of predicate abstraction [16] was originally adapted for symbolic verification in [9] and then optimized in [19]. This idea has been further developed in implicit predicate abstraction [35], which eliminates the burden of an up-front exponential blowup in the computation of the abstract states by embedding the abstraction in the symbolic encoding of the transitions. This approach has been used also in combination with IC3 [1, 5, 6].

In this paper, we propose a new approach to the verification of dynamical systems with non-linear polynomial dynamics based on the use of semi-algebraic decomposition. The contributions of the paper are the following:

• We cast the problem of computing and verifying properties of dynamical systems using the semi-algebraic decomposition in the framework of verification via implicit predicate abstraction (i.e., a first-order logic characterization of the semi-algebraic decomposition abstraction). Thus, we apply SMT-based model checking techniques to prove safety properties of polynomial dynamical systems.

• We define a linear symbolic encoding for the abstraction. Note that the naive formulation of the predicate abstraction problem (which follows from the explicit computation approach proposed in [32]) is not effective in practice: in fact, the number of abstract states is exponential in the total number of polynomials that define the abstraction, and the encoding requires to enumerate all the possible pairs of abstract states to check the existence of an abstract transition. We exploit the properties of the LZZ formulation to define a concise encoding that is linear in the number of the polynomials, hence making the approach feasible in practice.

• We implement and experimentally evaluate the approach. The results show how the reduction to the verification of discrete infinite-state transition systems is complementary to reachability analysis techniques and proves cases that were previously out of reach for the state-of-the-art tools.

Outline: The rest of the paper is structured as follows: Sect. 2 gives an overview of the approach with a motivating example; Sect. 3 provides the background definitions; Sect. 4 shows the naive encoding of the abstraction, while in Sect. 5 we derive the linear encoding and define the related implicit semi-algebraic abstraction; in Sect. 6, we present the experimental results; in Sect. 7, we discuss the related work and, finally, in Sect. 8, we draw some conclusions and directions for future work.

2 Overview of the Approach

Consider a verification problem (adapted from [22]) on the non-linear dynamical system with two variables x and y, and differential equations $\dot{x} = -2y, \dot{y} = x^2$. We want to prove that the system cannot reach the set of bad states $(x+2)^2+y^2-1 \le 0$ (i.e., it never leaves the safe region $(x+2)^2+y^2-1 > 0$) when starting from the initial set of states $x-y-\frac{1}{2} \ge 0 \wedge x + 2 > 0$. Note that although in this example the evolution of the system is not restricted, our approach can deal with the more general case in which the evolution is constrained by an invariant condition that must always hold. The system is safe and avoids the set of bad states (see system’s dynamic in Fig. 1a).

We can prove that the system is safe by first constructing and then model checking a discrete semi-algebraic abstraction [32]: given the set of polynomials $\mathbb {A}:= \{x - y - \frac{1}{2},x + y + \frac{1}{2},x + 2\}$, the semi-algebraic abstraction partitions the state space according to the sign ($\{>,<,=\}$) of the polynomials in $\mathbb {A}$ (an example of abstract state is the state $x + 2 > 0 \wedge x - y - \frac{1}{2}< 0 \wedge x + y + \frac{1}{2} < 0$ represented as ① in Fig. 1b). There exists a transition from an abstract state to another one if the two states are neighbors and there exists at least one trajectory of the dynamical system going from one state to the other. The existence of such condition can be checked using the LZZ algorithm [22], which checks if a semi-algebraic set $\psi$ is a differential invariant for a polynomial dynamical system $\boldsymbol{f}$ when its execution is restricted to the domain H (another semi-algebraic set). The algorithm reduces the invariant check to the satisfiability of the Non-Linear Real Arithmetic Theory formula $\textit{LZZ}_{{\psi },{\boldsymbol{f}},{H}}{(Z)}$, where $Z$ is a set of real-valued variables. We can systematically check if there exists a transition from an abstract state $s_1$ to the abstract state $s_2$ proving that $s_1$ is not invariant when restricted to the domain $s_1 \vee s_2$ (i.e., checking that $\textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)}$ is false).

Furthermore, we can use an algorithm, called LazyReach [32], to compute the forward set of reachable abstract states starting from the initial states. As usual, if no abstract states intersect the set of bad states then the system is safe, and the reachable set of abstract states is a continuous invariant for the system. Figure 1b shows the state space of the dynamical system: the initial and bad states of the verification problem (represented with the green and red region respectively), the solution of the polynomials from $\mathbb {A}$ (represented as blue lines), and further superimpose the set of reachable abstract states and transitions (represented as numbered circles and arrows between the circles). The abstraction shown in Fig. 1b is the result after applying LazyReach to the verification problem.

Fig. 1.

Safety verification problem and reachable states of the abstraction for the non-linear dynamical system $\dot{x} = -2y, \dot{y} = x^2$, bad states $(x+2)^2+y^2-1 \le 0$ (red circle), and initial set of states $x-y-\frac{1}{2} \ge 0 \wedge x + 2 > 0$ (green region). Figure (a) shows the verification problem and the system’s vector field. Figure (b) shows the reachable abstract states and the transitions of the algebraic abstraction (numbered circles and arrows) computed using LazyReach and the differential invariant (green and gray regions) obtained from the set of polynomials $\mathbb {A}= \{x - y - \frac{1}{2},x + y + \frac{1}{2},x + 2\}$ (blue lines), computed using Implicit Abstraction. Abstract states represent different combinations of signs for the abstraction’s polynomials. Examples of abstract states are ① $x + 2 > 0 \wedge x - y - \frac{1}{2}< 0 \wedge x + y + \frac{1}{2} < 0$, ② $x + 2 > 0 \wedge x - y - \frac{1}{2} = 0 \wedge x + y + \frac{1}{2} < 0$, and ③ $x + 2 > 0 \wedge x - y - \frac{1}{2} = 0 \wedge x + y + \frac{1}{2} = 0$. (Color figure online)

A main challenge for the LazyReach algorithm is to explicitly enumerate the reachable states and transitions among them, since their number is exponential in the number of polynomials $\mathbb {A}$ (i.e., the number of total states is already $3^{|\mathbb {A}|}$). For the example above, where we have 3 polynomials, the maximum number of states would be 27, with an even bigger number of transitions (e.g., one must consider the transition between each pair of neighbouring abstract states). Even if LazyReach enumerates the reachable abstract states on-the-fly, the explosion in the number of states and transitions is still a bottleneck. Our implementation of $LazyReach$ applied to the above example explores a total of 9 states and checks the existence of 27 transitions, taking about 12 s to complete.

A possible solution to tackle the state explosion problem is the DWCL algorithm, proposed in [32]. The DWCL algorithm¹ tries to reduce the number of abstract states by checking if the sign of a polynomial $a \in \mathbb {A}$ is invariant, that is if:

• the sign of the polynomial a does not change in the initial states (i.e., the predicate $a \bowtie 0$, with $\bowtie \in \{<,>,=\}$, holds for all the initial states); and

• $a \bowtie 0$ is a continuous invariant for the dynamical system (this can be checked with $\textit{LZZ}_{{a \bowtie 0},{\boldsymbol{f}},{H}}{(Z)}$).

When a predicate $a \bowtie 0$ is a continuous invariant, the algorithm strengthens the invariant of the dynamical system (by adding $a \bowtie 0$ to the invariants), allowing to remove a from the set of polynomials $\mathbb {A}$. While the DWCL algorithm may already find a strong-enough invariant to prove the safety property, the algorithm falls back to the LazyReach algorithm in the general case to explore the abstract state space, hopefully with a strengthened invariant domain and a smaller set of polynomials. In practice, the state-space explosion problem of LazyReach still exists in the case “not enough” polynomials are sign-invariant, as it happens in our motivating example. In the example, no polynomials are sign-invariant²: this means that the DWCL algorithm will not remove any polynomials from the set $\mathbb {A}$ and LazyReach will still suffer from the state-space explosion problem.

The semi-algebraic abstraction is a specific instance of predicate abstraction [16] of the dynamical system $\boldsymbol{f}$. For discrete-state systems, there exist efficient algorithms to either explicitly compute the abstraction using Satisfiability Modulo Theory (SMT) solvers [19, 20] or to implicitly represent the abstraction and directly verify a safety property (e.g., implicit predicate abstraction [35]). Since these algorithms work on a fully symbolic representation of the abstract state space, they can cope with the state-space explosion due to the number of predicates of the abstraction. However, applying the same symbolic-state techniques to compute or verify the semi-algebraic abstraction is still challenging, mainly because it requires to express the transition relation $T(X,X')$ of the semi-algebraic abstraction in a first-order logic formula. We notice that such transition relation T can be directly obtained from the abstraction’s definition³:

$$ \exists Z. \Bigg ( \bigvee _{(s_1,s_2) \in 3^\mathbb {A}}{ s_1(X) \wedge s_2(X') \wedge (\lnot \textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)}) \Bigg ). } $$

The above transition relation enumerates all the possible pairs of abstract states and its size is exponential in the number of polynomials in $\mathbb {A}$. The additional variables $Z$ are copies of the state variables of the system and are used to encode the LZZ condition. Clearly, even creating such formula is not scalable and hinders the application of the standard abstraction and verification techniques used for discrete systems. Note that, while the LZZ algorithm works for semi-algebraic sets (i.e., the candidate invariant $\psi$ and the invariant states H are both arbitrary Boolean combinations of non-linear arithmetic terms), here we apply LZZ to check the existence of a transition between two abstract states, hence we still have to explicitly enumerate the abstract transitions.

Our main contribution, presented in Sect. 5, is a compact formulation of the above transition relation that has a size linear in the number of the polynomials $\mathbb {A}$. The steps to obtain such exponentially smaller transition are:

• 1. We specialize the LZZ formula $\lnot \textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)}$ to encode the existence of a transition between two abstract states $s_1$ and $s_2$. The resulting formula is a disjunction, and each disjunct encodes the necessary and sufficient condition for a continuous transition to $s_2$ to exist, either inside the set $s_1(Z)$ or outside the set $\lnot s_1(Z)$. Intuitively, we obtain a specific encoding for checking the existence of an abstract transition, instead of reusing the LZZ as a “black box”.

• 2. We “lift” the above disjunction to the disjunction of all the abstract states, obtaining the formula:

  $$ \exists Z. (\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z}) \vee \textit{OutExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})), $$

  where $\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$ encodes the “inside condition” for all the pairs of transitions (and similarly for the “outside condition” $\textit{OutExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$).

• 3. The formula $\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$ still contains an explicit enumeration on the pairs of abstract states. We show how we obtain an equivalent formula, $\textit{InsSymb}_{{\boldsymbol{f}}}({X},{X'},{Z})$, that encodes the same condition for each polynomial $a \in \mathbb {A}$ in the abstraction, obtaining a linear, instead of exponential, encoding. We apply the same reasoning on $\textit{OutExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$.

We then use the concise transition relation of T to obtain a symbolic transition system $S_{\textit{Impl},\mathbb {P}}$ that implicitly encodes the semi-algebraic abstraction for the dynamical system $\boldsymbol{f}$ with the polynomials $\mathbb {A}$ and predicates $\mathbb {P}= \{a \bowtie 0 \mid a \in \mathbb {A}\ \wedge \ \bowtie \in \{>,<,=\}\}$. Technically, instead of computing the predicate abstraction, we encode an implicit abstraction [35]. Consequently, we avoid the expensive quantifier elimination step. We can then verify the safety property on the transition system $S_{\textit{Impl},\mathbb {P}}$ using an SMT-based model checking algorithm. We use the algorithm from [4], since $S_{\textit{Impl},\mathbb {P}}$ contains non-linear arithmetic formulas. Our approach verifies the example of Fig. 1 and finds the continuous invariant:

$$\begin{aligned}\begin{gathered} (x - y < \frac{1}{2} \vee x \ge -2) \wedge (x - y \ge \frac{1}{2} \vee x + y \ge -\frac{1}{2}) \wedge (x - y \ge \frac{1}{2} \vee x + y > - \frac{1}{2}), \end{gathered}\end{aligned}$$

which is shown in the union of the green and gray regions in Fig. 1b.

3 Preliminaries

In this work, we consider first order logic formulas in the theory of non-linear arithmetic over the reals (NRA). We denote with $\phi (X)$ the formula $\phi$ containing free variables from the set $X = \{x_1, \ldots , x_n\}$. We simplify the notation of the formula $\phi (X)$ to $\phi$ when the set X is clear from the context.

Invariant Verification for Polynomial Dynamical Systems Safety Verification of Dynamical Systems. Given a set of variables X we write $\boldsymbol{X} = [x_1, \ldots , x_n]^T$ to specify a vector containing all the variables in X ordered lexicographically. We use the subscript $\boldsymbol{X}_i$ to access to the i-th element of the vector. We focus on polynomial dynamical systems of ordinary differential equations (ODEs) $\boldsymbol{\dot{X}} = \boldsymbol{f}(\boldsymbol{X})$, where $\boldsymbol{\dot{X}}$ is the vector of first-order derivatives of the variables $\boldsymbol{X}$ and $\boldsymbol{f}(\boldsymbol{X})$ is a vector of polynomials (i.e., $\boldsymbol{f}_i(\boldsymbol{X})$ is a polynomial). The safety verification problem consists of proving that every trajectory of the dynamical system $\boldsymbol{\dot{X}} = \boldsymbol{f}(\boldsymbol{X})$ starting inside the initial set of states $\psi$ and while being inside the evolution domain constraints H remains inside the safe set of states $\phi$. We write the problem using the differential dynamic logic [27] formula:

$$ \begin{aligned} \psi \rightarrow [\boldsymbol{\dot{X}} = \boldsymbol{f}(\boldsymbol{X})\ \& \ H] \phi , \end{aligned}$$

(1)

asserting that if the system is in a state satisfying the pre-condition $\phi$ (the initial states) this implies ($\rightarrow$ operator) that all the trajectories evolving according to the ODE $\boldsymbol{\dot{X}} = \boldsymbol{f}(\boldsymbol{X})$ and evolution domain H (box modality []) will satisfy the post-condition $\phi$ (the safe states). Formally, the system is safe if:

$$ \forall \boldsymbol{x}_0 \in \psi . \forall \tau \ge 0. \forall t \in [0,\tau ]. ( (\varphi (\boldsymbol{x}_0,t) \in H) \rightarrow \varphi (\boldsymbol{x}_0,t) \in \phi ), $$

were the differentiable function $\varphi : \mathbb {R}^{n+1} \rightarrow \mathbb {R}^n$, such that $\frac{d}{dt}(\varphi (\boldsymbol{x}_0,t)) = \boldsymbol{f}(\varphi (\boldsymbol{x}_0,t))$, is the solution to the initial value problem $\boldsymbol{x}_0 \in \mathbb {R}^n$ (i.e., $\varphi (\boldsymbol{x}_0,t)$ describes the state the dynamical system $\boldsymbol{f}$ reaches after $t \in \mathbb {R}$ time when starting in the initial state $\boldsymbol{x}_0$).

The problem of proving the system is safe can be reduced to find a formula $\theta (X)$ such that: i) $H \wedge \psi \rightarrow \theta$, ii) $\theta \rightarrow [\boldsymbol{\dot{X}} = \boldsymbol{f}(\boldsymbol{X})\ \& \ H]\ \theta$, and iii) $\theta \rightarrow \phi$. $\theta (X)$ is a continuous invariant [28] that contains the initial states and that is contained in the safe states.

LZZ Algorithm  [22]. The LZZ algorithm reduces the problem of checking if $\theta$ is a continuous invariant to checking the validity of the following formula:

$$\begin{aligned} \textit{LZZ}_{{\theta },{\boldsymbol{f}},{H}}{(X)} \,\dot{=}\,&( (\theta (X) \wedge H(X) \wedge \textit{In}_{{\boldsymbol{f}},{H}}({X})) \rightarrow \textit{In}_{{\boldsymbol{f}},{\theta }}({X})) \wedge&\\&( (\lnot \theta (X) \wedge H(X) \wedge \textit{In}_{-{\boldsymbol{f}},{H}}({X})) \rightarrow \lnot \textit{In}_{-{\boldsymbol{f}},{\theta }}({X})),&\nonumber \end{aligned}$$

(2)

where the formula $\textit{In}_{{\boldsymbol{f}},{\gamma }}({X})$ for the ODEs $\boldsymbol{f}$ and the formula $\gamma$ represents the set of states which will evolve inside the set $\gamma$ for some non-zero time in the future. Respectively, the formula $\textit{In}_{-{\boldsymbol{f}},{\gamma }}({X})$ represents the set of states evolved inside the set $\gamma$ for some non-zero time in the past, and $-\boldsymbol{f}$ represents the dynamical system evolving in “reverse”. Note that the construction of the formula $\textit{In}_{{\boldsymbol{f}},{\gamma }}({X})$ assumes $\gamma$ to be in disjunctive normal form (DNF):

$$\begin{aligned} \gamma = \bigvee _{d \in disj(\gamma )}{ \bigwedge _{a \bowtie 0 \in pred(d)}{ a(X) \bowtie 0 } }, \end{aligned}$$

where $disj(\gamma )$ are the disjuncts of a formula $\gamma$, pred(d) are the predicates in the disjunct d, and $\bowtie \in \{>,\ge \}$⁴. The formula $\textit{In}_{{\boldsymbol{f}},{\gamma }}({X})$ is defined as:

$$\begin{aligned} \textit{In}_{{\boldsymbol{f}},{\gamma }}({X}) = \bigvee _{d \in disj(\gamma )}{ \bigwedge _{a \bowtie 0 \in pred(d)}{ \textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({X}) } }. \end{aligned}$$

(3)

The formula $\textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({X})$ encodes the set for a single predicate $a \bowtie 0$ using the Lie derivatives of the polynomial a(X). The i-th Lie derivative $L_{\boldsymbol{f}}^ia$ of a polynomial a(X) with respect to the ODEs $\boldsymbol{f}$ is defined recursively as:

$$\begin{aligned} L_{\boldsymbol{f}}^{(0)} {a} \,\dot{=}\,a, \qquad L_{\boldsymbol{f}}^{(i)} {a} \,\dot{=}\,\frac{\partial }{\partial \boldsymbol{X}} L_{\boldsymbol{f}}^{(i-1)} {a} \boldsymbol{f}. \end{aligned}$$

$\textit{In}_{{\boldsymbol{f}},{a > 0}}({X})$ encodes that the first non-zero Lie derivative of a must be positive in order for the trajectories of the system to enter the set $a > 0$ and stay inside the set for a positive time⁵(see [22] and [12] for a thorough explanation):

$$\begin{aligned} \textit{In}_{{\boldsymbol{f}},{a> 0}}({X})&\,\dot{=}\,\bigvee _{0 \le i \le N_{a,f}}{ \Bigg (\bigwedge _{0 \le j < i}{L_{\boldsymbol{f}}^{(j)} {a} = 0} \wedge L_{\boldsymbol{f}}^{(i)} {a} > 0 \Bigg ), }\end{aligned}$$

(4)

$$\begin{aligned} \textit{In}_{{\boldsymbol{f}},{a \ge 0}}({X})&\,\dot{=}\,\textit{In}_{{\boldsymbol{f}},{a > 0}}({X}) \vee \bigvee _{0 \le i \le N_{a,f}}{L_{\boldsymbol{f}}^{(i)} {a} = 0}, \end{aligned}$$

(5)

where $N_{a,\boldsymbol{f}}$ is an integer constant and is an upper bound on the minimum integer number r (called rank) such that $L_{\boldsymbol{f}}^{(r)} {a} \ne 0$ (for all $x \in \mathbb {R}^n$). $N_{a,\boldsymbol{f}}$ can be computed using Gröbner basis as explained in [22].

In the following, we will only use the fact that the formula $\textit{In}_{{\boldsymbol{f}},{\gamma }}({X})$ for the DNF formula $\gamma$ is the DNF formula where $In_{f}$ is applied to the predicates (as shown in Formula (3)).

Semi-Algebraic Abstraction  [32]. The semi-algebraic abstraction of the dynamical system $\boldsymbol{\dot{X}} = \boldsymbol{f}(\boldsymbol{X})$ partitions its state space with respect to a set of polynomials $\mathbb {A}\,\dot{=}\,\{a_1, \ldots , a_m\}$. The abstraction is the (explicit state) transition system $S_\mathbb {A}\,\dot{=}\,\langle 3^{\mathbb {A}}, I_{f,\mathbb {A}}, T_{f,\mathbb {A}} \rangle$ where:

• $3^{\mathbb {A}} \,\dot{=}\,\{s = \bigwedge _{a \in \mathbb {A}}{a \bowtie 0} \mid \bowtie \in \{>,<,=\}\}$ is the set of abstract states;

• $I_{f,\mathbb {A}} \,\dot{=}\,\{ s \in 3^\mathbb {A}\mid s \wedge \psi \text { is satisfiable}\}$ is the set of abstract initial states; and

• $T_{f,\mathbb {A}} \subseteq 3^{\mathbb {A}} \times 3^{\mathbb {A}}$ is the abstract transition relation. A transition $(s_1,s_2) \in T_{f,\mathbb {A}}$ if:

  • $s_1$ is an abstract state adjacent to $s_2$. The abstraction exploits the continuity assumption on $\boldsymbol{f}$ and does not allow the system to transition directly from a state where a predicate is greater than 0 (e.g., $a>0$) to a state where the same predicate is less than 0 (e.g., $a < 0$), and vice-versa. The abstraction does not visit two abstract states containing predicates with opposite signs, forcing instead to visit the intermediate state where the predicate is equal to 0.

  • There exists a continuous trajectory from $s_1$ to $s_2$. This condition corresponds to checking that the following differential dynamic logic formula is not valid (i.e. $s_1$ is not a differential invariant when restricting the evolution domain to $s_1 \vee s_2$):

    $$ s_1 \rightarrow [\boldsymbol{\dot{X}} = \boldsymbol{f}(\boldsymbol{X})\ \& \ s_1 \vee s_2] s_1, $$

    which can be checked using the sound and complete LZZ algorithm, i.e. checking the satisfiability of the first-order formula $\lnot \textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)})$.

Since the number of states $3^\mathbb {A}$ is finite we can compute the set of reachable states. The concretization of this set, $\theta$ contains the initial states and is a differential invariant. If $\theta$ further implies the safe states $\psi$, then we prove the safety verification problem 1. However, the computation of the abstract transition relation is exponential in the number of polynomials in $\mathbb {A}$ because we would need to enumerate all the possible pairs of transitions $(s_1,s_2) \in 3^\mathbb {A}\times 3^\mathbb {A}$.

Predicate Abstraction

A symbolic transition system S is a tuple $S \,\dot{=}\,\langle V,I,T \rangle$, where V is a set of (state) variables, I(V) is a formula representing the initial states, and $T(V,V')$ is a formula representing the transition relation. A state s of S is an interpretation of the state variables V. A (finite) path $\pi$ of S is a finite sequence $\pi \,\dot{=}\,s_0,s_1,\ldots ,s_k$ of states with the same domain and interpretation of symbols in the signature $\Sigma$ such that $s_0\models I$ and for all i, $0\le i<k$, $s_i, s'_{i+1} \models T$. We say that a state s is reachable in S iff there exists a path of S ending in s. Given a formula P(V) and a transition system S, the invariant verification problem, denoted with $S\models P$, checks if for all the finite paths $s_0,s_1,\ldots ,s_k$ of S, for all i, $0\le i\le k$, $s_i\models P$.

Predicate Abstraction [16] partitions the concrete system $S=\langle V,I,T \rangle$ according to a finite set of predicates $\mathbb {P}\,\dot{=}\,\{p_1, \ldots , p_k\}$ in a finite symbolic transition system:

$$ {\widehat{S}}_{\mathbb {P}} = \langle V_{\mathbb {P}}, {\widehat{I}}_{\mathbb {P}}(V_{\mathbb {P}}), {\widehat{T}}_{\mathbb {P}}(V_{\mathbb {P}}, V'_{\mathbb {P}}) \rangle $$

using a new abstract Boolean variable $v_{p}$ for each predicate $p$ ($V_{\mathbb {P}} = \{v_{p} \mid v \in V\}$ is the set of those new variables). The abstraction relation $\textit{H}_{\mathbb {P}}(V,V_{\mathbb {P}}) \,\dot{=}\,\bigwedge _{p\in \mathbb {P}} v_{p} \leftrightarrow p(V)$ defines how a set of concrete states is abstracted to the abstract states. We compute the abstraction of a formula $\psi (V)$ by existentially quantifying the concrete variables V:

$$ {\widehat{\psi }}_{\mathbb {P}}(V_{\mathbb {P}}) \,\dot{=}\,\exists V. (\psi (V) \wedge \textit{H}_{\mathbb {P}}(V,V_{\mathbb {P}})). $$

Similarly, we compute the abstract transition relation for $T(V,V')$:

$$ {\widehat{T}}_{\mathbb {P}}(V_{\mathbb {P}}, V'_{\mathbb {P}}) \,\dot{=}\,\exists V,V'. (T(V,V') \wedge \textit{H}_{\mathbb {P}}(V,V_{\mathbb {P}}) \wedge \textit{H}_{\mathbb {P}}(V',V'_{\mathbb {P}})). $$

The above formulation is sufficient to compute the predicate abstraction for an infinite-state transition system $S = \langle V,I,T \rangle$ and a set of predicates $\mathbb {P}$. However, the main challenge in computing the abstraction is to eliminate the quantifiers, since quantifier elimination is expensive to compute.

Implicit Predicate Abstraction. Implicit Predicate Abstraction [35] is a model checking algorithm that avoids computing the abstract version of the initial states, safety property, and transition relation, instead it encodes the existence of a path in the abstract system. It exploits the fact that the abstraction induces an equivalence relation among concrete states of the system (i.e., two concrete states are equivalent if they belong to the same abstract state) and that this relation can be expressed as a quantifier free formula:

$$\begin{aligned} \textit{EQ}_{\mathbb {P}}(V,\overline{V})\,\dot{=}\,\bigwedge _{p\in \mathbb {P}} p(V) \leftrightarrow p(\overline{V}). \end{aligned}$$

(6)

We use the equivalence $\textit{EQ}_{\mathbb {P}}(V,\overline{V})$ to relate two sets of concrete states and we encode the problem of reaching a set of target states $\lnot P$ in k steps of the transition system S as follows:

$$\begin{aligned} \textit{BMC}_{\mathbb {P}}^{k}&\,\dot{=}\,&I(V^0)\wedge \textit{EQ}_{\mathbb {P}}(V^0,\overline{V}^0) \wedge \\&\bigwedge _{1\le h< k} \Big ( T(\overline{V}^{h-1},V^h) \wedge \textit{EQ}_{\mathbb {P}}(V^h,\overline{V}^h) \Big ) \wedge T(\overline{V}^{k-1},V^{k}) \wedge \\&\textit{EQ}_{\mathbb {P}}(V^k,\overline{V}^k) \wedge (\lnot P(\overline{V}^k)). \end{aligned}$$

The formula $\textit{BMC}_{\mathbb {P}}^{k}$ is satisfiable iff there exists a path in the abstract transition system ${\widehat{S}}_{\mathbb {P}}$ of length k starting from the (abstracted) initial states ${\widehat{I}}_{\mathbb {P}}(V_{\mathbb {P}})$ and reaching the (abstracted) bad states ${\widehat{\lnot P}}_{\mathbb {P}}(V_{\mathbb {P}})$.

4 Explicit Computation of the Semi-Algebraic Abstraction

We frame the problem of computing the semi-algebraic abstraction as a predicate abstraction problem. This formulation allows us to use the standard techniques to compute or analyze the predicate abstraction for discrete systems.

We consider the invariant verification problem $\psi \rightarrow [\boldsymbol{\dot{X}} = \boldsymbol{f}(\boldsymbol{X})\ \& \ H] \phi$ as in Eq. (1) and a set of polynomials $\mathbb {A}= \{a_1, \ldots , a_m\}$ for the abstraction. We construct a symbolic transition system of the semi-algebraic abstraction:

$$ {\widehat{S}}_{\mathbb {P}} \,\dot{=}\,\langle V_{\mathbb {P}}, {\widehat{I}}_{\mathbb {P}}(V_{\mathbb {P}}), {\widehat{T}}_{\mathbb {P}}(V_{\mathbb {P}},V'_{\mathbb {P}}) \rangle , $$

where the set of predicates of the abstraction is $\mathbb {P}= \{a \bowtie 0 \mid a \in \mathbb {A}\ \wedge \ \bowtie \in \{>,<,=\}\}$, and the set of abstract variables $V_{\mathbb {P}}$ is defined as in Sect. 3 (i.e., the abstraction contains a Boolean variable $v_p$ for each predicates $p \in \mathbb {P}$). We similarly use the formula $H_\mathbb {P}(X, V_{\mathbb {P}})$ to describe the equivalence relation of the concrete states. The formulas ${\widehat{I}}_{\mathbb {P}}(V_{\mathbb {P}})$ and ${\widehat{\lnot P}}_{\mathbb {P}}(V_{\mathbb {P}})$ are the semi-algebraic abstraction of the initial states $\psi$ and of the unsafe states $\lnot \phi$:

$$ {\widehat{I}}_{\mathbb {P}}(V_{\mathbb {P}}) \,\dot{=}\,\exists X. (\psi (X) \wedge H_\mathbb {P}(X, V_{\mathbb {P}})), \qquad {\widehat{\lnot P}}_{\mathbb {P}}(V_{\mathbb {P}}) \,\dot{=}\,\exists X. (\lnot \phi (X) \wedge H_\mathbb {P}(X, V_{\mathbb {P}})), $$

and we obtain the abstraction by existentially quantifying the concrete variables X. The definition of the abstract transition relation ${\widehat{T}}_{\mathbb {P}}(V_{\mathbb {P}}, V'_{\mathbb {P}})$, which differs from the encoding of the semi-algebraic decomposition, is:

$$\begin{aligned} {\widehat{T}}_{\mathbb {P}}(V_{\mathbb {P}}, V'_{\mathbb {P}}) \,\dot{=}\,\exists X, X'. \Bigg (&N_{}({X},{X'}) \wedge H(X) \wedge H(X') \wedge \\&H_\mathbb {P}(X, V_{\mathbb {P}}) \wedge H_\mathbb {P}(X', V'_{\mathbb {P}}) \wedge \exists Z. T_{\mathbb {A}}(X,X',Z) \Bigg ), \nonumber \end{aligned}$$

(7)

where $N_{}({X},{X'})$ encodes the adjacent relation between abstract states:

$$ N_{}({X},{X'}) = \bigwedge _{a \in \mathbb {A}}{ \Big ( (a(X) < 0 \rightarrow a(X') \le 0) \wedge (a(X) > 0 \rightarrow a(X') \ge 0) \Big ), } $$

and $T_{\mathbb {A}}(X,X',Z)$ encodes the existence of a transition in the dynamical system $\boldsymbol{f}$ for each pair of abstract states $(s_1,s_2) \in 3^\mathbb {A}$:

$$\begin{aligned} T_{\mathbb {A}}(X,X',Z) \,\dot{=}\,\bigvee _{(s_1,s_2) \in 3^\mathbb {A}}{ \Big ( s_1(X) \wedge s_2(X') \wedge \lnot \textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)} \Big ). } \end{aligned}$$

(8)

Theorem 1

The transition systems $S_{\mathbb {A}}$ and ${\widehat{S}}_{\mathbb {P}}$ are bisimilar.

Corollary 1

${\widehat{S}}_{\mathbb {P}} \models \lnot {\widehat{\lnot P}}_{\mathbb {P}}(V_{\mathbb {P}})$ implies $\psi \rightarrow [\boldsymbol{\dot{X}} = \boldsymbol{f}(\boldsymbol{X})\ \& \ H] \phi$.

Proof

(sketch). The proof follows directly from Theorem 1.    $\square$

While the encoding of the transition relation ${\widehat{T}}_{\mathbb {P}}(V_{\mathbb {P}}, V'_{\mathbb {P}})$ is symbolic, it (and in particular the sub-formula $T_{\mathbb {A}}(X,X',Z)$) explicitly enumerates an exponential number of abstract pairs of states. Clearly, this encoding is not practical and defeats the purpose of using symbolic techniques to compute the abstraction.

5 Linear Encoding of the Semi-Algebraic Abstraction

Specializing the LZZ Formula for Checking Abstract Transitions

The construction of the semi-algebraic abstraction uses the formula $\lnot \textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)}$ to encode the existence of a transition from the abstract state $s_1$ to the abstract state $s_2$. We observe that here the LZZ algorithm is applied to formulas with a specific structure – the abstract states $s_1(Z)$ and $s_2(Z)$, in contrast to arbitrary semi-algebraic sets as in the general case of $\textit{LZZ}_{{\theta },{\boldsymbol{f}},{H}}{(X)}$ where the formulas $\theta$ and H are in DNF. Instead, in the case of $\textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)}$, each abstract state $s_i(X)$ assigns a sign to each polynomial $a \in \mathbb {A}$ and is represented as conjunctions of predicates $s_i = a_1 \bowtie _1 0 \wedge a_2 \bowtie _2 0 \wedge \ldots a_m \bowtie _m 0$, where $\bowtie _j \in \{>,<,=\}$. We will write the conjunction representing a state $s_i(X)$ as $\bigwedge _{a \bowtie 0 \in s_i}{a(X) \bowtie 0}$. Also note that the evolution domain constraints are also a disjunction of two abstract states $s_1 \vee s_2$.

We specialize Eq. (2) to the specific case of $\textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)}$. We will use such specialization to obtain a compact (linear in the number of polynomials) encoding later in the section. Instantiating the formula (2) to the case of $\textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)}$, we get:

$$\begin{aligned}&\textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)} \,\dot{=}\,\nonumber \\&\qquad ( (s_1(Z) \wedge (s_1(Z) \vee s_2(Z)) \wedge \textit{In}_{{\boldsymbol{f}},{s_1 \vee s_2}}({Z})) \rightarrow \textit{In}_{{\boldsymbol{f}},{s_1}}({Z})) \wedge \end{aligned}$$

(9)

$$\begin{aligned}&\qquad ( (\lnot s_1(Z) \wedge (s_1(Z) \vee s_2(Z)) \wedge \textit{In}_{-{\boldsymbol{f}},{s_1 \vee s_2}}({Z}) ) \rightarrow \lnot \textit{In}_{-{\boldsymbol{f}},{s_1}}({Z})) \nonumber \\&\text {Applying the Boolean identities: } (\alpha \wedge (\alpha \vee \beta )) \leftrightarrow \alpha , \quad (\lnot \alpha \wedge (\alpha \vee \beta )) \leftrightarrow \lnot \alpha \wedge \beta \nonumber \\&\,\,\Longleftrightarrow ( (s_1(Z) \wedge \textit{In}_{{\boldsymbol{f}},{s_1 \vee s_2}}({Z})) \rightarrow \textit{In}_{{\boldsymbol{f}},{s_1}}({Z})) \wedge \end{aligned}$$

(10)

$$\begin{aligned}&\qquad \,\,\,\, ( (\lnot s_1(Z) \wedge s_2(Z) \wedge \textit{In}_{-{\boldsymbol{f}},{s_1 \vee s_2}}({Z}) ) \rightarrow \lnot \textit{In}_{-{\boldsymbol{f}},{s_1}}({Z})) \nonumber \\&\text {Rewriting the implication and applying De Morgan's laws: } \nonumber \\&\,\,\,\Longleftrightarrow ( \lnot s_1(Z) \vee \lnot \textit{In}_{{\boldsymbol{f}},{s_1 \vee s_2}}({Z}) \vee \textit{In}_{{\boldsymbol{f}},{s_1}}({Z})) \wedge \end{aligned}$$

(11)

$$\begin{aligned}&\qquad \,\,\,\,\, ( s_1(Z) \vee \lnot s_2(Z) \vee \lnot \textit{In}_{-{\boldsymbol{f}},{s_1 \vee s_2}}({Z}) \vee \lnot \textit{In}_{-{\boldsymbol{f}},{s_1}}({Z})) \nonumber \\&\begin{aligned} \text {Expanding the definition of}\,In (Eq.~(3)):&\textit{In}_{{\boldsymbol{f}},{\alpha \vee \beta }}{} \,\dot{=}\,(\textit{In}_{-{\boldsymbol{f}},{\alpha }}{} \vee \textit{In}_{{\boldsymbol{f}},{\beta }}{})\\&\textit{In}_{-{\boldsymbol{f}},{\alpha \vee \beta }}{} \,\dot{=}\,(\textit{In}_{-{\boldsymbol{f}},{\alpha }}{} \vee \textit{In}_{-{\boldsymbol{f}},{\beta }}{}) \end{aligned} \nonumber \\&\,\,\,\Longleftrightarrow ( \lnot s_1(Z) \vee \lnot (\textit{In}_{{\boldsymbol{f}},{s_1}}({Z}) \vee \textit{In}_{{\boldsymbol{f}},{s_2}}({Z})) \vee \textit{In}_{{\boldsymbol{f}},{s_1}}({Z})) \wedge \\&\qquad \,\,\,\,\, ( s_1(Z) \vee \lnot s_2(Z) \vee \lnot (\textit{In}_{-{\boldsymbol{f}},{s_1}}({Z}) \vee \textit{In}_{-{\boldsymbol{f}},{s_2}}({Z})) \vee \lnot \textit{In}_{-{\boldsymbol{f}},{s_1}}({Z})) \nonumber \\&\begin{aligned} \text {Applying the Boolean identities: }&(\lnot (\alpha \vee \beta ) \vee \alpha ) \leftrightarrow (\lnot \beta \vee \alpha ), (\lnot (\alpha \vee \beta ) \vee \lnot \alpha ) \leftrightarrow \lnot \alpha \end{aligned} \nonumber \\&\,\,\,\Longleftrightarrow (\lnot s_1(Z) \vee \lnot \textit{In}_{{\boldsymbol{f}},{s_2}}({Z}) \vee \textit{In}_{{\boldsymbol{f}},{s_1}}({Z})) \wedge \\&(s_1(Z) \vee \lnot s_2(Z) \vee \lnot \textit{In}_{-{\boldsymbol{f}},{s_1}}({Z})). \nonumber \end{aligned}$$

(12)

Note that, while In does not distribute over arbitrary Boolean formulas (see [12]), when we expand the definition of $In_{\boldsymbol{f},s_1 \vee s_2}$ (Eq. (12)), the formula $s_1 \vee s_2$ is in DNF. Thus, Formula (13) is equivalent to the initial Formula (9) of $\textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)}$. We then write the negation of the Formula 13 as:

$$\begin{aligned} \lnot \textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)} \,\dot{=}\,&(s_1(Z) \wedge \textit{In}_{{\boldsymbol{f}},{s_2}}({Z}) \wedge \lnot \textit{In}_{{\boldsymbol{f}},{s_1}}({Z})) \vee \end{aligned}$$

(13)

$$\begin{aligned}&(\lnot s_1(Z) \wedge s_2(Z) \wedge \textit{In}_{-{\boldsymbol{f}},{s_1}}({Z})). \nonumber \end{aligned}$$

(14)

Linear Encoding of the Semi-Algebraic Transition Relation

In the following steps, we revise the formula $T_{\mathbb {A}}(X,X',Z)$ that encodes the existence of the transitions in the abstraction, still enumerating all possible pairs of states, using the specialized LZZ encoding from Eq. (14). We substitute the subformula $\lnot \textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)}$ with the specialized LZZ encoding (Eq. (16)); we then distribute the conjunction $s_1(X) \wedge s_2(X')$ over the disjunction present in the definition of $\lnot \textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)}$ (Eq. (17)), and then over possible pairs of states (Eq. (18)). We rename the two disjuncts in Eq. (18) as $\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$ and $\textit{OutExpl}_{{\boldsymbol{f}}}({X},{X'},{Z}))$ (Eq. (19)). The formulas $\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$ and $\textit{OutExpl}_{{\boldsymbol{f}}}({X},{X'},{Z}))$ still enumerate explicitly the abstract states. However, each of these formulas is a conjunction of predicates, application of the $In_{\boldsymbol{f}}$ operator to a conjunction of predicates, and negations of the application of $In_{\boldsymbol{f}}$.

$$\begin{aligned}&T_{\mathbb {A}}(X,X',Z) \,\dot{=}\,\nonumber \\&\qquad \exists Z. \bigvee _{(s_1,s_2) \in 3^\mathbb {A}}{ ( s_1(X) \wedge s_2(X') \wedge \lnot \textit{LZZ}_{{s_1},{\boldsymbol{f}},{s_1 \vee s_2}}{(Z)} ) }\end{aligned}$$

(15)

$$\begin{aligned}&\Longleftrightarrow \exists Z. \bigvee _{(s_1,s_2) \in 3^\mathbb {A}}{ \Bigg ( \begin{aligned} s_1(X) \wedge s_2(X') \wedge (&(s_1(Z) \wedge \textit{In}_{{\boldsymbol{f}},{s_2}}({Z}) \wedge \lnot \textit{In}_{{\boldsymbol{f}},{s_1}}({Z})) \vee \\&(\lnot s_1(Z) \wedge s_2(Z) \wedge \textit{In}_{-{\boldsymbol{f}},{s_1}}({Z}))) \end{aligned} \Bigg ) } \end{aligned}$$

(16)

$$\begin{aligned}&\Longleftrightarrow \exists Z. \bigvee _{(s_1,s_2) \in 3^\mathbb {A}}{ \Bigg ( \begin{aligned} (s_1(X) \wedge s_2(X') \wedge s_1(Z) \wedge \textit{In}_{{\boldsymbol{f}},{s_2}}({Z}) \wedge \lnot \textit{In}_{{\boldsymbol{f}},{s_1}}({Z})) \vee \\ ((s_1(X) \wedge s_2(X') \wedge \lnot s_1(Z) \wedge s_2(Z) \wedge \textit{In}_{-{\boldsymbol{f}},{s_1}}({Z})) \end{aligned} \Bigg ) } \end{aligned}$$

(17)

$$\begin{aligned}&\Longleftrightarrow \exists Z. \Bigg ( \begin{array}{c} \bigvee _{(s_1,s_2) \in 3^\mathbb {A}}{ ( s_1(X) \wedge s_2(X') \wedge s_1 \wedge \textit{In}_{{\boldsymbol{f}},{s_2}}({Z}) \wedge \lnot \textit{In}_{{\boldsymbol{f}},{s_1}}({Z}) ) } \vee \\ \bigvee _{(s_1,s_2) \in 3^\mathbb {A}}{ ( s_1(X) \wedge s_2(X') \wedge \lnot s_1 \wedge s_2 \wedge \textit{In}_{-{\boldsymbol{f}},{s_1}}({Z}) ) } \end{array} \Bigg ) \end{aligned}$$

(18)

$$\begin{aligned}&\Longleftrightarrow \exists Z. (\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z}) \vee \textit{OutExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})). \end{aligned}$$

(19)

We now show how we obtain a formula $\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$ with a linear size. We expand the definition of the formula $\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$ with respect to the predicates in $s_1$ and $s_2$. Recall that each abstract state is a conjunction of predicates obtained from the set of polynomial $\mathbb {A}$ (i.e., $s \,\dot{=}\,\bigwedge _{a \in \mathbb {A}}{a \bowtie _a 0}$, $\bowtie _a \in \{>,<,=\}$) and that we use $a \bowtie 0 \in s$ to enumerate the predicates in s.

$$\begin{aligned} \textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z}) \,\dot{=}\,&\bigvee _{s_1,s_2 \in 3^{\mathbb {A}}}{} \Bigg ( \Bigg .&\bigwedge _{a \bowtie 0 \in s_1}{a(X) \bowtie 0} \wedge \bigwedge _{a \bowtie 0 \in s_2}{a(X') \bowtie 0} \wedge \\&\bigwedge _{a \bowtie 0 \in s_1}{a(Z) \bowtie 0} \wedge \bigwedge _{a \bowtie 0 \in s_2}{\textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})} \wedge \nonumber \\&\bigvee _{a \bowtie 0 \in s_1}{\lnot \textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})} \Bigg . \Bigg ). \nonumber \end{aligned}$$

(20)

In the above formula, we used De Morgan rules to rewrite the formula $\lnot \bigwedge _{a \bowtie 0 \in s_1}{\textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})}$ as the formula $\bigvee _{a \bowtie 0 \in s_1}{\lnot \textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})}$. We express the formula $\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$ as an enumeration of the predicates, over the variables X and $X'$, determining the abstract states $s_1$ and $s_2$, instead of the pairs of abstract states:

$$\begin{aligned} \textit{InsSymb}_{{\boldsymbol{f}}}({X},{X'},{Z}) \,\dot{=}\,&\bigwedge _{a \in \mathbb {A}, \bowtie \in \{>,<,=\}}{\Big (a(X) \bowtie 0 \rightarrow a(Z) \bowtie 0 \Big )} \wedge \\&\bigwedge _{a \in \mathbb {A}, \bowtie \in \{>,<,=\}}{\Big (a(X') \bowtie 0 \rightarrow \textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})\Big )} \wedge \nonumber \\&\bigvee _{a \in \mathbb {A}, \bowtie \in \{>,<,=\}}{ \Big (a(X) \bowtie 0 \wedge (\lnot \textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})) \Big )}. \nonumber \end{aligned}$$

(21)

Lemma 1

$\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$ and $\textit{InsSymb}_{{\boldsymbol{f}}}({X},{X'},{Z})$ are equivalent.

Proof

(sketch).

$\Rightarrow$) We show that $\mu \models \textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$ implies $\mu \models \textit{InsSymb}_{{\boldsymbol{f}}}({X},{X'},{Z})$. Since $\mu \models \textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$ we have that $\mu$ is an interpretation for one of the disjuncts on the possible pairs of states of $\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$:

$$\begin{aligned}&\bigwedge _{a \bowtie 0 \in s_1}{a(X) \bowtie 0} \wedge \bigwedge _{a \bowtie 0 \in s_2}{a(X') \bowtie 0} \wedge \bigwedge _{a \bowtie 0 \in s_1}{a(Z) \bowtie 0} \wedge \\&\bigwedge _{a \bowtie 0 \in s_2}{\textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})} \wedge \bigvee _{a \bowtie 0 \in s_1}{\lnot \textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})}. \end{aligned}$$

Hence, there exist two (and exactly two) abstract states $s_1,s_2$, such that $\mu \models s_1(X)$ and $\mu \models s_2(X')$. This means that any predicate $a \bowtie 0 \not \in s_1$ is such that $\mu \not \models a \bowtie (X)$ and similarly for predicates not in the state $s_2$ for the variables $X'$ (recall that, given a polynomial $a \in \mathbb {A}$, the possible abstraction predicates $a > 0$, $a < 0$, and $a = 0$ are mutually exclusive). We show that $\mu$ is an interpretation for all the conjuncts in $\textit{InsSymb}_{{\boldsymbol{f}}}({X},{X'},{Z})$. We have that $\mu \models \bigwedge _{a \in \mathbb {A}, \bowtie \in \{>,<,=\}}{\Big (a(X) \bowtie 0 \rightarrow a(Z) \bowtie 0 \Big )}$ since for all $a \in \mathbb {A}$, $\mu \models a(X) \bowtie 0 \rightarrow a(Z) \bowtie 0$ (when $a \in s_1$ we have $\mu \models a(Z) \bowtie 0$, while when $a \not \in s_1$ the implication trivially holds). Similarly, this happens for $\bigwedge _{a \in \mathbb {A}, \bowtie \in \{>,<,=\}}{\Big (a(X) \bowtie 0 \rightarrow a(Z) \bowtie 0 \Big )}$. We can see the disjunction: $\bigvee _{a \in \mathbb {A}, \bowtie \in \{>,<,=\}}{ \Big (a(X) \bowtie 0 \wedge (\lnot \textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})) \Big )}$ as:

$$\begin{aligned} \bigvee _{a \bowtie 0 \in s_1}{ \Big (a(X) \bowtie 0 \wedge (\lnot \textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})) \Big )} \vee \bigvee _{a \bowtie 0 \not \in s_1}{ \Big (a(X) \bowtie 0 \wedge (\lnot \textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})) \Big )}. \end{aligned}$$

We have that $\mu$ satisfies the first disjunct (and hence the whole disjunction) because when $a \bowtie 0 \in s_1$ we have that $\mu \models \bigvee _{a \bowtie 0 \in s_1}{\lnot \textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})}$.

$\Leftarrow$) We show that $\mu \models \textit{InsSymb}_{{\boldsymbol{f}}}({X},{X'},{Z})$ implies $\mu \models \textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$. As before, we notice that are only two predicates $s_1,s_2$ such that $\mu \models s_1(X)$ and $\mu \models s_2(X')$ and that all the predicates not in $s_1$ and not in $s_2$ do not hold in $\mu$. Thus, from $\mu \models \textit{InsSymb}_{{\boldsymbol{f}}}({X},{X'},{Z})$ we have that

$$\begin{aligned} \mu \models \bigwedge _{a \in s_1}{a(Z) \bowtie 0} \wedge \bigwedge _{a \in s_2}{\textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})} \wedge \bigvee _{a \in s_1}{\lnot \textit{In}_{{\boldsymbol{f}},{a \bowtie 0}}({Z})}. \end{aligned}$$

Hence, $\mu$ is a model for at least one of the disjuncts in $\textit{InsExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$.    $\square$

We similarly define the compact encoding of $\textit{OutExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$:

$$\begin{aligned} \textit{OutSymb}_{{\boldsymbol{f}}}({X},{X'},{Z}) \,\dot{=}\,&\bigwedge _{a \in \mathbb {A}, \bowtie \in \{>,<,=\}}{\Big (a(X) \bowtie 0 \rightarrow \textit{In}_{-{\boldsymbol{f}},{a \bowtie 0}}({Z}) \Big )} \wedge \\&\bigwedge _{a \in \mathbb {A}, \bowtie \in \{>,<,=\}}{\Big (a(X') \bowtie 0 \rightarrow a(Z) \bowtie 0\Big )} \wedge \nonumber \nonumber \\&\bigvee _{a \in \mathbb {A}, \bowtie \in \{>,<,=\}}{ \Big (a(X) \bowtie 0 \wedge \lnot a(Z) \bowtie 0 \Big )}. \nonumber \end{aligned}$$

(22)

Lemma 2

$\textit{OutExpl}_{{\boldsymbol{f}}}({X},{X'},{Z})$ and $\textit{OutSymb}_{{\boldsymbol{f}}}({X},{X'},{Z})$ are equivalent.

Proof

The proof of Lemma 2 is similar to the proof of Lemma 1.    $\square$

We now express the transition relation from Eq. (7) in a compact form:

$$\begin{aligned} {\widehat{T_{\textit{Symb}}}}_{\mathbb {P}}(V_{\mathbb {P}}, V'_{\mathbb {P}}) \,\dot{=}\,\exists X, X'. \Bigg (&N_{}({X},{X'}) \wedge H(X) \wedge H(X') \wedge&\\&H_\mathbb {A}(X, V_{\mathbb {P}}) \wedge H_\mathbb {A}(X', V'_{\mathbb {P}}) \wedge&\nonumber \\&\exists Z. ( \textit{InsSymb}_{{\boldsymbol{f}}}({X},{X'},{Z}) \vee \textit{OutSymb}_{{\boldsymbol{f}}}({X},{X'},{Z}) ) \Bigg ).&\nonumber \end{aligned}$$

(23)

Theorem 2

${\widehat{T}}_{\mathbb {P}}(V_{\mathbb {P}}, V'_{\mathbb {P}})$ and ${\widehat{T_{\textit{Symb}}}}_{\mathbb {P}}(V_{\mathbb {P}}, V'_{\mathbb {P}})$ are equivalent.

Proof

Follows directly from Lemma 2 and Lemma 1.    $\square$

Implicit Semi-Algebraic Abstraction

The formula ${\widehat{T_{\textit{Symb}}}}_{\mathbb {P}}(V_{\mathbb {P}}, V'_{\mathbb {A}})$ represents the transition relation of the semi-algebraic abstraction. Computing the finite-state transition system representing the semi-algebraic abstraction requires to eliminate the existential quantifiers from the initial states, transition relation, and safety property formulas. However, the above formula ${\widehat{T_{\textit{Symb}}}}_{\mathbb {P}}(V_{\mathbb {P}}, V'_{\mathbb {A}})$ contains non-linear real arithmetic terms from the polynomials and the Lie derivatives we compute in $In_{\boldsymbol{f}}$, so removing the quantifiers from the formula requires to apply a quantifier elimination algorithm (e.g., Cylindrical Algebraic Decomposition [8]) that does not scale, even when the number of polynomials is small. Instead, we construct a symbolic transition system that implicitly encodes the abstraction:

$$\begin{aligned} S_{\textit{Impl},\mathbb {P}} \,\dot{=}\,\langle&X \cup \overline{X}\cup Z, \psi (X) \wedge \textit{EQ}_{\mathbb {P}}(X,\overline{X}), T_{\textit{Impl},\mathbb {P}}(\overline{X},{X}',Z) \wedge \textit{EQ}_{\mathbb {P}}(X',\overline{X'}) \rangle , \end{aligned}$$

where

$$\begin{aligned} T_{\textit{Impl},\mathbb {P}}(\overline{X},X',Z) \,\dot{=}\,&N_{}({\overline{X}},{X'}) \wedge H(\overline{X}) \wedge H(X') \wedge&\\&( \textit{InsSymb}_{{\boldsymbol{f}}}({\overline{X}},{X'},{Z}) \vee \textit{OutSymb}_{{\boldsymbol{f}}}({\overline{X}},{X'},{Z}) ).&\nonumber \end{aligned}$$

The above encoding is a an implicit predicate abstraction [35] that preserves reachability properties and is such that:

Theorem 3

$S_{\textit{Impl},\mathbb {P}} \models P(\overline{X})$ if and only if ${\widehat{S}}_{\mathbb {P}} \models \lnot {\widehat{\lnot P}}_{\mathbb {P}}(V_{\mathbb {P}})$.

Thus, we can model check the transition system $S_{\textit{Impl},\mathbb {P}} \models P(\overline{X})$ to prove a property P holds on the dynamical system. Note that, to this purpose, we can apply standard SMT-based model checking algorithms.

The transition system $S_{\textit{Impl},\mathbb {P}}$ doubles the state space introducing a copy of the state variables $\overline{X}$ and encodes the equivalence relation between pairs of concrete states in X and in $\overline{X}$ with the formula $\textit{EQ}_{\mathbb {P}}(X,\overline{X})$ (c.f. Formula 6). The transition relation $T_{\textit{Impl},\mathbb {P}}(\overline{X},X',Z)$ then encodes a transition in the semi-algebraic abstraction with the linear encoding $\textit{InsSymb}_{{\boldsymbol{f}}}({\overline{X}},{X'},{Z})$ and $\textit{OutSymb}_{{\boldsymbol{f}}}({\overline{X}},{X'},{Z})$. In this way, a transition in the transition system $S_{\textit{Impl},\mathbb {P}}$ corresponds to a transition in the semi-algebraic abstraction, and vice-versa.

6 Experimental Evaluation

Research Questions We evaluate the performance of our approach (Implicit Abstraction) for the verification of invariant properties on the semi-algebraic abstraction of dynamical systems. Implicit Abstraction first encodes the semi-algebraic abstraction in a transition system (as we show in Sect. 5), and then model checks the invariant on the transition system with an off-the-shelf model checker. Our experiments aim to answer the following research questions:

RQ 1: How does Implicit Abstraction compare with the LazyReach algorithm [32], which explicitly enumerates the reachable states of the abstraction?

RQ 2: How does Implicit Abstraction compare with the DWCL algorithm [32], which applies a divide-and-conquer strategy to reduce the number of polynomials in the abstraction?

Experimental Setup

We implemented the construction of the implicit abstraction transition system in Python using PySMT [11] to manipulate formulas, and SymPy [23] for polynomial manipulation and Gröbner bases computation (i.e., to compute the Lie derivatives’ ranks). We verify the implicit abstraction transition system with the model checking algorithm for symbolic transition systems with NRA constraints from [4]. The algorithm abstracts the non-linear transition system into a linear transition system, which is checked by the algorithm in [6] and is implemented using the MathSAT  [7] SMT solver. We implemented both the LazyReach and the DWCL algorithms in the same Python tool. Our implementation of DWCL can use different backends to decide the satisfiability of NRA formulas, namely MathSAT⁶, the z3 SMT solver [25], or Mathematica  [17].

We consider 90 invariant verification problems for dynamical systems from the KeyMaera X theorem prover [10]. These problems are a superset of the ones used in [32] and are used in the Applied Verification of Continuous and Hybrid Systems (ARCH) competition [24]. We obtain a total of 180 benchmark instances using, for each problem, two sets of polynomials for the semi-algebraic abstraction⁷. The first set contains all the factors of the right-hand side of the ODEs; the second set extends the first one by including also the Lie derivatives of the polynomials. The latter set induces an abstraction that is more precise but also has a larger state-space.

We evaluate the performance of the algorithms Implicit Abstraction, LazyReach, and DWCL to solve the above verification problems. The underlying problem requires to decide the satisfiability of NRA formulas, and the decision procedures for this problem are efficient for different subsets of problems. For this reason we further evaluate different configurations of the LazyReach and DWCL algorithms using three different solvers for NRA formulas (MathSAT, z3, and Mathematica). Note that, while in principle, we could use multiple SMT backends also in the model checking algorithm [4] and replace the MathSAT SMT solver with another SMT solver (e.g., z3), this change would not significantly impact the overall performance, because the algorithm abstracts the non-linear formulas with linear ones where both MathSAT and z3 have comparable performance.

We run the Implicit Abstraction, LazyReach, and DWCL algorithm on all the 180 benchmark instances with a time out of 100 seconds, and we measure the execution times to either prove (safe result) or find an abstract counterexample (unknown result) for each instance. An archive containing the necessary to reproduce the experiments is available online at http://www.sergiomover.eu/cav2021.html.

Results

RQ 1 - Implicit Abstraction vs. LazyReach. From the cumulative plot in Fig. 2, we see that Implicit Abstraction almost always outperforms LazyReach.

From the cumulative plot in Fig. 2a we see that Implicit Abstraction significantly outperforms LazyReach on safe instances. For better readability, in the plot we only show the (virtual) portfolio algorithm running each configuration of LazyReach, Virtual Best LazyReach, obtained by considering the best run time among the different configurations of LazyReach using different backend solvers. Virtual Best LazyReach solves a total of 42 safe instances, while Implicit Abstraction solves 100 safe instances. The scatter plots shown in the first row of Fig. 3 confirms the same intuition (note that the safe instances represented as are mostly in the lower-right triangle of the plot).

Figure 2b shows the cumulative plot when verifying unknown instances. Note that the total number of unknown instances in the benchmarks are much smaller than the safe ones (combining the results of all the algorithms we have 123 safe instances, 19 unknown instances, and 38 still unsolved instances). From Fig. 2b, we see that the performance of Implicit Abstraction is comparable with LazyReach, solving a total of 8 instances and 11 instances respectively.

RQ 2 - Implicit Abstraction vs. DWCL. From the cumulative plots in Fig. 2, the Virtual Best DWCL solves 37 more instances than Implicit Abstraction. However, we also see from Fig. 2 that the global Virtual Best solves more instances and is faster than Virtual Best DWCL. In fact, Implicit Abstraction is orthogonal to DWCL and is comparable to DWCL when fixing either Mathematica or z3 (Implicit Abstraction solves 108 instances, DWCL Mathematica solves 109, and DWCL z3 solves 114).

The scatter plots in the second row of Fig. 3 compare Implicit Abstraction with DWCL MathSAT, DWCL Mathematica, and DWCL z3. From these plots, we see that there are several instances that are solved by only one of the two algorithms compared in each plot. While we see similar data when comparing Implicit Abstraction with Virtual Best DWCL (always in the scatter plots of Fig. 3), the number of instances solved uniquely by Implicit Abstraction seems smaller. We get a more precise picture of the complementarity of Implicit Abstraction, DWCL Mathematica, and DWCL z3 from the diagrams in Fig. 4, where we can clearly see that Implicit Abstraction is orthogonal to both DWCL Mathematica and DWCL z3. From the diagram, we see that when using a different backend (i.e., Mathematica or z3) DWCL solves a different set of instances. This difference in performance using Mathematica and z3 is not surprising since Mathematica and z3 uses different algorithms to solve formulas in NRA.

We further notice that Implicit Abstraction uses the MathSAT SMT solver in the backend, and from our experiments (see again Fig. 3) DWCL MathSAT performs quite poorly compared to both DWCL Mathematica and DWCL z3. While naively replacing MathSAT in the model checking algorithm we use [4] would not provide a significant performance improvement, it is reasonable to think that investigating a tighter integration with either z3 or Mathematica could improve the model checking performance. However, we believe this integration to be beyond the scope for this paper, where we enable the use of symbolic model checking techniques to analyze the semi-algebraic decomposition.

Fig. 2.

Plots the total number of instances (on the y axis) as a function of the cumulative time (in seconds, on the x axis) took by Implicit Abstraction, LazyReach, and DWCL to solve (a) safe and (b) unknown instances. The comparison includes the results of LazyReach and DWCL using different (MathSAT, z3, and Mathematica), as well as virtual portfolios combining the best results obtained by a given algorithm when run with multiple backends. We omit some configurations in (b) to improve readability.

7 Related Work

In this work, we focus on the (unbounded time) safety verification problem for polynomial dynamical systems. Such problem is relevant when proving safety for hybrid programs [27] with Keymaera X [10] or for hybrid CPS with the HHL Prover [36]. Our reduction to transition systems may be used as sub-procedure in both theorem provers to automate the search of a continuous invariant.

There exist different techniques to prove safety properties for polynomial dynamical systems (see e.g., [13]): barrier certificates [18, 29], first integrals [14], and Darboux Polynomials [15]. All these techniques are orthogonal to semi-algebraic abstraction, and can be used to find invariant polynomials to restrict the abstract state space. Pegasus [33] implements all the above techniques, the LazyReach, and DWCL algorithms. Our algorithm can be integrated in Pegasus. The LZZ [22] procedure has been originally proposed to synthesize a continuous invariant. Instead, we use the LZZ procedure to encode the abstract transition relation, and then we prove a safety property in the abstraction. We also provide a specialized encoding of LZZ to check the existence of abstract transitions.

The semi-algebraic abstraction [32] is a qualitative abstraction [34, 37]. In this work, we propose a different algorithm to verify semi-algebraic abstractions that allows us to explore the abstract state-space symbolically, in contrast to the LazyReach algorithm [32]. In principle, our technique is orthogonal to the DWCL algorithm [32], since we could replace LazyReach, which is used in DWCL as a sub-routine, with our approach (i.e., model check the implicit abstraction).

Fig. 3.

Scatter plots comparing the run time (in seconds) of Implicit Abstraction (on the y axis) with LazyReach (first row, on the x axis) and DWCL (second row, on the x axis). represent safe verification problems. are instances where the algorithm found an abstract counterexample. When Implicit Abstraction runs for more than the 100 s time out, we plot the instance on the vertical line marked as to, and similarly for LazyReach and DWCL on the horizontal line.

Fig. 4.

Diagrams representing the distribution of unique instances solved combining different algorithms (DWCL Mathematica, DWCL z3, and Implicit Abstraction). Each set, displayed as a dotted circle enclosed by a dotted line, represents the set of instances solved with one algorithm. The number shown in each partition is the number of instances solved uniquely by the sets forming the partition. For example, the central partition (i.e., the intersection of all the sets) of the diagram (a) shows that DWCL Mathematica, DWCL z3, and Implicit Abstraction solved the same set of 141 instances.

Relational abstraction [31] abstracts the dynamical system’s trajectories with a discrete transition relation, reducing the verification problem on the continuous system to a verification problem on the discrete system. The implicit encoding of the semi-algebraic abstraction can be seen as an instance of relational abstraction, where a trajectory of the dynamical system is mapped to a sequence of abstract transitions (similarly to what happen with relational abstractions for time-sampled systems in [2, 38]). Since relational abstractions can be composed with each other (e.g., see [26]), we can strengthen the implicit semi-algebraic abstraction encoding with a relational abstraction. This composition is useful in the case the semi-algebraic abstraction cannot easily capture the system’s behavior (e.g., a precise relation of the time elapsed in a transition [26]).

Predicate abstraction [16] is a commonly used abstraction techniques to verify infinite-state systems. Several symbolic techniques [3, 19, 20] focus on the efficient computation of the predicate abstraction. In principle, we can also use those technique to explicitly compute the semi-algebraic abstraction. However, the up-front, explicit computation of the abstraction is a bottleneck and can be avoided with implicit predicate abstraction [35] when the goal is to verify a safety property on the abstract system. We use implicit abstraction to obtain an implicit encoding of the semi-algebraic abstraction. The transition system of the semi-algebraic abstraction contains NRA formulas (the polynomials can be non-linear or the Lie derivative of the polynomials are non-linear). While there are few algorithms and tool that can verify such transition systems (e.g., [4]), our technique is agnostic to the underlying model checking algorithm.

8 Conclusions and Future Work

In this paper, we addressed the safety problem of polynomial dynamical systems. We built on the LZZ algorithm to define a symbolic encoding of the abstraction based on a set of polynomials. The encoding is linear in the number of polynomials and can be used to implicitly represent the abstraction without the need of enumerating the abstract states, enabling the use of SMT-based model checking techniques. The experimental evaluation showed that the approach is promising and complementary to existing techniques solving a number of new instances.

The main directions for future works are, on one side, refining the abstraction discovering new polynomials that are able to remove spurious abstract counterexamples, and, on the other side, the application of the approach to hybrid systems where the continuous dynamics depends on the discrete state of the system.