# Safety Verification of Interconnected Hybrid Systems Using Barrier Certificates.

1. Introduction

The problem of safety verification of hybrid dynamical systems has always been a fundamental issue within the systems, control, and computer communities. In principle, safety verification of hybrid dynamical systems aims to determine that any trajectory starting at admissible initial states cannot evolve to unsafe region in the state space [1]. Numerous methods have been developed for the past two decades [2] and a variety of dynamical characteristics have been researched. Particularly, we concentrate on safety verification of a special kind of nonlinear hybrid dynamical system called polynomial hybrid system. Polynomial hybrid systems are hybrid systems where both the dynamical behavior description and the states constraints are given in terms of polynomial nonlinearities. A wide range of applications could be modeled as, transformed into, or approximated by polynomial hybrid systems, for example, in power systems [3] and process control [4]. In [5-7], computational verification methods based on symbolic computation have been proposed; those methods are mainly based on the theory of ideal over polynomial ring together with techniques such as abstract interpretation. On the other hand, computational verification methods based on numerical computation which originated from [8] have also been well developed. One of the typical methods called barrier certificate generalizes these numerical verification methods and imposes its theoretical foundation on linear matrix inequalities (LMI), semidefinite programming (SDP), sum-of-squares (SOS) programming, and bilinear SOS programming.

Generally speaking, barrier certificate is a function of states whose zero level set separates an unsafe region from all system trajectories starting from an admissible set of initial states. The existence of a barrier certificate is sufficient for safety of dynamical systems, which is analogous to the sufficiency of the existence of a Lyapunov function for asymptotic stability of dynamical systems. As an important numerical method of safety verification of dynamical systems, barrier certificates have been well developed under the frameworks of general nonlinear systems [9], time-delayed systems [10, 11], stochastic systems [12], interconnected continuous systems [13, 14], and hybrid systems [1, 15]. Besides, converse theorem of barrier certificates was discussed recently in [16].

Hybrid systems are dynamical systems exhibiting both continuous and discrete dynamic behaviors, and interconnected hybrid systems are an interconnection of several hybrid systems consisting of assignments relating the inputs and outputs of the individual hybrid systems. Therefore, safety of interconnected hybrid systems relies on both safety of the individual subsystems and their interconnections. In this paper, we propose compositional barrier certificates for safety verification of interconnected hybrid systems. As we know, many networked embedded systems, particularly recently proposed Internet-of-Things and Cyber-Physical Systems [17], are characterized by interconnected hybrid systems; however, safety verification for interconnected hybrid systems has not been well developed. Thus, there is a need to study safety verification method for interconnected hybrid systems. Motivated by the above-mentioned reasons and the practical background, we consider the issue of developing compositional barrier certificates of interconnected hybrid systems for their safety verification. To the best of our knowledge, safety verification has been discussed only for interconnected continuous systems [13, 18-20], but not for interconnected hybrid systems yet, which also motivated our research.

Due to the new features deriving from interconnected hybrid systems, finding a compositional barrier certificate for safety verification presents more technical challenges. Considering that the existences of barrier certificates of each interconnected hybrid system are not sufficient for safety of interconnected hybrid systems, additional dissipation-inequality-like constraints are required to be imposed on interconnections. Compositional barrier certificates in our paper impose additional dissipation-inequality-like coupling constraints on a set of individual barrier certificates for each subsystem. Furthermore, constructing compositional barrier certificates satisfying dissipation-inequality-like constraints is intractable in general; however, through applying SOS relaxation and generalized S-procedure, some conservative compositional barrier certificates could be derived through numerical computation. Once these compositional barrier certificates composed of individual barrier certificates and coupling constraints are feasible, bilinear SOS programming could be applied to construct such compositional barrier certificates through purely numerical computation. Numerical SOS programming solvers such as SOSTOOLS [21] and SOSOPT [22] are developed for such computations. With this methodology, we are able to verify safety of interconnected hybrid systems without resorting exhaustive simulations.

The paper is organized as follows. Section 2 introduces the notations as well as some preliminary definitions. Section 3 adopts the compositional hybrid I/O automata framework to describe interconnected hybrid systems and presents the formal definition of safety. Section 4 explains how to formulate the verification problem by incorporating interconnections satisfying diagonal stability property with individual barrier certificates. Section 5 shows how to construct the compositional barrier certificates through solving a feasibility problem of bilinear SOS programming. Section 6 presents a numerical example to show the validity of the proposed method and Section 7 comprises conclusions.

2. Mathematical Preliminaries

Notations. Let R denote the field of real numbers, and [R.sup.n] stand for the n-dimensional real vector space. [R.sub.>0], [N.sub.>0] refer to the sets of positive real numbers and positive natural numbers, respectively. Lower case alphabets such as i, j, k, I, m, n represent variables, while symbols such as [mathematical expression not reproducible] are vectorial variables. [parallel] x [parallel] refers to the Euclidean vector norm. For matrices or vectors, the superscript "T" denotes matrix transposition. [I.sup.mxm] is the identity matrix, 0 denotes zero vector, 0 is scalar, and [0.sup.mxn] is an m x n zero matrix. The notation diag {*} indicates a square diagonal matrix with the arguments along the diagonal. [A.sup.-1] is the inverse of matrix A.

Definition 1 (positive-definite polynomial and its Lie-derivative). Let [??] denote the n-tuple ([x.sub.1], ..., [x.sub.n]), [P.sup.m.sub.n] will be taken as the polynomial field over variables in x with the highest degree of m, and a polynomial function p([??]) [member of] [P.sup.m.sub.n] is said to be positive definite iff

