1 Introduction

Embedded control systems combine computer software with the physical world, and their global behavior can be modeled using hybrid systems. To assert correctness of such systems, their global behavior under all possible nondeterminism resulting from the interaction between continuous and discrete dynamics should be accurately analyzed. Thus, one of the key ingredients for safe design and verification of embedded control systems is a set representation which, on one hand, is expressive enough to describe the evolution of sets of hybrid trajectories and, on the other hand, can be manipulated by time-efficient algorithms. For most hybrid systems with nontrivial continuous dynamics, exact computation of hybrid trajectories is impossible, so the focus is put on approximate computation of reachable states. In the area of abstract interpretation within program verification, there is a similar need for data structures for set manipulation, called abstract domains, which should be fine-grained enough to be accurate, yet computationally tractable to deal with complex programs.

Two classical abstract domains are intervals [12] and convex polyhedra [13], and their variants have been developed to achieve a good compomise between computational speed and precision, such as zones [28], octagons [29], linear templates [35], zonotopes [19], and tropical polyhedra [4]. For hybrid model checking, convex polyhedra and their special classes such as parallelotopes and zonotopes are also among popular set representations. Beyond polyhedral set representations, ellipsoids can be used for reachable set computations [27]. In abstract interpretation, polynomial inequalities are used for invariant computation via their reduction to linear inequalities in [7] and polynomial equalities via Gröner basis methods [34]. Quadratic templates are also proposed, where semi-definite relaxations are used for deriving nonlinear invariants (for instance quadratic invariants inspired by Lyapunov functions) [2, 15]. Recently, complex zonotopes [1] extended usual zonotopes to the complex domain, which geometrically speaking are Minkowski sum of line segments and some ellipsoids. Other extensions of zonotopes, such as quadratic [3] and more general polynomial zonotopes [6] have been proposed. Complex zonotopes are however different from polynomial zonotopes because while a polynomial zonotope is a set-valued polynomial function of intervals, a complex zonotope is a set-valued function of unit circles in the complex plane.

Complex zonotopes can utilize the possibly complex eigenstructure of the dynamics of linear impulsive systems to define contractive sets for stability verification. This is an advantage over polytopes or usual zonotopes that can only utilize the real eigenstructure but not the complex eigenstructure. For stability verification of nearly periodic linear impulsive systems, complex zonotopes demonstrated good accuracy on some benchmark examples. However, a drawback of complex zonotopes is that adding more generators to it can violate the property of contraction with respect to the dynamics. Therefore, it is not easy to refine complex zonotopes for verifying stability for larger intervals of sampling times. Moreover, we had to heuristically guess a suitable complex zonotope for stability verification instead of systematically synthesizing it.

Overcoming the aforementioned drawback, in this paper, we introduce a more general set representation called template complex zonotopes. In a template complex zonotope, the bounds on the complex combining coefficients, called scaling factors, are treated as variables, while the directions for the generators are fixed a priori by a template of complex vectors. This allows us to systematically synthesize a suitable template complex zonotope for stability verification, instead of guessing it like in the case of complex zonotopes. Furthermore, template complex zonotopes can be refined easily by adding any arbitrary set of vectors to the existing template, because the scaling factors can be adjusted accordingly. We present experiments on some benchmark examples where template complex zonotopes contract faster than complex zonotopes, resulting in faster verification.

Basic notation. We represent integers by \(\mathbb {Z}\), real numbers by \(\mathbb {R}\) and complex numbers by \(\mathbb {C}\). For integers p and q, the set of \(p\times q\) matrices with entries drawn from a set \(\varPsi \) is denoted \(\mathbb {M}_{p\times q}(\varPsi )\). If z is a vector of complex numbers, then real(z) denotes the real part of z and the imaginary part is denoted img(z). For a positive integer i, the i th component of z is denoted by \(z_i\). For a matrix X and positive integers i, j, \(X_{ij}\) is the i th row and j th column entry of X. The diagonal square matrix containing entries of z along the diagonal is denoted by \(\mathscr {D}(z)\). If c is a scalar complex number, its absolute value is \(|c|=(|real(c)|^2+|img(c)|^2)^{1/2}\). The infinity norm of a possibly complex n-dimensional vector z is \(\Vert z\Vert _{\infty }=\max _{i=1}^n{|z_i|}\). The infinity norm of a possibly complex \(n\times m\) matrix X is \(\Vert X\Vert _\infty =\max _{i=1}^{n}\sum {|X_{ij}|}\).

