Keywords

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

Hybrid automata is a modeling formalism in which discrete transitions and continuous evolution can be intermixed to describe fairly complex cyber-physical systems. HybridSal [15] is a tool for performing verification of hybrid automata models [2, 3, 5, 6, 8, 9, 11, 14, 16]. It is a tool built over the SAL tool [7] that can be used to model and verify discrete (finite or infinite) state transition systems. The core component of HybridSal is an abstraction engine that takes a hybrid model and outputs a discrete (SAL) model that is a sound abstraction of the hybrid model [13]. The abstract SAL model can be analyzed using the usual SAL model checking tools (such as the infinite bounded model checker or the k-induction prover).

In this paper, we revisit the relational abstraction technique [13] and its improvement to time-aware relational abstraction [10], which are both available in the current version of HybridSal [15]. We identify a class of problems for which these techniques yield very coarse abstractions, and present an approach to fix this shortcoming. The approach is based on creating sound approximations of nonlinear functions using sound approximations of the natural logarithm (\(\ln \)) function. We present examples that can be verified using the new approach that could not be verified previously by HybridSal.

2 Relational Abstraction

The HybridSal abstraction engine constructs a so-called relational abstraction of the system. A relational abstraction does not abstract the state space of the system, but only over-approximates the transition relation [13]. Concretely, the relational abstraction of a transition system \((S,\rightarrow )\) (with state space S and transition relation \(\rightarrow \)) is another transition system \((S,\rightarrow ^a)\) such that \(\rightarrow \;\subseteq \;\rightarrow ^a\).

The semantics of a hybrid system is given as a state transition system \((S,\rightarrow _d\cup \rightarrow _c)\), where \(\rightarrow _d\) are transitions that capture the “discrete” behavior of the system, and \(\rightarrow _c\) are transitions that capture the “continuous” behavior. The HybridSal tool constructs relational abstraction of hybrid systems by abstracting only the relation \(\rightarrow _c\); that is, the abstract system is \((S, \rightarrow _d\cup \rightarrow _c^a)\). We next briefly describe the relations \(\rightarrow _c\) and \(\rightarrow _c^a\).

The continuous behavior of a hybrid system is typically specified using ordinary differential equations. Consider a system of differential equations, \(d{\varvec{x}}/dt = f(x)\), whose dynamics are constrained to remain within invariant \({\mathtt{Inv }}\). The concrete semantics of this continuous behavior is defined by the relation \(\rightarrow _c\):