p([??])>0 (1)

for all [mathematical expression not reproducible] with p([??]) = 0. The first-order Liederivative of p([??]) along a continuous flow [mathematical expression not reproducible] is as follows:

[mathematical expression not reproducible]. (2)

Definition 2 (SOS polynomial). A multivariate polynomial p([??]) is an SOS polynomial if there exist finite polynomials [p.sub.1]([??]), ..., [p.sub.k]([??]) such that

p([??]) = [k.summation over (i=1)] [p.sup.2.sub.i] ([??]). (3)

Let [[SIGMA].sup.2m.sub.n] ([[SIGMA].sub.n] for short) denote the set of all SOS polynomials in x under the degree of 2m.

Definition 3 (semialgebraic set). A set [mathematical expression not reproducible] is called a semialgebraic set iff [p.sub.1]([??]), ..., [p.sub.s]([??]) [member of] [P.sup.m.sub.n] and s [member of] [N.sub.>0] is finite.

Definition 4 (K polynomial function). A polynomial function [alpha]([parallel][??][parallel]) : [R.sub.[greater than or equal to]0] [right arrow] [R.sub.[greater than or equal to]0] is of class K; equivalently [alpha]([parallel][??][parallel]) [member of] [P.sup.m.sub.n] [intersection] K, if it is strictly increasing and [alpha]([??]) = 0.

Definition 5 (Kronecker product). Let A = [[a.sub.i,j]] [member of] [R.sup.mxn], B [member of] [R.sup.pxq] denote two matrices, and then the Kronecker product of A and B is defined as the matrix:

[mathematical expression not reproducible]. (4)

Definition 6 ([less than or equal to] for matrices). For two matrices A = [[a.sub.i,j]] [member of] [R.sup.mxn], B = [[b.sub.i,j]] [member of] [R.sup.mxn], A [less than or equal to] B if and only if

[a.sub.ij] [less than or equal to] [b.sub.i,j] [for all]1 [less than or equal to] i [less than or equal to] m, l [less than or equal to] j [less than or equal to] n. (5)

The bilinear SOS program is a subclass of nonlinear program which takes the following form.

Definition 7 (bilinear SOS program, see [22]). Standard bilinear SOS program form is

Min scalar variable t

[mathematical expression not reproducible], (6)

where [mathematical expression not reproducible] are decision variables. [mathematical expression not reproducible] are polynomials with given data and affine in [??].

3. Formal Models of Interconnected Systems

Throughout this paper, we adopt the compositional hybrid I/O automata framework discussed in [23] for describing interconnected hybrid systems. Interactions of individual hybrid dynamics occur at both the continuous and discrete levels. In this section, we would like to present the formal model of compositional hybrid I/O automata H which is a composition of finite hybrid I/O automaton [H.sub.i[member of][??]] indexed by the finite set [??]. To provide the formal definition of compositional hybrid I/O automata, we initially consider the individual hybrid I/O automata.

Definition 8 (individual hybrid I/O automaton). An individual hybrid I/O automaton [H.sub.i] of H is a tuple [H.sub.i] = {[X.sub.i], [U.sub.i], [Y.sub.i], [S.sub.i], [Q.sub.i], [G.sub.i], [F.sub.i], [X.sup.0.sub.i], [X.sup.0.sub.i], [X.sup.u.sub.i]} with the following components:

(i) [mathematical expression not reproducible] is a set of real-valued system internal variables [[??].sub.i] [member of] [X.sub.i]. The number [n.sub.i] is called the dimension of [H.sub.i].

(ii) [U.sub.i] [subset] [R.sup.r] is a set of real-valued system external inputs [[??].sup.c.sub.i], [[??].sup.d.sub.i] [member of] [U.sub.i], where [[??].sup.c.sub.i] denotes the continuous input while [[??].sup.d.sub.i] denotes the discrete input. U; is disjoint from [X.sub.i].

(iii) [Y.sub.i] [subset or equal to] [R.sup.r] is a set of real-valued system external outputs [[??].sup.c.sub.i], [[??].sup.d.sub.e] [member of] [Y.sub.i], where [[??].sup.c.sub.i] denotes the continuous output while [[??].sup.d.sub.i] denotes the discrete output. [Y.sub.i] is disjoint from [X.sub.i] [union] [U.sub.i].

(iv) [S.sub.i] is a finite set of indexes of switching signals. The index function [sigma](t) : [0, T] [right arrow] [S.sub.i] = {[1.sub.i], ..., [j.sub.i], [l.sub.j], ..., [s.sub.i]} denotes the sequence of activated switching signals [S.sub.i] over the continuous-time interval [0,T].

(v) [Q.sub.i] is a finite set of modes. The overall state space of individual hybrid systems [H.sub.i] is [Q.sub.i] x [X.sub.i], and a state is denoted by ([q.sub.i], [[??].sub.i]) [member of] [Q.sub.i] x [X.sub.i] [q.sup.j.sub.i], [q.sup.k.sub.i] [member of] [Q.sub.i] denote different modes of [H.sub.i] when j [not equal to] k.