The rest of the paper is organized as follows. We introduce template complex zonotopes in Sect. 5.2 and discuss important operations on them like linear transformation, Minkowski sum and inclusion checking. In Sect. 5.3, we first define a nearly periodic linear impulsive system and the problem of verifying global exponential stability. Using Proposition 5.1, we relate the contraction of a template complex zonotope to the eigenstructure of the dynamics, which is a motivation for using template complex zonotopes for stability verification. Later in that section, we discuss how to find suitable template complex zonotopes and verify their contraction to establish exponential stability of the system. In Sect. 5.4, we describe experiments on two benchmark examples and their results which corroborate the efficiency of our approach.

2 Template Complex Zonotopes

A template complex zonotope is a set representation in which each point is described as a linear combination of a set of complex-valued vectors, called as a template, such that the complex combining coefficients are bounded in absolute values by a set of positive bounds called scaling factors.

Definition 5.1

(Template complex zonotope) For \(n,m\in \mathbb {Z}_{> 0}\), let \(V\in \mathbb {M}_{n\times m}(\mathbb {C})\) be a template, \(c\in \mathbb {C}^n\) be a center point and \(s\in {{\mathbb {R}}}^m_{\ge 0}\) be scaling factors. Then we define a template complex zonotope as

$$ \mathscr {C}\left(V,c,s\right)=\left\{ V\zeta +c:\zeta \in \mathbb {C}^m~\wedge ~\forall i\in \{1,\ldots ,m\},|\zeta _i|\le s_i\right\} . $$

Complex zonotopes, which were introduced in [1], are a special case of template complex zonotopes where \(s_i = 1\) for all \(i\in \{1,\ldots ,m\}\). The real projection of a template complex zonotope can represent, in addition to polytopic zonotopes, non-polyhedral convex sets. Therefore, they are also more expressive than usual (real-valued) zonotopes. To illustrate, Fig. 5.1 represents the non-polyhedral real projection of the template complex zonotope \(\mathscr {C}\left(V,0,s\right)\) where \(V=\left({\begin{matrix}(1+2i) &{} 1 &{} (2+i)\\ (1-2i) &{} 1 &{} (2-i)\end{matrix}}\right)\) and \(s=[1~1~1]^T\).

Fig. 5.1
figure 1

Real projection of a template complex zonotope

Full size image

In the rest of the paper, unless otherwise stated, we assume that V is an \(n\times m\) complex matrix, s is an \(m\times 1\) column vector and c is a \(n\times 1\) column vector for \(m,n\in \mathbb {Z}_{> 0}\).

Operations on template complex zonotopes. Concerning linear transformation and the Minkowski sum, computations on template complex zonotopes are similar to those on usual (real-valued) zonotopes as stated in the following results, which can be proved by the same techniques as that of a usual zonotope.

Lemma 5.1

(Linear transformation and Minkowski sum)  Let \(A\in \mathbb {M}_{n\times n}(\mathbb {C})\), \(V\in \mathbb {M}_{n\times m}(\mathbb {C})\), \(G\in \mathbb {M}_{n\times r}(\mathbb {C})\), \(c,d\in \mathbb {C}^n\), \(s\in {{\mathbb {R}}}^m_{\ge 0}\), \(h\in \mathbb {R}^r_{\ge 0}\) for some \(n,m,r\in \mathbb {Z}_{> 0}\).

  1. 1.

    Linear transformation: \(A\mathscr {C}\left(V,c,s\right)=\mathscr {C}\left(AV,Ac,s\right)\).

  2. 2.

    Minkowski sum: \(\mathscr {C}\left(V,c,s\right)\oplus \mathscr {C}\left(G,d,h\right)=\mathscr {C}\left(\left[V~~G\right],(c+d),\left(\begin{array}{l}s\\ h\end{array}\right)\right)\).

Checking inclusion is a fundamental problem in reachability computation. For stability verification, we are interested in efficiently checking the inclusion between two template complex zonotopes centered at the origin. Although this problem is non-convex in general, we derive an easily verifiable convex condition which is sufficient (but not necessary), as follows. The inclusion checking method we propose in the following can be extended to zonotopes centered anywhere.