$$\begin{aligned} {\varvec{x}}_\mathbf{1} \rightarrow _c {\varvec{x}}_\mathbf{2} \text{ if }&\exists {F}:\exists {(t\ge 0)}: {\varvec{x}}_\mathbf{1} = F(0), {{\varvec{x}}} _\mathbf{{2}} = F(t), dF/dt = f(F(t)), \nonumber \\&\forall {(0\le t'\le t)}: F(t')\in {\mathtt{Inv }} \end{aligned}$$
(1)

Here, the function F is a solution of the differential equations [1].

It is extremely difficult to reason with the relation in Eq. 1. Relational abstraction overcomes this problem by constructing an over-approximation of this relation that is much easier to analyze. Henceforth, let us assume that continuous dynamics are specified using linear ordinary differential equations; for simplicity, say \(d{\varvec{x}}/dt = A{\varvec{x}}\), where A is an \(n\times n\) matrix.

2.1 Time-Oblivious Relational Abstraction

A relational abstraction that does not mention the time variable, t, explicitly is called a time-oblivious relational abstraction. By default, HybridSal constructs time-oblivious abstractions [15]. If \({\varvec{c}}^T\) is a left-eigenvector of A corresponding to eigenvalue \(\lambda \), then it is easily proved that if \({\varvec{x}}\rightarrow _c{\varvec{x'}}\), then

$$\begin{aligned} {\varvec{c}}^T{\varvec{x'}}= & {} {\varvec{c}}^T{\varvec{x}}{\mathrm {e}}^{\lambda (t'-t)} \end{aligned}$$
(2)

When \(\lambda > 0\), we can over-approximate the relationship between \({\varvec{x}}\) and \({\varvec{x'}}\) in the form of the following time-oblivious abstraction:

$$\begin{aligned} ({\varvec{c}}^T{\varvec{x'}} = {\varvec{c}}^T{\varvec{x}} = 0) \vee ({\varvec{c}}^T{\varvec{x'}} \ge {\varvec{c}}^T{\varvec{x}} > 0) \vee ({\varvec{c}}^T{\varvec{x'}} \le {\varvec{c}}^T{\varvec{x}} < 0) \end{aligned}$$
(3)

Note there is no mention of the time elapsed (\(t'-t\)) in the above expression. Furthermore, all expressions above are linear. Each left eigenvector of A corresponding to a real eigenvalue will generate one constraint of the form in Eq. 3. If the eigenvalue \(\lambda \) has a nonzero imaginary part, we can still get a piecewise linear time-oblivious relational abstraction on the real and imaginary parts of the corresponding eigenvector [15].

There are two shortcomings in the time-oblivious abstraction computed above. First, it is too coarse. It loses all time-related information. For example, if we have a 2-d system \(dx/dt = -x, dy/dt = -y\), the time-oblivious abstraction forgets that the (exponential) decay rates of x and y are the same. Second, if matrix A is defective, that is, it has fewer eigenvectors corresponding to eigenvalue \(\lambda \) than the algebraic multiplicity of \(\lambda \), then we do not even know how to construct a reasonably good time-oblivious abstraction.

As an example, consider the 2-d system \(dx/dt = x+y, dy/dt = y\). The corresponding matrix \(A = [1,1;0,1]\) is defective – it has eigenvalue 1 with multiplicity 2, but there is only one associated left eigenvector [0,1]. The solution of the ODE is given by the equations:

$$\begin{aligned} y(t) = y(0){\mathrm {e}}^{t}, \;\; x(t) = x(0){\mathrm {e}}^{t} + y(0)t{\mathrm {e}}^{t} \end{aligned}$$
(4)

The default time-oblivious relational abstraction constructed by HybridSal would just have inequalities (as in Eq. 3) for y(t), but x(t) would be unconstrained. This is because HybridSal lacked a general technique for handling defective A matrices.

2.2 Time-Aware Relational Abstraction

The first shortcoming of the time-oblivious abstraction computed by HybridSal was recently recognized and it resulted in the introduction of time-aware relational abstractions [10].

A time-aware relational abstraction relates the change in the value of an expression to the time elapsed. It can be more precise than a time-oblivious abstraction. Consider the exponentially increasing/decaying expression in Eq. 2 constructed from the left eigenvector \({\varvec{c}}^T\) corresponding to a real eigenvalue \(\lambda \). Taking the natural logarithm on both sides of Eq. 2, we get

$$\begin{aligned} \ln ({\varvec{c}}^T{\varvec{x'}})= & {} \ln ({\varvec{c}}^T{\varvec{x}}) + {\lambda (t'-t)} \end{aligned}$$
(5)

The expressions \({\varvec{c}}^T{\varvec{x'}}\), \({\varvec{c}}^T{\varvec{x}}\), and \({\lambda (t'-t)}\) (for a fixed value of \(\lambda \)) are linear in the state variables \({\varvec{x}}\) and the time variable t (and their next values). So, we just need a piecewise-affine (lower and upper) approximation of the natural logarithm function \(\ln \) to construct a time-aware relational abstraction. Such an approximation exists and is shown in Fig. 1: intuitively, the upper bound \({\mathtt {\ln _{ub}}}\) is defined by first-order Taylor approximations of \(\ln \) at points \(e^{i+1}-e^i\) [4].

Using the piecewise-linear approximation functions \({\mathtt {\ln _{lb}}}\) and \({\mathtt {\ln _{ub}}}\) defined in Fig. 1, we abstract Eq. 5 using the following linear arithmetic formula:

$$\begin{aligned} {\mathtt {\ln _{lb}}}({\varvec{c}}^T{\varvec{x'}}) \le {\mathtt {\ln _{ub}}}({\varvec{c}}^T{\varvec{x}}) + {\lambda (t'-t)} \;\wedge \; {\mathtt {\ln _{ub}}}({\varvec{c}}^T{\varvec{x'}}) \ge {\mathtt {\ln _{lb}}}({\varvec{c}}^T{\varvec{x}}) + {\lambda (t'-t)} \end{aligned}$$
(6)

Since the number of intervals that define the piecewise linear approximation of the \(\ln \) function is unbounded (Fig. 1), HybridSal creates an approximation that uses only finitely many intervals: \((-\infty ,{\mathrm {e}}^{-n}]\), \([{\mathrm {e}}^m,+\infty )\), and \([{\mathrm {e}}^i,{\mathrm {e}}^{i+1}]\), \(i=-n,\ldots ,-1,0,1,\ldots ,m-1\). When creating time-aware relational abstractions in HybridSal, the precision parameters n, m are chosen by the user (via a commandline argument): picking a higher value increases precision.

Fig. 1.
figure 1

Piecewise-linear lower and upper approximation for natural logarithm function.

Full size image

The \(\ln (x)\) function in Fig. 1 is approximated by dividing the x axis into the (infinitely many) intervals \([{\mathrm {e}}^i,{\mathrm {e}}^{i+1}]\), \(i\in \mathbb {Z}\). In the interval \([e^i,e^{i+1}]\), a lower-bound, \({\mathtt {\ln _{lb}}}(x)\), for \(\ln (x)\) is given by the line joining the two end-points; that is, \({\mathtt {\ln _{lb}}}(x) := \frac{(x-e^i)}{(e^{i+1}-e^i)}+i\); whereas an upper-bound is given by \({\mathtt {\ln _{ub}}}(x) := {\mathtt {\ln _{lb}}}(x) + 0.12\). The tangents at the end-points also provide an upper-bound; hence, a better upper-bound, \({\mathtt {\ln _{ub}^{(2)}}}(x)\), is \(\min ( {\mathtt {\ln _{ub}}}(x), \frac{(x-e^i)}{e^i}+i, \frac{(x-e^{i+1})}{e^{i+1}}+i+1 )\).

Using \({\mathtt {\ln _{lb}}}\) and \({\mathtt {\ln _{ub}}}\), we know how to create time-aware abstractions for exponentially changing expressions (Eq. 2), as well as, periodically changing expressions (\(x(t) = \frac{x(0)}{\cos (\theta _0)}{\mathrm {e}}^{\lambda t} \cos (\omega t + \theta _0)\)); see [10].

2.3 Defective Matrices

If the dynamics are specified by an A matrix that is not defective, then, for an n-dimensional system, we can always find n linearly independent vectors, such that for each vector \({\varvec{c}}\), the value of the linear expression \({\varvec{c}}^T{\varvec{x}}\) is either exponentially changing or periodically changing. Hence, for such systems, we can get relatively good linear, time-aware relational abstractions.

If A is defective, then we can still find n linearly independent vectors, but now their dynamics can additionally contain terms that are “products” of exponential/trigonometric function and \(t^k\), where t is the time variable and k is some natural number. See the dynamics of x(t) in Eq. 4 for an example.

The main observation we make in this paper is that we can abstract a product of two terms by using the approximations for \(\ln \) function described above. In particular, the equation \(z = xy{\mathrm {e}}^{u}\) can be abstracted by the expression:

$$\begin{aligned}&(z=0\leftrightarrow (x=0\vee y=0)) \wedge (z>0 \leftrightarrow ((x>0\wedge y>0)\vee (x<0\wedge y<0))) \;\;\wedge \nonumber \\&{\mathtt {\ln _{lb}}}(|x|)+{\mathtt {\ln _{lb}}}(|y|)+u\le {\mathtt {\ln _{ub}}}(|z|) \wedge {\mathtt {\ln _{ub}}}(|x|)+{\mathtt {\ln _{ub}}}(|y|)+u\ge {\mathtt {\ln _{lb}}}(|z|) \end{aligned}$$
(7)

Let \(\phi (u,x,y,z)\) denote the above formula. The formula \(\phi \) contains only linear expressions, and hence we can use a linear theory solver to reason about it.

We can now use the abstraction \(\phi \) to construct abstractions of linear systems whose dynamics are specified by defective matrices. Concretely, we construct a relational abstraction of the dynamics for x(t) given in Eq. 4, namely \(x' = x{\mathrm {e}}^{t'-t}+y(t'-t){\mathrm {e}}^{t'-t}\), as follows:

$$\begin{aligned} x' = z_1 + z_2 \wedge \phi (t'-t, x, 1, z_1) \wedge \phi (t'-t, y, t'-t, z_2) \end{aligned}$$
(8)

where \(z_1,z_2\) are new variables. For an arbitrary A matrix, defective or not, we can now compute time-aware relational abstractions by first transforming A into Jordan normal form J; say \(A = U^{-1}JU\). The value of each expression \({\varvec{c}}^T{\varvec{x}}\), where \({\varvec{c}}^T\) is a row of U, is a linear combination of terms of the form \(t^k {\mathrm {e}}^{\lambda t}\) (or \(t^k\cos (bt){\mathrm {e}}^{at}\) or \(t^k\sin (bt){\mathrm {e}}^{at}\)). Thus, using \(\phi \), we can get piecewise linear abstractions for each expression by straight-forwardly extending the ideas used to construct the abstraction in Eq. 8 (and combine the ideas with [10] for periodic dynamics).

3 Experiments

Dynamics where the A matrix is defective are quite common. Some of the simplest examples turn out to have defective matrices. For example, a linear motion with constant velocity is described by \([\dot{x};\dot{v}] = A[x;v]+{\varvec{b}}\), where \(A =[0,1;0,0]\) is defective. Similarly, linear motion with constant acceleration also gives rise to defective A matrices. Even real-world examples appear to more often have defective A matrices than not. So, it was important for us to improve the quality of abstraction HybridSal generates on these dynamics.

One good verification challenge benchmark is the adaptive cruise controller from  [12]. The controller sets the acceleration of the following car, \(a_f\), as \(\dot{a_f} = -3a_f - 3(v_f - v_l) + gap - (v_f+10)\), where \(v_l,a_l\) denote the velocity and acceleration of the leading car, \(v_f,a_f\) are those of the following car, and gap is the distance between the cars. We assume that the controller is engaged whenever \(gap \ge 5, 0\le v_l,v_f\le 30\) and \(gap - 0.1 (v_f^2 - v_l^2) - 10 - (v_f-v_i)\ge 0\). We assume that \(a_l\) is an input and is constrained to be within \(-5 m/s^2\) and \(2m/s^2\), and the velocities \(v_l,v_f\) are always non-negative. The goal is to prove that after it is engaged, the controller guarantees that \(gap \ge 0\) always.

The currently released version of HybridSal, which includes an option to create time-aware relational abstraction, fails to verify the above example since it fails to use the equation \(v_l'-v_l = a_l (t'-t)\) (because the A matrix is defective). However, if we add a constraint that abstracts this equation (using the \(\phi \) formula), then HybridSal can prove safety. Even though \(a_l\) can vary arbitrarily, this equation still holds (for some \(a_l\) due to mean value theorem). Note that the quadratic term in the initial set had to be approximated by linear terms in the HybridSal model.

To further evaluate the precision of the proposed abstraction function, we also created several simple examples of linear systems whose A matrices were defective, but whose explicit solutions could be worked out by hand. For the safety property, we had an upper-bound on the value of the variable whose solution expression had the highest degree in the time variable t. Using knowledge of the explicit solution, we created initial sets and unsafe regions. We report the results in Table 1. The current version of HybridSal, of course, fails on all these examples. The new approach presented in this paper allowed us to prove conservative bounds in each case. In Table 1, Column true bnd. contains the true bound (computed by hand using the analytical solution), Column proved/CE is the bound that our approach was able to prove, followed by a bound that yielded a (spurious) counter-example. Column time reports the time it took the SMT solver (Yices) to prove the bound in Column proved/CE, followed by the time it took Yices to find a counter-example for the second bound in Column proved/CE.

Table 1. Experimental results: All six examples have 1 jordan block in the A matrix. For each example, Column #vars denotes the number of state variables, \(\lambda \) is the eigenvalue(s), alg. mult. is the (sum of) algebraic multiplicity of the eigenvalue(s), #evecs is the number of eigenvectors, true bnd. is the true upper bound (analytically calculated) for the “top” variable, proved/CE is the bound proved by the tool followed by the bound that generated a (spurious) counter-example, and time is the time (in seconds) taken by Yices to prove/generate a counter-example. The last two columns report the same results, but using a refined upper bound for \(\ln \) function.
Full size table

To further validate the claim that the sound approximations for \(\ln \) are the key, we used a slightly better (refined) upper-bound, \({\mathtt {\ln _{ub}^{(2)}}}\) defined in Fig. 1, for \(\ln \) function and re-ran the experiments, and in each case, the tool proved a tighter safety property than before (last two columns in Table 1). As expected, using the refined approximation caused Yices to take more time. The tool and examples are all available from the HybridSal webpage [15].

We note that on examples that contain only non-defective matrices, there is no overhead added by our new extension: the piecewise-linear approximation of product terms is not triggered and the new approach becomes identical to the old [10]. We also note that for matrices that have large eigenvalues, we may need to create a more precise abstraction by choosing large values for the precision parameters. Consequently, the cost of analysis (model checking) increases for such examples. In future work, we plan to address this issue.

4 Conclusion

We presented an approach for improving the time-aware relational abstraction that is currently computed by the HybridSal tool. In particular, we improved the precision of the abstraction for linear systems whose A matrices are defective. We showed that the new approach enables HybridSal to prove correctness of systems that could not be proved correct using an approach that performed coarse abstraction for defective A matrices. This extension is significant since defective matrices occur frequently in models of real systems.