(vi) [G.sub.i] [subset or equal to] [X.sub.i] is the set of guard conditions for [H.sub.i]. A switching is enabled at [t.sup.*.sub.i] once [[??].sub.i]([t.sup.*.sub.i]) [member of] [G.sub.i] holds, namely, a state-dependent switching. Throughout this paper, all switchings of [H.sub.i] are assumed to be state-dependent. Furthermore, [C.sub.i] is taken as the complement of [G.sub.i] ([C.sub.i] = [X.sub.i] - [G.sub.i]).

(vii) [mathematical expression not reproducible] is a set of continuous vector fields. For each state ([q.sub.i], [[??].sub.i]) [member of] [Q.sub.i] x [X.sub.i], [F.sub.i] incorporates a differential constraint on the continuous evolution according to the differential equation:

[mathematical expression not reproducible], (7)

where [??] [member of] [C.sub.i], [t.sub.i] [member of] ([t.sup.k-1.sub.1], [t.sup.k.sub.i]], k [member of] [N.sub.>0], and [[sigma].sub.i]([t.sub.i]) [member of] [S.sub.i].

(viii) [T.sub.i] : [Q.sub.i] x [G.sub.i] x S [right arrow] [Q.sub.i] is a relation capturing discrete switchings between two modes. Here a switching

[mathematical expression not reproducible] indicates that from mode [q.sub.i], [H.sub.i] can undergo a switching to the mode [q.sup.k.sub.i] at the instant [t.sup.*.sub.i]. Only finite switchings are allowed over finite-time intervals.

(ix) [X.sup.0.sub.i] [subset or equal to] X is the set of admissible initial states of [H.sub.i].

(x) [X.sup.u.sub.i] [subset or equal to] X is the set of unsafe states of [H.sub.i].

Trajectories of H; start from the admissible initial states [[??].sup.0.sub.i] and are concatenations of a sequence of continuous evolutions in [[??].sub.i] and discrete switchings among different modes [q.sup.j.sub.i], [q.sup.k.sub.i] [member of] [Q.sub.i] satisfying the following.

Initiation. [[??].sup.0.sub.i] [member of] [X.sup.0.sub.i] is an admissible initial state of [H.sub.i].

Discrete Consecution. At the instant [mathematical expression not reproducible], the switching signal [[sigma].sub.i]([t.sup.*.sub.i]) [member of] [S.sub.i]

[mathematical expression not reproducible]. (8)

activates and produces a discrete output according to

[mathematical expression not reproducible] (9)

simultaneously.

Continuous Consecution. For an activating mode [q.sup.j.sub.i] [member of] [Q.sub.i] over the [[t.sup.k.sub.i], [t.sup.k+1.sub.i])

[mathematical expression not reproducible] (10)

holds and produces continuous outputs according to

[mathematical expression not reproducible] (11)

over the continuous interval.

Here, [t.sup.*-.sub.i] denotes the left limit of [t.sup.*.sub.i] and [t.sup.*+.sub.i] denotes its right limit. Additionally, [mathematical expression not reproducible] are all restricted to polynomials throughout this paper.

Compositional hybrid I/O automaton H is given as an interconnection of finite individual hybrid I/O automaton consisting of assignments relating the inputs and outputs of interconnected [H.sub.i].

Definition 9 (compositional hybrid I/O automaton). A compositional hybrid I/O automaton H is a finite set of interconnected hybrid I/O automata [H.sub.i] indexed by i [member of] I. Formally, H is a tuple H = {I, [[union].sub.i[member of]l] {[H.sub.i]}, [N.sup.c], [N.sup.d], K} with the following components:

(i) I is a finite set of indexes of interconnected hybrid automaton {[H.sub.i]}. Without loss of generality, we assume I has M [member of] [N.sub.>0] elements.

(ii) [[union].sub.i[member of]l] {[H.sub.i]} is a finite set of interconnected hybrid I/O automata. X, U, Y, S, Q, F, T, [X.sup.0], [X.sup.u] of H are the Cartesian products of each corresponding item of all individual [H.sub.i]s, respectively. Particularly, [mathematical expression not reproducible], which means [??] [member of] G if there exists an [[??].sub.i] of [H.sub.i] which intersects corresponding guard [G.sub.i]. Dually, C [subset or equal to] X is defined as [mathematical expression not reproducible]. Besides, only finite switchings are allowed over any finite-time intervals.

(iii) K represents the static topology of the interconnection, which is in the form of an M x M matrix K = [[[a.sub.j,k]].sub.M x M], [a.sub.j,k] [member of] {0,1}, 1 [less than or equal to] j, k [less than or equal to] M.

(iv) [N.sup.c] is a finite set of interconnections following continuous assignments

[mathematical expression not reproducible] (12)

over continuous-time intervals, where [[??].sup.c.sub.i] is the interconnection over a continuous-time interval. [[a.sub.i,1], ..., [a.sub.i,M]] is the ith row of [mathematical expression not reproducible] are assumed to be polynomial functions.

(v) [N.sup.d] is a finite set of interconnections following discrete assignments

[mathematical expression not reproducible] (13)

at discrete instants, where [[??].sup.d.sub.i] is the interconnection at switching instant, and [[a.sub.i,1], ..., [a.sub.i,M]] is the ith row of [mathematical expression not reproducible] are assumed to be polynomial functions.

Intuitively, trajectory of H is the composition of trajectories of [H.sub.i]s under restrictions of the interconnections. We take [mathematical expression not reproducible] to represent the trajectory of [H.sub.i]; thus, the trajectory [mathematical expression not reproducible] of H is a Cartesian product satisfying the following.

Initiation. [mathematical expression not reproducible].