Let us consider that we want to check the inclusion of a template complex zonotope \(\mathscr {C}\left(V^a,0,s^a\right)\) inside a template complex zonotope \(\mathscr {C}\left(V^b,0,s^b\right)\), where \(V^a\in \mathbb {M}_{n\times r}(\mathbb {C})\), \(V^b\in \mathbb {M}_{n\times m}(\mathbb {C})\), \(s^a\in \mathbb {R}^{r}_{\ge 0}\) and \(s^b\in \mathbb {R}^m_{\ge 0}\) for some \(n,m,r\in \mathbb {Z}_{> 0}\). We relate any point in \(V^a\) to a point in \(V^b\) as follows. Consider \(X\in \mathbb {M}_{r\times m}(\mathbb {C})\) as a matrix solving \(V^a\mathscr {D}(s^a)=V^bX\), which we call a transfer matrix from \(\mathscr {C}\left(V^a,0,s^a\right)\) to \(\mathscr {C}\left(V^b,0,s^b\right)\). Recall that \(\mathscr {D}(s^a)\) is the diagonal square matrix containing entries of \(s^a\) along its diagonal. Let any point z in \(\mathscr {C}\left(V^a,0,s\right)\) be written as \(z=V^a\zeta \) where \(\zeta \) is a combining coefficient whose absolute values are bounded by \(s^a\). By normalizing with the scaling factors, we can write \(\zeta =\mathscr {D}(s)\varepsilon \) for some \(\varepsilon :\Vert \varepsilon \Vert _{\infty }\le 1\). So, we get \(z=V^a\mathscr {D}(s)\varepsilon \). Then using the relation for the transfer matrix, we rewrite \(z=V^bX\varepsilon \). If the absolute value of every component of \(X\varepsilon \) is less than the corresponding value of \(s^b\), then \(X\varepsilon \) can be treated as a combining coefficient of \(\mathscr {C}\left(V^b,0,s^b\right)\) for the point z and then z also belongs to \(\mathscr {C}\left(V^b,0,s^b\right)\). This is true if \(\sum _{j=1}^m|X_{ij}|\le s^b_i~\forall i\in \{1,\ldots ,m\}\). This gives us a sufficient condition, stated in the following theorem for inclusion of \(\mathscr {C}\left(V^a,0,s^a\right)\) in \(\mathscr {C}\left(V^b,0,s^b\right)\).

Theorem 5.1

(Inclusion) Let \(V^a\in \mathbb {M}_{n\times r}(\mathbb {C})\), \(V^b\in \mathbb {M}_{n\times m}(\mathbb {C})\), \(s^a\in \mathbb {R}^{r}_{\ge 0}\) and \(s^b\in \mathbb {R}^m_{\ge 0}\) for some \(n,m,r\in \mathbb {Z}_{> 0}\). Then \(\mathscr {C}\left(V^a,0,s^a\right)\subseteq \mathscr {C}\left(V^b,0,s^b\right)\) if all the following statements are true.

$$\begin{aligned} \begin{aligned}&\exists X\in \mathbb {M}_{m\times r}(\mathbb {C}):~\\&V^bX=V^a\mathscr {D}(s^a)~~\text {and}~~\forall i\in \{1,\ldots ,m\}~~\left(\sum _{j=1}^r|X_{ij}|\right)\le s_i^b. \end{aligned} \end{aligned}$$
(5.1)

For fixed \(V_a\) and \(V_b\), the constraints in Theorem 5.1 are second-order conic constraints in the variables \(s^a\), \(s^b\), and X. Many convex optimization solvers can solve such constraints efficiently upto a high numerical precision.

3 Nearly Periodic Linear Impulsive System

A nearly periodic linear impulsive system is a hybrid system whose state evolves continuously by a linear differential equation for some bounded time period, after which there is an instantaneous linear impulse. Formally, a linear impulsive system is specified by a tuple \(\mathscr {L}=\langle A_c,A_r,\varDelta \rangle \) where \(A_c\) and \(A_r\) are \(n\times n\) real matrices called the linear field matrix and impulse matrix, respectively. The positive integer n is the dimension of the state space and \(\varDelta =[t_{min},t_{max}]\) is an interval of nonnegative reals, called the sampling period interval. The dynamics of the nearly periodic linear impulsive system is described as follows. A function \(\mathbf x :\mathbb {R}_{\ge 0}\rightarrow \mathbb {R}^n\) is called a trajectory of the system if there exists a sequence of sampling timesdefinition \((t_i)_{i=1}^\infty \) satisfying all the following:

$$\begin{aligned} \begin{aligned}&(t_{i+1}-t_i)\in \varDelta ~~\forall i\in \mathbb {Z}_{> 0}~~~~(\text {uncertainty in sampling period})\\&\dot{\mathbf{x }}(t)=A_c\mathbf x (t)~~\forall t\in \mathbb {R}_{\ge 0}:~t\ne t_i ~\forall i\in \mathbb {Z}_{> 0}~~(\text {continuous})\\&\mathbf x (t_i^+)=A_r\mathbf x (t_i^-)~~\forall i\in \mathbb {Z}_{> 0}~~~~(\text {linear impulse}) \end{aligned} \end{aligned}$$
(5.2)

We say that the linear impulsive system is globally exponentially stable (GES) if all the trajectories of the system beginning at any point in the state space eventually reach arbitrarily close to the origin at an exponential rate, as follows.

Definition 5.2

(Global exponential stability) The system (5.2) is globally exponentially stable (GES) if there exist positive scalars \(c>0\) and \(\lambda \in [0,1)\) such that for all \(t\in \mathbb {R}_{\ge 0}\), \(\mathbf x (t)\le c\lambda ^t\Vert \mathbf x (0)\Vert \).

We state the stability verification problem as follows.

Problem 5.1

(Stability verification problem) proposition Given \(A_c\), \(A_r\), \(t_{min}\), find the largest upper bound \(t_{max}\) on the sampling time to guarantee exponential stability.

Related work on stability verification of nearly periodic linear impulsive systems

A common approach to this problem is extending Lyapunov techniques, which results in Lyapunov Krakovskii functionals [37, 39] (using the framework of time-delay systems), and discrete-time Lyapunov functions [36]. Stability with respect to time-varying input delay can also be handled by input/output approach [24]. Stability verification problem for time-varying impulsive systems can also be formulated in a hybrid systems framework [8, 20, 32], for which various Lyapunov-based methods including discontinuous time-independent [31] or time-dependent Lyapunov functions [17] were developed. Another approach involves using convex embedding [18, 21, 22]. In this approach, stability conditions can be checked using parametric Linear Matrix Inequalities (LMIs) [21], or as set contractiveness (such as, polytopic set contractiveness) [10, 16, 25]. Inspired by these results on set contractiveness, conditions [1] provides a stability condition, expressed in terms of complex zonotopes, which is more conservative but can be efficiently verified. The novelty of this work is in the extension of complex zonotopes to template complex zonotopes which allows a systematic way to synthesize contractive zonotopic sets to verify stability.

The state reached after a linear impulse followed by a continuous evolution for time t is \(e^{A_ct}A_rx\). So, let us denote \(H_t=e^{A_ct}A_r\) for any positive real t, which we call as the reachability operator if t lies in the sampling period interval \(\varDelta \). Given a set \(\varPsi \subset \mathbb {R}^n\), the set of all reachable points of \(\varPsi \), when acted upon by an impulse followed by continuous evolution for sampling time period \(t\in \varDelta \) until before the next impulse, is \(\bigcup _{t\in \varDelta }H_t\varPsi \). It was shown previously in [16, 25] that a necessary and sufficient condition for exponential stability is the existence of a convex, compact, and closed set containing the origin in its interior, called a C-set, that contracts between subsequent impulses. In other words, we can establish exponential stability by finding a C-set \(\varPsi \) such that \(H_t\varPsi \subseteq \lambda \varPsi \) for some \(\lambda \in [0,1)\) and for all \(t\in \varDelta \). In this paper, we want to find contractive C-sets represented as template complex zonotopes. We define contraction of a template complex due to a linear operator as follows, which when less than one, implies that the zonotope is contractive.

Definition 5.3

For a template complex zonotope \(\mathscr {C}\left(V,0,s\right)\), the amount of contraction by a square matrix \(J\in \mathbb {M}_{n\times n}(\mathbb {R})\), denoted by \(\chi (V,s,J)\) is

$$ \chi (V,s,J)=\min \left\rbrace \lambda \in \mathbb {R}_{\ge 0}:J\mathscr {C}\left(V,0,s\right)\subseteq \lambda \mathscr {C}\left(V,0,s\right)\right\lbrace . $$

Our motivation for considering template complex zonotopes can be inferred from the following proposition.

Proposition 5.1

  Let V contain only the eigenvectors of \(H_t\) as its column vectors and \(\mu \) be the vector of eigenvalues corresponding the columns of V. Then \(H_t\mathscr {C}\left(V,0,s\right)=\mathscr {C}\left(V,0,\mathscr {D}(|\mu |)s\right)\).