Discrete Consecution. For x e G, at least one [mathematical expression not reproducible] would undergo a switching. Switchings of interconnected trajectories are not required to occur simultaneously under our framework. At each instant of discrete consecution, an impulsive interconnection occurs according to the following algebraic equations:

[mathematical expression not reproducible]. (14)

Continuous Consecution. For [??] [member of] C, states of all trajectories of [H.sub.i] evolve continuously under the continuous interconnections according to the following differential equations:

[mathematical expression not reproducible]. (15)

For compositional hybrid I/O automata H, [??] [member of] X evolves continuously when all trajectories of [H.sub.i]s evolve continuously, while switchings occur once there exists a discrete consecution among [H.sub.i]s.

Based on the concept of trajectories of H, safety of H could be formalized as follows.

Definition 10 (safety of H). Let an interconnected hybrid I/O automaton H = {I, [U.sub.i[member of]l]{[H.sub.i]}, [N.sup.c], [N.sup.d], K} be given. Take [mathematical expression not reproducible] as the trajectory of H; then H is unsafe if there exists an instant [t.sup.*.sub.i] [member of] [0, T] such that [mathematical expression not reproducible]

[mathematical expression not reproducible] (16)

holds. Furthermore, H is safe when none of the trajectories of H starting from admissible initial states would intersect unsafe states [X.sup.u] of H.

4. Compositional Barrier Certificates

In this section, we present a brief introduction to the barrier certificate method and propose the compositional barrier certificate for safety verification of compositional hybrid I/O automaton.

4.1. Intuitive Interpretation of Barrier Certificates. To address the safety verification, we need to determine whether a trajectory starting from admissible initial states would reach the set of unsafe states. Barrier certificate methodology could certify safety of a dynamical system through constructing a function called barrier certificate. Generally speaking, barrier certificate B : [??] [right arrow] R ([??] denotes the state space) is a function of states satisfying a set of constraints on both the function itself and states evolution along the trajectories, and states [??] [member of] [??] satisfying B([??]) = 0 form a barrier separating all unsafe states from possible system trajectories. B([??]) takes different values on different regions: for example, for each [??] [member of] [X.sup.u] ([X.sup.u] denotes unsafe states region), it satisfies B([??] > 0), while for each [??] [member of] [X.sup.s] ([X.sup.s] denotes reachable states region of trajectories) B([??] [less than or equal to] 0) holds. Thus, system safety could be certified by the existence of a barrier certificate. An intuitive illustration of a barrier certificate is presented in Figure 1. As shown in the figure, unsafe states region is separated from states of trajectories by the barrier certificate.

4.2. Compositional Barrier Certificates. In the following, we present two lemmas to show sufficiency of the existence of barrier certificates for safety of individual hybrid I/O automaton and discuss how to impose inequality constraints on interconnections to construct compositional barrier certificates.

Lemma 11 (conservative barrier certificates for [H.sub.i]). Let an interconnected individual hybrid I/O automaton = [[X.sub.i], [U.sub.i], [Y.sub.i], [Q.sub.i], [G.sub.i], [F.sub.i], [T.sub.i], [X.sup.0.sub.i], [X.sup.u.sub.i]} be given. For each [[??].sup.c.sub.i], [[??].sup.d.sub.i] [member of] [U.sub.i], suppose there exists a function [B.sub.i]([[??].sub.i]) for all [m.sub.i] modes of [H.sub.i]. [B.sub.i]([[??].sub.i]) ispiecewise differentiable with respect to its state variable and satisfies

[B.sub.i]([??]) > 0, [for all][??], [member of] [X.sup.u.sub.i], (17)

[B.sub.i]([[??].sub.i]) [less than or equal to] 0, [for all][[??].sub.i] [member of] [X.sup.0.sub.i], (18)

[mathematical expression not reproducible] (19)

[mathematical expression not reproducible], (20)

where, for the case in (20), [H.sub.i] undergoes a switching from mode [q.sup.j.sub.i] to mode [q.sup.k.sub.i]. If such [B.sub.i]([[??].sub.i]) exists, then the safety of [H.sub.i] is guaranteed.

Proof (by contradiction). For each [[??].sup.c.sub.i], assume that barrier certificates [B.sup.j.sub.i] ([[??].sub.i]) satisfying (17)-(20) can be found and suppose there exists an instant [t.sup.*.sub.i] [member of] [0, T] when [[??].sub.i]([t.sup.*.sub.i]) [member of] [X.sup.u.sub.i]. Suppose there exist two sequences of instants [mathematical expression not reproducible] are either finite or infinite. At each [mathematical expression not reproducible] is activated, while, at each [t.sup.p], an impulsive interconnection rather than the continuous-time interconnection is activated. From (17), we derive [mathematical expression not reproducible]. The impulsive interconnection m; could be omitted considering

[mathematical expression not reproducible] (21)

for any finite p. And from (20), it concludes that [B.sub.i]([[??].sub.i]) decreases at each switching. Over the continuous-time interval [0, [t.sup.*.sub.i]], we have

[mathematical expression not reproducible]. (22)

Therefore, the derived [B.sub.i]([[??].sub.i]([t.sup.*.sub.i])) [less than or equal to] 0 contradicts the assumption [B.sub.i]([[??].sub.i]([t.sup.*.sub.i])) > 0. Thus, we conclude that any trajectory starting from admissible initial states would not intersect unsafe states. In conclusion, the existence of barrier certificates [B.sub.i]([[??].sub.i]) is sufficient for safety of [H.sub.i].