For a fixed sampling time period, i.e., when \(t_{min}=t_{max}=t\), we can infer from the above proposition that the contraction of the template complex zonotope formed by the eigenvector template is bounded by the largest absolute value of the eigenvalues. Therefore, when the sampling period is fixed, we can find contractive template complex zonotopes for exponentially stable systems by choosing the template as the collection of eigenvectors. However, we are interested in the case where the sampling time period varies in the interval \(\varDelta \), i.e., there are uncountably many reachability operators parametrized over the time interval \(\varDelta \). Motivated by the above analysis, when the sampling period is uncertain, we choose the template as the collection of eigenvectors of a few reachability operators and try to synthesize suitable scaling factors for which the template complex zonotope contracts with respect to the chosen finite set of reachability operators. However, later we also verify that the synthesized template complex zonotope actually contracts with respect to all the (uncountably many) reachability operators. First, we describe the procedure to synthesize the template complex zonotope.

Synthesizing a candidate template complex zonotope. This step of systematically synthesizing a suitable template complex zonotope that is likely to be contractive constitutes the main improvement over the procedure proposed in [1]. Our criterion for synthesizing the template complex zonotope is that it has to be contractive with respect to a few reachability operators (called reference operators), which is a necessary condition for contraction with respect to the overall system dynamics. Since the eigenstructure of the reachability operators is related to the stability of the system, we include the eigenvectors of a few reachability operators in the template. For a fixed number \(k\in \mathbb {Z}_{> 0}\) of reference operators, they can be chosen incrementally as follows. Define k-sampled time points as \(\varLambda _k=\left\rbrace t_{min}+i\frac{(t_{max}-t_{min})}{k}:i\in \{0,\ldots ,k-1\}\right\lbrace .\) Then, we define the set of k-sampled reachability operators as \(\varGamma _k=\left\rbrace H_{t}:t\in \varLambda _k\right\lbrace \). Let us denote the template of collection of eigenvectors of all operators in \(\varGamma _k\) as \(E_k\). For this template, we synthesize suitable scaling factors based on the following theorem. The derivation of this theorem uses the inclusion checking condition from Theorem 5.1.

Theorem 5.2

If \(E_k\) have rank n. For a vector of scaling factors \(s\in \mathbb {R}^{m}_{\ge 0}\), the template complex zonotope \(\mathscr {Z}=\mathscr {C}\left(E_k,0,s\right)\) would represent a C-set and also \(H_t\mathscr {Z}\subseteq \lambda \mathscr {Z}\) for \(\lambda \in (0,1)\) if following are all satisfied.

$$\begin{aligned} \begin{aligned}&s\in \mathbb {R}^n_{\ge 1}~~\text {(sufficient condition for representing C-set)}\\&\exists X_t\in \mathbb {M}_{m\times m}(\mathbb {C})~~\forall t\in \varLambda _k~~\text {s.t.}\\&E_kX_t=H_tE_k\mathscr {D}(s)~~~~(\text {transfer matrix condition})\\&\sum _{j=1}^m\left|\left(X_t\right)_{ij}\right|\le \lambda s_i~~\forall i\in \{1,\ldots ,m\}~~\text {(bounding contraction)}\\ \end{aligned} \end{aligned}$$
(5.3)

Therefore, we can synthesize a template complex zonotope that is contractive with respect to a finite chosen number \(k>0\) of reference operators by solving for the scaling factors satisfying the second-order conic constraints in (5.3).

Verifying contraction. To verify that this synthesized template complex zonotope actually contracts with respect to all the reachability operators \(H_t\), where t is parametrized over the whole sampling time interval \(\varDelta \), we divide the sampling interval into small enough subintervals and verify contraction in each interval. To bound the amount of contraction in small intervals, we use some useful properties of contraction, which were earlier derived in [1].

Let \(H_{t+\rho }\) be an operator where \(\rho \) lies in the interval \((0,\varepsilon )\). For an order of Taylor expansion \(r\in \mathbb {Z}_{> 0}\) and some \(\delta \in [0,\varepsilon ]\), define

$$ P^t_r(\rho )=\sum _{i=0}^r\frac{A_c^i\rho ^i}{i!}H_t~~\text {and}~~ E^t_r(\delta )=\frac{A_c^{r+1}\delta ^{r+1}}{(r+1)!}H_t. $$

Then based on Taylor expansion, we get that

$$ H_{t+\rho } = P_r^t(\rho ) +{theorem} E_r^t(\delta ). $$

Furthermore, a bound on contraction as sum of contractions depending on \(\varepsilon \) is derived in [1] as

$$\begin{aligned} \begin{aligned}&~~~~~~~~~~~\chi \left(V,s,H_{t+\rho }\right)\le \left(\max _{i=0}^r\chi \left(V,s,P^t_r(\varepsilon )\right)\right)+ \frac{\varepsilon ^{r+1}}{(r+1)!}\chi \left(V,s,A_c^{r+1}H_t\right) \end{aligned} \end{aligned}$$
(5.4)

The right-hand side of (5.4) can be bounded if we know a bound on the contraction under a linear operation, which is derived as follows.

Lemma 5.2

Let \(J\in \mathbb {M}_{n\times n}(\mathbb {R})\). Define

$$ \beta (V,s,J)=\min \{\Vert X\Vert _\infty :X\in \mathbb {M}_{m\times m}(\mathbb {C})~\wedge ~ V\mathscr {D}(s)X=JV\mathscr {D}(s)\} $$

Then we have \(\chi (V,s,J)\le \beta (V,s,J)\).

Proof

If \(JV\mathscr {D}(s)=V\mathscr {D}(s)X\), we want to prove that \(J\mathscr {C}\left(V,0,s\right)=\mathscr {C}\left(JV,0,s\right)\subseteq \Vert X\Vert _\infty \mathscr {C}\left(V,0,s\right)\). We deduce \(\mathscr {C}\left(JV,0,s\right)=\{ JV\zeta \;:\; \forall i\in \{1,\ldots ,m\}|\zeta _i|\le s_i \}\; = \; \{JV\mathscr {D}(s)\zeta ^\prime :\Vert \zeta ^\prime \Vert _{\infty } \le 1\} =\) \(\{V\mathscr {D}(s)X\zeta ^\prime :\Vert \zeta ^\prime \Vert _\infty \le 1\}\subseteq \Vert X\Vert _\infty \{V\mathscr {D}(s)\zeta ^\prime :\Vert \zeta ^\prime \Vert _{\infty }\le 1\} = \Vert X\Vert _\infty \{V\zeta \;:\; \forall i\in \{1,\ldots ,m\} |\zeta _i|\le s_i \} = \Vert X\Vert _{\infty }\mathscr {C}\left(V,0,s\right)\).

Then the contraction for sampling time interval \((t,t+\delta )\) can be bounded as follows.

Theorem 5.3

Let \(\rho \in (t,t+\varepsilon )\) and for \(r\in \mathbb {Z}_{>0}\), \( P^t_r(\rho )=\sum _{i=0}^r\frac{A_c^i\rho ^i}{i!}H_t\). Define \(\eta _r(V,s,t,\varepsilon )= \left(\max _{i=0}^r\beta \left(V,s,P^t_r(\varepsilon )\right)\right)+ \frac{\varepsilon ^{r+1}}{(r+1)!}\beta \left(V,s,A_c^{r+1}H_t\right)\), where the bound \(\beta (.)\) is defined in Lemma 5.2. Then \(\chi \left(V,s,H_{t+\rho }\right)\le \eta _r(V,s,t,\varepsilon ) \)

Verification algorithm. We begin with \(k=3\) reference operators that correspond to the two end points of the sampling interval and the middle point. The algorithm first finds suitable scaling factors s that gives a template complex zonotope which contracts with respect to these reference operators. Next, it checks whether the contraction of the template complex zonotope \(\mathscr {C}\left(E_k,0,s\right)\) with respect to all the reachability operators is less than one. For checking contraction, we use the algorithm earlier proposed in  [1]. If successful, then exponential stability of the system is verified. Otherwise, k is increased, the algorithm synthesizes the template complex zonotope for the increased k and then checks contraction. If unsuccessful after a maximum value of k, the algorithm stops and the result is inconclusive. This is described in Algorithm 1. This algorithm has been implemented and we defer experimental results to Sect. 5.4.

figure a

4 Experiments

We evaluated our algorithm on two benchmark examples of linear impulsive systems below and compared it with other state-of-the-art approaches. For convex optimization, we use CVX version 2.1 with MATLAB 8.5.0.197613 (R2015a). The reported experimental results were obtained on Intel(R) Core(TM) i5-3470 CPU @ 3.20GHz.