Remark 12. Intuitively, the value of [B.sub.i]([[??].sub.i]) decreases along both continuous flows as well as switchings, since [B.sub.t]([[??].sup.0.sub.i]) < 0, all states of trajectories [H.sub.i] of are negative, and reachable states would not intersect with the unsafe states region. It should be admitted that [B.sub.i]([[??].sub.i]) derived in Lemma 11 is conservative; however, for the safety of interconnected hybrid systems H, this conservatism is justified.

For the convenience of expression, output as well as feedback [mathematical expression not reproducible] is rewritten as

[mathematical expression not reproducible], (23)

where [mathematical expression not reproducible] denotes the 1st-row, 1st column element of vector [mathematical expression not reproducible] is a concatenation of vectors [[??].sup.c.sub.1], ..., [[??].sup.c.sub.M]. Additionally, [H.sub.i], [G.sub.i] are polynomial matrices; please distinguish them from the symbols

Lemma 13 (coupling constraints on interconnections). Let an interconnected I/O automaton H be given. For each interconnected individual hybrid system [H.sub.i], define H = [[H.sub.1.sup.T], ..., [H.sub.M.sup.T]] and G = [[G.sub.1.sup.T], ..., [G.sub.M.sup.T]], if there exists [GAMMA] = diag{[[gamma].sub.1], ..., [[gamma].sub.M]} > [0.sup.MxM] such that

[mathematical expression not reproducible] (24)

holds, where [[gamma].sub.1], ..., [[gamma].sub.M] [member of] [R.sub.>0]. Then there exits [mathematical expression not reproducible], satisfying

[mathematical expression not reproducible], (25)

for all i [member of] I.

Proof. Since there exists [GAMMA] = diag{[[gamma].sub.1], ..., [[gamma].sub.M]} > [0.sup.MxM] with [[gamma].sub.1], ..., [[gamma].sub.M] [member of] [R.sub.>0] such that G [cross product] [I.sup.rxr] [less than or equal to] [GAMMA][H.sup.T][K.sup.T]KH [cross product] [I.sup.rxr], it could be verified that each column of [mathematical expression not reproducible] through matrix computation; therefore, [mathematical expression not reproducible] stands. Under constraint (19), the rest is proved by contradiction. Assume that, [for all][[gamma].sub.i] [member of] [R.sub.>0] satisfying (24), [mathematical expression not reproducible] holds; then take [mathematical expression not reproducible], and derive [mathematical expression not reproducible], which is contradiction to constraint (19). Therefore, T satisfying (24) is sufficient for [mathematical expression not reproducible].

Remark 14. Note that if inequality constraint (24) is satisfied, then Lie-derivative of [B.sub.i]([[??].sub.i]) is negative definite under the constraint of [mathematical expression not reproducible] Those constraints imposed on interconnections are enlightened by the dissipation inequalities, which guarantees the structural stability of interconnected hybrid systems. It should be noticed that such dissipation-inequality-like constraints are imposed on nondefinite barrier functions, while dissipation inequalities impose constraints on positive-definite energy functions.

Theorem 15 (compositional barrier certificate for H). Let an interconnected hybrid I/O automaton H be given. For each interconnected individual hybrid system [H.sub.i], suppose that both [B.sub.i]([[??].sub.i]) satisfying constraints (17)-(20) in Lemma 11 and a vector r = diag{[[gamma].sub.1], ..., [[gamma].sub.M]} satisfying (24) in Lemma 13 have been found, if there exists a diagonal matrix D = diag{[d.sub.1], ..., [d.sub.M]} > [0.sup.MxM] such that

D (GK -T) + [(KG -[GAMMA]).sup.T] D [less than or equal to] 0, (26)

where [d.sub.1], ..., [d.sub.M] [member of] [R.sub.>0]; then H is safe.

Proof. Since [B.sub.i]([[??].sub.i])s satisfying (17)-(20) and [GAMMA] = diag{[[gamma].sub.1], ..., [[gamma].sub.M]} satisfying (24) exist, and there is a diagonal matrix D = diag{[d.sub.1], ..., [d.sub.M]} > [0.sup.MxM] satisfying (26), a compositional function B([??]) is built as

B([??]) = [summation over (i[member of]l)][[gamma].sub.i][B.sub.i]([[??].sub.i]). (27)

Since we have [mathematical expression not reproducible], it yields [mathematical expression not reproducible]. Similarly, [mathematical expression not reproducible] is derived. Through introducing (24) and (26), for all [??] [member of] X - [X.sup.u], we derive

[mathematical expression not reproducible]. (28)

Considering [for all]i [member of] D [for all][[??].sub.l] [member of] [G.sub.i]: [B.sub.i]([q.sup.k.sub.i]) [less than or equal to] [B.sub.i]([q.sup.j.sub.i]), where [q.sup.k.sub.i] [not equal to] [q.sup.j.sub.i], [q.sup.j.sub.i], [q.sup.k.sub.i] [member of] [Q.sub.i], we derive [mathematical expression not reproducible]; equivalently, B([??]) is nonincreasing at mode switchings. Therefore, B([??]) is the barrier certificate for H; furthermore, safety of H is guaranteed.