Example 1

We consider a networked control system with uncertain but bounded transmission period. A networked control system is composed of a plant and a controller that interact with each other by transmission of feedback input from controller to the plant. If the system dynamics is linear with linear feedback, then for uncertain but bounded transmission period, we can equivalently represent it as a linear impulsive system where \(A_c=\left(\begin{array}{ccc} A_p &{} 0 &{} B_p\\ 0 &{} 0 &{} 0\\ 0 &{} 0 &{} 0 \end{array}\right),~A_r=\left(\begin{array}{ccc} \mathbb {I} &{} 0 &{} 0\\ B_oC_p &{} A_o &{} 0\\ D_oC_p &{} C_o &{} 0 \end{array}\right)\) for some parameter matrices \(A_p\), \(B_p\), \(B_o\), \(C_p\), \(A_o\), \(C_o\), and \(D_o\). The sampling interval \(\varDelta \) of the linear impulsive system specifies bounds on the transmission interval. Our example of a networked control system is taken from Björn et al. [38]. The system is originally described by discrete-time transfer functions, which has an equivalent state-space representation with parameter matrices \(A_p=\left(\begin{array}{cc}-1 &{} 0\\ 1 &{} 0\end{array}\right)\), \(B_p=\left(\begin{array}{c}1\\ 0\end{array}\right)\), \(C_p=\left(\begin{array}{cc}0&1\end{array}\right)\), \(A_o=0.4286\), \(B_o=-0.8163\), \(C_o=-1\) and \(D_o=-3.4286\). Given the lower bound on the transmission period as \(t_{min}=0.8\), we want to find as high a value of \(t_{max}\) as possible for which the system is GES.

Example 2

We consider the following linear impulsive system from Hetel et. al. [22] that describes an LMI-based approach to verify stability. The specification is given by \(A_c=\left(\begin{array}{ccc} 0 &{} -3 &{} 1\\ 1.4 &{} -2.6 &{} 0.6\\ 8.4 &{} -18.6 &{} 4.6 \end{array}\right) \) and \(A_r=\left(\begin{array}{ccc} 1 &{} 0 &{} 0\\ 0 &{} 1 &{} 0\\ 0 &{} 0 &{} 0 \end{array}\right).\)

Table 5.1 Example 1
Full size table
Table 5.2 Example 2
Full size table
Table 5.3 Template complex zonotopes (TCZ) vs Complex zonotopes (CZ) [1]
Full size table

Setting and Results. While implementing the algorithm for stability verification, we used order Taylor expansion, a tolerance of \(tol=0.01\) for Example 1 and \(tol=0.006\) for Example 2. We required \(k=3\) number of reachability operators for both examples, for synthesizing a suitable template complex zonotope used in checking contraction. We could verify exponential stability in a sampling interval [0.08, 0.58] for Example 1 and [0.1, 0.496] for Example 2. The comparison of our approach with the state-of-the-art NCS toolbox [8] and also other approaches is presented in Tables 5.1 and 5.2. For the first example, our method outperforms other approaches, while it is competitive with other approaches on the second example. Furthermore, Table 5.3 shows that the template complex zonotope based approach is also faster than the complex zonotope approach of [1].

5 Conclusion

We extended complex zonotopes to template complex zonotopes in order to improve the efficiency of the computation of contractive sets and positive invariants. Template complex zonotopes retain a useful feature of complex zonotopes, which is the scope to incorporate the eigenvectors of linear dynamics among the generators because the eigenstructure is related to existence of positive invariants. In addition, compared to complex zonotopes, the advantage template complex zonotopes have is the ability to regulate the contribution of each generator to the set by using the scaling factors. Accordingly, we proposed a systematic and more efficient procedure for verification of stability of nearly periodic impulsive systems. The advantage of this new set representation is attested by the experimental results that are better or competitive, compared to the state-of-the-art methods and tools on benchmark examples. This work also contributes a method for exploiting the eigenstructure of linear dynamics to algorithmically determine template directions, required by most verification approaches using template-based set representations. A number of directions for future research can be identified. First, we intend to extend these techniques to analysis to switched systems under constrained switching laws. Also computationally speaking, our approach is close in spirit to abstract interpretation. Indeed, the operations used to find contractive sets can be extended to invariant computation for general hybrid systems with state-dependent discrete transitions.