Remark 16. On the assumption of existences of barrier certificates for each [H.sub.i] and appropriate D = diag{[d.sub.1], ..., [d.sub.M]} > [0.sup.MxM], Lie-derivatives of each [B.sub.i]([[??].sub.i]) would be negative definite consistently. Then, B([??]) is negative definite along their trajectories of states under the restrictions of interconnections. Naturally, safety of H is guaranteed.

5. Computation of Barrier Certificates

In this section, we discuss how to construct compositional barrier certificates from the conditions set up in Section 4. Bilinear SOS programming is applied to support the computation of barrier certificates for H. H is defined on semialgebraic sets with all vector fields that are restricted to be polynomial equality as well as inequality. Here, we parameterize the barrier certificates [B.sub.i]([[??].sub.i])s as polynomials and require the state space and initial, unsafe, and guard sets to be given by polynomial equality or inequality constraints. Through applying generalized S-procedure, constraints in the forms of semialgebraic sets could be incorporated into constraints (17)-(20); then Lemma 11 is formulated as a bilinear SOS program (feasibility problem). With the help of numerical solvers such as SOSTOOLS [21] and SOSOPT [22], those barrier certificates could be computed automatically.

5.1. Computation of Individual Barrier Certificates for [H.sub.i]s. To compute individual barrier certificates, all the sets of states in (17)-(20) should be transformed into semialgebraic sets. Let [mathematical expression not reproducible] be given as vectors of polynomials [mathematical expression not reproducible], where those inequalities are satisfied entry-wise. For example, when X is defined as [mathematical expression not reproducible], it is equivalent to the semialgebraic set [mathematical expression not reproducible].

Generalized S-procedure is then introduced to corporate those semialgebraic sets constraints with (17)-(20) and Lemma 11 is formulated as a bilinear SOS program.

Lemma 17 (generalized S-procedure, see [24]). Given functions [mathematical expression not reproducible] such that [mathematical expression not reproducible], then it holds that

[mathematical expression not reproducible]. (29)

For more details on generalized S-procedure, please refer to [24].

Theorem 18 (barrier certificates as bilinear SOS program). Let an interconnected hybrid I/O automaton [H.sub.i] = {[X.sub.i], [U.sub.i], [Y.sub.i], [S.sub.i], [Q.sub.i], [G.sub.i], [F.sub.i], [F.sub.i], [T.sub.i], [X.sup.0.sub.i], [X.sup.u.sub.i]} be given, and [X.sub.i], [X.sup.0.sub.i], [X.sup.u.sub.i], [G.sub.i] have been transformed into semialgebraic sets. The polynomial barrier certificate [B.sub.i]([[??].sub.i]) could be computed through solving the following bilinear SOS program:

[mathematical expression not reproducible], (30)

[mathematical expression not reproducible], (31)

[mathematical expression not reproducible] (32)

[mathematical expression not reproducible], (33)

where [[lambda].sub.i]([[??].sub.i]) [member of] [P.sub.n] is a polynomial decision variable, [[member of].sub.i], [v.sub.i] [member of] [R.sub.>0] are scalar decision variables, and [mathematical expression not reproducible] are all SOS polynomial decision variables.

Proof. Notice that there exists a coupling between the polynomial decision variables [[lambda].sub.i]([[??].sub.i]) and [B.sub.i]([[??].sub.i]), and this programming problem is bilinear. Here is the sketch of a proof. Since [mathematical expression not reproducible], the positive definiteness could be guaranteed by [mathematical expression not reproducible] by applying generalized S-procedure. Similarly, (31)-(33) could be derived. Scalar ] decision variable introduced in (33) is for the switching. Therefore, [B.sub.i]([[??].sub.i]) derived by solving the bilinear SOS program satisfying (30)-(33) is a barrier certificate for [H.sub.i].

Remark 19. Loosely speaking, generalized S-procedure is for determining satisfaction of an inequality constraint [p.sub.0]([??]) [greater than or equal to] 0 when other inequality constraints [p.sub.1]([??]) [greater than or equal to] 0, ..., [p.sub.m]([??]) [greater than or equal to] 0 are fulfilled. Through applying generalized S-procedure, the above theorem formulates inequalities (30)-(33) together as a bilinear SOS program computationally tractable for the feasibility of barrier certificates constrained by (17)-(20).

5.2. Computation of Compositional Barrier Certificate for H. In order to derive the compositional barrier certificate for H, r should be estimated first by solving the following optimization problem:

[mathematical expression not reproducible] (34)

The above optimization is a linear program problem which could be solved with the help of linear programming solvers. With derived r, compositional barrier certificates for H could be computed directly by solving a bilinear SOS program.

Theorem 20 (compositional barrier certificate for H as bilinear SOS program). Let an interconnected hybrid I/O automaton H be given. For each interconnected H;, there exists an individual barrier certificate Bi(xi); then, the compositional barrier certificate B(x) could be computed through solving the following bilinear SOS program:

Min D = diag [[d.sub.1], ..., [d.sub.m]} (35)

[mathematical expression not reproducible] (36)

[mathematical expression not reproducible], (37)

[mathematical expression not reproducible] (38)

D > [0.sup.mxm], (39)

where [mathematical expression not reproducible]. D is a scalar matrix decision variable, [member of] = [[[member of].sub.1], ..., [[member of].sub.m]] is a scalar vectorial decision variable, [s.sub.1]([??]), [s.sub.2]([??]) are SOS polynomials decision variables, and p([??]) is a polynomial decision variable.

Proof. Here is the sketch of a proof. As indicated in the above theorem, [B.sub.1]([[??].sub.1]), ..., [B.sub.m]([[??].sub.m]) are barrier certificates for [H.sub.i]s. Constraints (36) and (37) imply that B(x) is nonpositive on [X.sup.u] and positive on [X.sup.s] = X - [X.sup.u]. Constraints (38) and (39) imply that

[mathematical expression not reproducible]. (40)

In conclusion, the derived B([??]) satisfies Theorem 15, and B([??]) is the compositional barrier certificate for H; thus, H is safe.

Remark 21. Since p([??]) is coupled with D, the above programming problem satisfying (36)-(39) is a bilinear SOS program. Theorem 20 then formulates the construction of a compositional barrier certificate as a feasibility problem in bilinear SOS problem. It should be noted that compositional barrier certificates derived by Theorem 20 are more conservative than that by Theorem 15; however, Theorem 20 provides a theoretically tractable method to construct compositional barrier certificates. Numerical solvers such as SOSTOOLS or SOSOPT for MATLAB could be used for solving bilinear SOS program automatically. More details on the issues of numerical computation are omitted; we strongly suggest that readers refer to [21] or [22].

6. Example

In this example, we consider the following interconnected hybrid systems H consisting of two coupled hybrid systems [H.sub.1], [H.sub.2]:

[mathematical expression not reproducible], (41)

where [[??].sup.0.sub.1], [[??].sup.0.sub.2] are admissible initial states, [[??].sup.u.sub.1], [[??].sup.u.sub.1] are unsafe states, and inequalities [x.sub.11] [x.sub.12] < 0, [x.sub.11][x.sub.12] [greater than or equal to] 0, [x.sub.21][x.sub.22] < 0, and [x.sub.21][x.sub.22] [greater than or equal to] 0 are switching conditions. [A.sub.1], [A.sub.2] and [B.sub.1], [B.sub.2] are modes of [H.sub.1] and [H.sub.2], respectively. [[??].sub.1], [[??].sub.2] are interconnection matrices. The derived barrier certificate is -0.01[x.sup.3.sub.11] - 1.88[x.sup.2.sub.11][x.sub.12] - 0.3[x.sup.2.sub.11][x.sub.21] - 476A2[x.sup.2.sub.11] + 5.77[x.sub.11][x.sup.2.sub.12] - 0.03[x.sub.11][x.sub.12][x.sub.21] - 0.03[x.sub.11][x.sub.12][x.sub.22] + 77.25[x.sub.11][x.sub.12] - 16.43[x.sub.11][x.sup.2.sub.21] + 0.03[x.sub.11][x.sub.21][x.sub.22] + 475.47[x.sub.11][x.sub.21] 0.51[x.sub.11] - 0.01[x.sup.3.sub.12] + 0.02[x.sup.2.sub.12][x.sub.21] - 0.42[x.sup.2.sub.12][x.sup.2.sub.22] - 154.77[x.sup.2.sub.12] + 102[x.sub.12][x.sub.22] + 1.12[x.sub.12] + 1.85[x.sup.2.sub.21][x.sub.22] + 191.09[x.sup.2.sub.21] + 1.95[x.sub.21][x.sup.2.sub.22] 27.16[x.sub.21][x.sub.22] + 1.21[x.sub.21] -0.01[x.sup.3.sub.22] -65.95[x.sup.2.sub.22] +1.48[x.sub.22] -1847.27. The software environment to test our method consists of SOSTOOLS and SeDuMi on MATLAB (R2013b) and monomials whose coefficients less than 0.01 are omitted. Since the barrier certificate exists, safety of H is verified.

7. Conclusion

In this paper, we have considered a network of interconnected hybrid systems with a safety constraint. We proposed a numerical method for verifying safety by constructing a compositional barrier certificate comprised of individual barrier certificates for each subsystem. The constructed compositional barrier function certifies global safety using individual barrier certificates and diagonal stability property of the network interconnection. Such a compositional barrier certificate is then formulated into a bilinear SOS program that is computationally tractable. With the help of numerical solvers such as SOSTOOLS and SOSOPT, safety verification of interconnected hybrid systems could be automatically accomplished. In the end, a numerical example is presented to show the validity of the proposed method.

http://dx.doi.org/ 10.1155/2016/4149059

Competing Interests

The authors declare that there is no conflict of interests regarding the publication of this paper.

Acknowledgments

The work is partially supported by the projects funded by the NSFC Key Project 61332008, NSFC Creative Team 61321064, NSFC 61572195. The Shanghai Trustworthy Computing Key Lab is supported by Shanghai Knowledge Service Platform ZF 1213. Jing Liuwould like to acknowledge the support of NSFC 91418203 and Shanghai Project (14511100400), NSFC Trustworthy Software Track 91318301. Miaomiao Zhang would like to acknowledge the support of NSFC 61472279.

References

[1] S. Prajna and A. Jadbabaie, "Safety verification of hybrid systems using barrier certificates," in Hybrid Systems: Computation and Control: 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004. Proceedings, vol. 2993 of Lecture Notes in Computer Science, pp. 477-492, Springer, Berlin, Germany, 2004.

[2] H. Gueguen, M.-A. Lefebvre, J. Zaytoon, and O. Nasri, "Safety verification and reachability analysis for hybrid systems," Annual Reviews in Control, vol. 33, no. 1, pp. 25-36, 2009.

[3] M. Anghel, F. Milano, and A. Papachristodoulou, "Algorithmic construction of Lyapunov functions for power system stability analysis," IEEE Transactions on Circuits and Systems I: Regular Papers, vol. 60, no. 9, pp. 2533-2546, 2013.

[4] A. Y. Sendjaja and V. Kariwala, "Achievable PID performance using sums of squares programming," Journal of Process Control, vol. 19, no. 6, pp. 1061-1065, 2009.

[5] S. Sankaranarayanan, H. B. Sipma, and Z. Manna, "Constructing invariants for hybrid systems," Formal Methods in System Design, vol. 32, no. 1, pp. 25-55, 2008.

[6] S. Sankaranarayanan, "Automatic invariant generation for hybrid systems using ideal fixed points," in Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control (HSCC '10), pp. 221-230, Stockholm, Sweden, April 2010.

[7] E. Rodrlguez-Carbonell and A. Tiwari, "Generating polynomial invariants for hybrid systems," in Hybrid Systems: Computation and Control: 8th International Workshop, HSCC 2005, Zurich, Switzerland, March 9-11, 2005. Proceedings, vol. 3414 of Lecture Notes in Computer Science, pp. 590-605, Springer, Berlin, Germany, 2005.

[8] P. A. Parrilo, Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization [Ph.D. thesis], California Institute of Technology, 2000.

[9] S. Prajna and A. Papachristodoulou, "Analysis of switched and hybrid systems-beyond piecewise quadratic methods," in Proceedings of the American Control Conference (ACC '03), vol. 4, pp. 2779-2784, IEEE, Denver, Colo, USA, June 2003.

[10] A. Papachristodoulou, "Analysis of nonlinear time-delay systems using the sum of squares decomposition," in Proceedings of the American Control Conference (ACC '04), vol. 5, pp. 4153-4158, IEEE, Boston, Mass, USA, July 2004.

[11] A. Papachristodoulou, M. M. Peet, and S. Lall, "Analysis of polynomial systems with time delays via the sum of squares decomposition," IEEE Transactions on Automatic Control, vol. 54, no. 5, pp. 1058-1064, 2009.

[12] S. Prajna, A. Jadbabaie, and G. J. Pappas, "A framework for worst-case and stochastic safety verification using barrier certificates," IEEE Transactions on Automatic Control, vol. 52, no. 8, pp. 1415-1428, 2007.

[13] C. Sloth, G. J. Pappas, and R. Wisniewski, "Compositional safety analysis using barrier certificates," in Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control (HSCC '12), pp. 15-24, Beijing, China, April 2012.

[14] C. Sloth, R. Wisniewski, and G. J. Pappas, "On the existence of compositional barrier certificates," in Proceedings of the 51st IEEE Conference on Decision and Control (CDC '12), pp. 4580-4585, Maui, Hawaii, USA, December 2012.

[15] H. Kong, X. Song, D. Han, M. Gu, and J. Sun, "A new barrier certificate for safety verification of hybrid systems," The Computer Journal, vol. 57, no. 7, pp. 1033-1045, 2014.

[16] R. Wisniewski and C. Sloth, "Converse barrier certificate theorem," in Proceedings of the IEEE 52nd Annual Conference on Decision and Control (CDC '13), pp. 4713-4718, IEEE, Firenze, Italy, December 2013.

[17] R. Alur, "Formal verification of hybrid systems," in Proceedings of the International Conference on Embedded Software (EMSOFT '11), pp. 273-278, IEEE, 2011.

[18] S. Coogan and M. Arcak, "Verifying safety of interconnected passive systems using SOS programming," in Proceedings of the 52nd IEEE Conference on Decision and Control (CDC '13), pp. 5951-5956, Firenze, Italy, December 2013.

[19] S. Coogan and M. Arcak, "A dissipativity approach to safety verification for interconnected systems," Institute of Electrical and Electronics Engineers. Transactions on Automatic Control, vol. 60, no. 6, pp. 1722-1727, 2015.

[20] G. H. Hines, M. Arcak, and A. K. Packard, "Equilibrium-independent passivity: a new definition and numerical certification," Automatica, vol. 47, no. 9, pp. 1949-1956, 2011.

[21] A. Papachristodoulou, J. Anderson, G. Valmorbida, S. Prajna, P. Seiler, and P. Parrilo, "SOSTOOLS version 3.00 sum of squares optimization toolbox for MATLAB," http://arxiv.org/abs/1310.4716.

[22] P. Seiler, "Sosopt: a toolbox for polynomial optimization," http:// arxiv.org/abs/1308.1889.

[23] N. Lynch, R. Segala, and F. Vaandrager, "Hybrid I/O automata," Information and Computation, vol. 185, no. 1, pp. 105-157, 2003.

[24] Z. Jarvis-Wloszek, R. Feeley, W. Tan, K. Sun, and A. Packard, "Control applications of sum of squares programming," in Positive Polynomials in Control, vol. 312, pp. 3-22, Springer, Berlin, Germany, 2005.

Guobin Wang, (1,2) Jifeng He, (1,2) Jing Liu, (1,2) Haiying Sun, (1,2) Zuohua Ding, (3) and Miaomiao Zhang (4)

(1) Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China

(2) National Trustworthy Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai 200062, China

(3) School of Informatics and Electronics, Zhejiang Sci-Tech University, Hangzhou 310018, China

(4) School of Software Engineering, Tongji University, Shanghai 201804, China

Correspondence should be addressed to Jing Liu; jliu@sei.ecnu.edu.cn

Received 23 October 2015; Accepted 26 January 2016