# Safety Verification of Interconnected Hybrid Systems Using Barrier Certificates

Authors: Guobin Wang; Jifeng He; Jing Liu; Haiying Sun; Zuohua Ding; Miaomiao Zhang
Journal: Mathematical Problems in Engineering
 (2016)

---

## Abstract

Safety verification determines whether any trajectory starting from admissible initial states would intersect with a set of unsafe states. In this paper, we propose a numerical method for verifying safety of a network of interconnected hybrid dynamical systems with a state constraint based on bilinear sum-of-squares programming. The safety verification is conducted by the construction of a function of states called barrier certificate. We consider a finite number of interconnected hybrid systems satisfying the input-to-state property and the networked interconnections satisfying a dissipativity property. Through constructing a barrier certificate for each subsystem and imposing dissipation-inequality-like constraints on the interconnections, safety verification is formulated as a bilinear sum-of-squares feasibility problem. As a result, safety of the interconnected hybrid systems could be determined by solving an optimization problem, rather than solving differential equations. The proposed method makes it possible to verify the safety of interconnected hybrid systems, which is demonstrated by a numerical example.


---

## Body

## 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. Section2 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
n stand for the n-dimensional real vector space. R
>
0
,
N
>
0 refer to the sets of positive real numbers and positive natural numbers, respectively. Lower case alphabets such as i
,
j
,
k
,
l
,
m
,
n represent variables, while symbols such as x
→
,
u
→
,
y
→ are vectorial variables. · refers to the Euclidean vector norm. For matrices or vectors, the superscript “T” denotes matrix transposition. I
m
×
m is the identity matrix, 0
→ denotes zero vector, 0 is scalar, and 0
m
×
n is an m
×
n zero matrix. The notation diag
⁡
{
·
} indicates a square diagonal matrix with the arguments along the diagonal. A
-
1 is the inverse of matrix A.Definition 1 (positive-definite polynomial and its Lie-derivative).
Letx
→ denote the n-tuple (
x
1
,
…
,
x
n
), P
n
m will be taken as the polynomial field over variables in x
→ with the highest degree of m, and a polynomial function p
(
x
→
)
∈
P
n
m is said to be positive definite iff(1)
p
x
→
>
0for all x
→
∈
R
n
∖
{
0
→
} with p
(
0
→
)
=
0. The first-order Lie-derivative of p
(
x
→
) along a continuous flow f
(
x
→
)
=
(
f
1
(
x
→
)
,
…
,
f
n
(
x
→
)
) is as follows:(2)
L
f
x
→
p
x
→
=
∑
i
n
∂
p
x
→
∂
x
i
f
i
x
→
.Definition 2 (SOS polynomial).
A multivariate polynomialp
(
x
→
) is an SOS polynomial if there exist finite polynomials p
1
(
x
→
)
,
…
,
p
k
(
x
→
) such that(3)
p
x
→
=
∑
i
=
1
k
p
i
2
x
→
.Let Σ
n
2
m (Σ
n for short) denote the set of all SOS polynomials in x
→ under the degree of 2
m.Definition 3 (semialgebraic set).
A set{
x
→
∈
R
n
:
p
1
(
x
→
)
≥
0
,
…
,
p
s
(
x
→
)
≥
0
} is called a semialgebraic set iff p
1
(
x
→
)
,
…
,
p
s
(
x
→
)
∈
P
n
m and s
∈
N
>
0 is finite.Definition 4 (K polynomial function).
A polynomial functionα
(
x
→
)
:
R
≥
0
→
R
≥
0 is of class K; equivalently α
(
x
→
)
∈
P
n
m
∩
K, if it is strictly increasing and α
(
0
→
)
=
0.Definition 5 (Kronecker product).
LetA
=
[
a
i
,
j
]
∈
R
m
×
n, B
∈
R
p
×
q denote two matrices, and then the Kronecker product of A and B is defined as the matrix:(4)
A
⊗
B
=
a
1,1
B
⋯
a
1
,
n
B
⋮
⋱
⋮
a
m
,
1
B
⋯
a
m
,
n
B
.Definition 6 (≤ for matrices).
For two matricesA
=
[
a
i
,
j
]
∈
R
m
×
n, B
=
[
b
i
,
j
]
∈
R
m
×
n, A
≤
B if and only if(5)
a
i
,
j
≤
b
i
,
j
∀
1
≤
i
≤
m
,
1
≤
j
≤
n
.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(6)
M
i
n
scalar  variable
t
s.t.
t
b
k
x
→
,
d
→
-
a
k
x
→
,
d
→
∈
Σ
n
,
k
=
1
,
…
,
N
g
b
k
x
→
,
d
→
∈
Σ
n
,
k
=
1
,
…
,
N
g
c
j
x
→
,
d
→
=
0
,
k
=
1
,
…
,
N
e
,where t
∈
R, x
→
∈
R
n, and d
→
∈
R
r are decision variables. {
a
k
(
x
→
,
d
→
)
}, b
k
(
x
→
,
d
→
), c
j
x
→
,
d
→ are polynomials with given data and affine in d
→.


## 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
i
∈
I indexed by the finite set I. 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 automatonH
i of H is a tuple H
i
=
{
X
i
,
U
i
,
Y
i
,
S
i
,
Q
i
,
G
i
,
F
i
,
T
i
,
X
i
0
,
X
i
u
} with the following components: (i)
X
i
⊆
R
n
i is a set of real-valued system internal variables x
→
i
∈
X
i. The number n
i is called the dimension of H
i.
(ii)
U
i
⊆
R
r is a set of real-valued system external inputs u
→
i
c
,
u
→
i
d
∈
U
i, where u
→
i
c denotes the continuous input while u
→
i
d denotes the discrete input. U
i is disjoint from X
i.
(iii)
Y
i
⊆
R
r is a set of real-valued system external outputs y
→
i
c
,
y
→
i
d
∈
Y
i, where y
→
i
c denotes the continuous output while y
→
i
d denotes the discrete output. Y
i is disjoint from X
i
∪
U
i.
(iv)
S
i is a finite set of indexes of switching signals. The index function σ
(
t
)
:
[
0
,
T
]
→
S
i
=
{
1
i
,
…
,
j
i
,
l
i
,
…
,
s
i
} denotes the sequence of activated switching signals S
i over the continuous-time interval [
0
,
T
].
(v)
Q
i is a finite set of modes. The overall state space of individual hybrid systems H
i is Q
i
×
X
i, and a state is denoted by (
q
i
,
x
→
i
)
∈
Q
i
×
X
i. q
i
j
,
q
i
k
∈
Q
i denote different modes of H
i when j
≠
k.
(vi)
G
i
⊆
X
i is the set of guard conditions for H
i. A switching is enabled at t
i
⋆ once x
→
i
(
t
i
⋆
)
∈
G
i holds, namely, a state-dependent switching. Throughout this paper, all switchings of H
i are assumed to be state-dependent. Furthermore, C
i is taken as the complement of G
i (C
i
=
X
i
-
G
i).
(vii)
F
i
:
C
i
→
2
X
i is a set of continuous vector fields. For each state (
q
i
,
x
→
i
)
∈
Q
i
×
X
i, F
i incorporates a differential constraint on the continuous evolution according to the differential equation:(7)
x
→
i
˙
=
f
i
σ
i
t
i
t
i
,
x
→
i
t
i
,
u
→
i
c
,where x
→
∈
C
i, t
i
∈
(
t
i
k
-
1
,
t
i
k
], k
∈
N
>
0, and σ
i
(
t
i
)
∈
S
i.
(viii)
T
i
:
Q
i
×
G
i
×
S
→
Q
i is a relation capturing discrete switchings between two modes. Here a switching (
q
i
j
,
x
→
i
(
t
i
⋆
)
,
σ
i
(
t
i
⋆
)
)
→
x
→
i
(
t
i
⋆
)
∈
G
i
q
i
k indicates that from mode q
i
j, H
i can undergo a switching to the mode q
i
k at the instant t
i
⋆. Only finite switchings are allowed over finite-time intervals.
(ix)
X
i
0
⊆
X is the set of admissible initial states of H
i.
(x)
X
i
u
⊆
X is the set of unsafe states of H
i.Trajectories ofH
i start from the admissible initial states x
→
i
0 and are concatenations of a sequence of continuous evolutions in x
→
i and discrete switchings among different modes q
i
j
,
q
i
k
∈
Q
i satisfying the following.Initiation. x
→
i
0
∈
X
i
0 is an admissible initial state of H
i.Discrete Consecution. At the instant t
i
⋆
:
x
→
i
(
t
i
⋆
)
∈
G
i, the switching signal σ
i
(
t
i
⋆
)
∈
S
i
(8)
q
i
j
,
x
→
i
t
i
⋆
,
σ
i
t
i
⋆
→
x
→
i
t
i
⋆
∈
G
i
q
i
k
⟹
lim
t
i
→
t
i
⋆
-
⁡
q
i
σ
i
t
i
=
q
i
j
∧
lim
t
i
→
t
i
⋆
+
⁡
q
i
σ
i
t
i
=
q
i
kactivates and produces a discrete output according to(9)
y
→
i
d
t
i
⋆
=
h
i
d
t
i
⋆
,
x
→
i
t
i
⋆simultaneously.Continuous Consecution. For an activating mode q
i
j
∈
Q
i over the [
t
i
k
,
t
i
k
+
1
)
(10)
x
→
i
t
i
∈
C
i
∧
x
→
i
˙
=
f
i
q
i
j
t
i
,
x
→
i
t
i
,
u
→
i
c
∀
t
i
∈
t
i
k
,
t
i
k
+
1holds and produces continuous outputs according to(11)
y
→
i
c
t
i
=
h
i
c
t
i
,
x
→
i
t
i
∀
t
i
∈
t
i
k
,
t
i
k
+
1over the continuous interval.Here,t
i
⋆
- denotes the left limit of t
i
⋆ and t
i
⋆
+ denotes its right limit. Additionally, f
i
(
t
i
,
x
→
i
,
u
→
i
c
)s, h
c
(
t
i
,
x
→
i
(
t
i
)
)s, and h
d
(
t
i
,
x
→
i
(
t
i
)
)s are all restricted to polynomials throughout this paper.Compositional hybrid I/O automatonH is given as an interconnection of finite individual hybrid I/O automaton consisting of assignments relating the inputs and outputs of interconnected H
i.Definition 9 (compositional hybrid I/O automaton).
A compositional hybrid I/O automatonH is a finite set of interconnected hybrid I/O automata H
i indexed by i
∈
I. Formally, H is a tuple H
=
{
I
,
⋃
i
∈
I
{
H
i
}
,
N
c
,
N
d
,
K
} with the following components: (i)
I is a finite set of indexes of interconnected hybrid automaton {
H
i
}. Without loss of generality, we assume I has M
∈
N
>
0 elements.
(ii)
⋃
i
∈
I
{
H
i
} is a finite set of interconnected hybrid I/O automata. X
,
U
,
Y
,
S
,
Q
,
F
,
T
,
X
0
,
X
u of H are the Cartesian products of each corresponding item of all individual H
is, respectively. Particularly, G
=
{
〈
x
→
1
,
…
,
x
→
i
,
…
,
x
→
M
〉
∈
X
:
∃
i
∈
I
,
x
→
i
∈
G
i
}, which means x
→
∈
G if there exists an x
→
i of H
i which intersects corresponding guard G
i. Dually, C
⊆
X is defined as {
〈
x
→
1
,
…
,
x
→
i
,
…
,
x
→
M
〉
∈
X
:
∀
i
∈
I
,
x
→
i
∈
C
i
}. 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
×
M matrix K
=
[
a
j
,
k
]
M
×
M, a
j
,
k
∈
{
0,1
}, 1
≤
j, k
≤
M.
(iv)
N
c is a finite set of interconnections following continuous assignments(12)
u
→
i
c
=
g
i
c
a
i
,
1
·
y
→
1
c
,
…
,
0
·
y
→
i
c
,
…
,
a
i
,
M
·
y
→
M
cover continuous-time intervals, where u
→
i
c is the interconnection over a continuous-time interval. [
a
i
,
1
,
…
,
a
i
,
M
] is the ith row of K. g
i
c
(
y
→
1
c
,
…
,
y
→
i
^
c
,
…
,
y
→
M
c
)s are assumed to be polynomial functions.
(v)
N
d is a finite set of interconnections following discrete assignments(13)
u
→
i
d
=
g
i
d
a
i
,
1
·
y
→
1
d
,
…
,
0
·
y
→
i
d
,
…
,
a
i
,
M
·
y
→
M
dat discrete instants, where u
→
i
d is the interconnection at switching instant, and [
a
i
,
1
,
…
,
a
i
,
M
] is the ith row of K. g
i
d
(
y
→
1
d
,
…
,
d
→
i
^
c
,
…
,
d
→
M
c
)s are assumed to be polynomial functions.Intuitively, trajectory ofH is the composition of trajectories of H
is under restrictions of the interconnections. We take ϕ
i
(
t
i
,
x
→
i
0
,
x
→
i
,
u
→
i
c
,
u
→
i
d
,
y
→
i
c
,
y
→
i
d
) to represent the trajectory of H
i; thus, the trajectory ϕ
(
t
,
x
→
0
,
x
→
,
u
→
c
,
u
→
d
,
y
→
c
,
y
→
d
) of H is a Cartesian product satisfying the following.Initiation.
x
→
0
=
〈
x
→
1
0
,
…
,
x
→
M
0
〉
∈
X
0 for all x
→
i
0
∈
X
i
0.Discrete Consecution. For x
→
∈
G, at least one ϕ
i
(
t
i
,
x
→
i
0
,
x
→
i
,
u
→
i
c
,
u
→
i
d
,
y
→
i
c
,
y
→
i
d
) 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:(14)
u
→
1
d
=
g
i
d
0
·
y
→
1
d
,
…
,
a
1
,
i
·
y
→
i
d
,
…
,
a
1
,
M
·
y
→
M
d
,
a
1,1
,
…
,
a
1
,
M
∈
0,1
⋮
u
→
M
d
=
g
i
d
a
M
,
1
·
y
→
1
d
,
…
,
a
M
,
i
·
y
→
i
d
,
…
,
0
·
y
→
M
d
,
a
M
,
1
,
…
,
a
M
,
M
∈
0,1
.Continuous Consecution. For x
→
∈
C, states of all trajectories of H
i evolve continuously under the continuous interconnections according to the following differential equations:(15)
u
→
1
c
=
g
i
c
0
·
y
→
1
c
,
…
,
a
1
,
i
·
y
→
i
c
,
…
,
a
1
,
M
·
y
→
M
c
,
a
1,1
,
…
,
a
1
,
M
∈
0,1
⋮
u
→
M
c
=
g
i
c
a
M
,
1
·
y
→
1
c
,
…
,
a
M
,
i
·
y
→
i
c
,
…
,
0
·
y
→
M
c
,
a
M
,
1
,
…
,
a
M
,
M
∈
0,1
.For compositional hybrid I/O automataH, x
→
∈
X evolves continuously when all trajectories of H
is evolve continuously, while switchings occur once there exists a discrete consecution among H
is.Based on the concept of trajectories ofH, safety of H could be formalized as follows.Definition 10 (safety ofH).
Let an interconnected hybrid I/O automatonH
=
{
I
,
⋃
i
∈
I
{
H
i
}
,
N
c
,
N
d
,
K
} be given. Take ϕ
(
t
,
x
→
0
,
x
→
,
u
→
c
,
u
→
d
,
y
→
c
,
y
→
d
) as the trajectory of H; then H is unsafe if there exists an instant t
i
⋆
∈
[
0
,
T
] such that ∀
t
∈
[
0
,
T
]
:
ϕ
(
t
,
x
→
0
,
x
→
,
u
→
c
,
u
→
d
,
y
→
c
,
y
→
d
)
∈
X
(16)
∃
u
→
c
:
ϕ
t
⋆
,
x
→
0
,
x
→
t
i
⋆
,
u
→
c
t
⋆
∈
X
u
∪
∃
u
→
d
:
ϕ
i
t
⋆
,
x
→
0
,
x
→
t
i
⋆
,
u
→
d
t
⋆
∈
X
uholds. Furthermore, H is safe when none of the trajectories of H starting from admissible initial states would intersect unsafe states X
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 certificateB
:
X
→
→
R (X
→ 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 x
→
∈
X
→ satisfying B
(
x
→
)
=
0 form a barrier separating all unsafe states from possible system trajectories. B
(
x
→
) takes different values on different regions: for example, for each x
→
∈
X
u (X
u denotes unsafe states region), it satisfies B
x
→
>
0, while for each x
→
∈
X
s (X
s denotes reachable states region of trajectories) B
(
x
→
≤
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.Figure 1
Intuitive interpretation of barrier certificates.


### 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 forH
i).
Let an interconnected individual hybrid I/O automatonH
i
=
{
X
i
,
U
i
,
Y
i
,
S
i
,
Q
i
,
G
i
,
F
i
,
T
i
,
X
i
0
,
X
i
u
} be given. For each u
→
i
c
,
u
→
i
d
∈
U
i, suppose there exists a function B
i
(
x
→
i
) for all m
i modes of H
i. B
i
(
x
→
i
) is piecewise differentiable with respect to its state variable and satisfies(17)
B
i
x
→
i
>
0
,
∀
x
→
i
∈
X
i
u
,
(18)
B
i
x
→
i
≤
0
,
∀
x
→
i
∈
X
i
0
,
(19)
∂
B
i
x
→
i
∂
x
→
i
f
i
j
t
i
,
x
→
i
t
i
,
u
→
i
c
≤
0
,
∀
x
→
i
∈
X
i
∧
B
i
x
→
i
=
0
,
(20)
B
i
q
i
k
≤
B
i
q
i
j
,
∀
x
→
i
∈
G
i
,
q
i
k
≠
q
i
j
,
q
i
j
,
q
i
k
∈
Q
i
,where, for the case in (20), H
i undergoes a switching from mode q
i
j to mode q
i
k. If such B
i
(
x
→
i
) exists, then the safety of H
i is guaranteed.Proof (by contradiction).
For eachu
→
i
c, assume that barrier certificates B
i
j
(
x
→
i
) satisfying (17)–(20) can be found and suppose there exists an instant t
i
⋆
∈
[
0
,
T
] when x
→
i
(
t
i
⋆
)
∈
X
i
u. Suppose there exist two sequences of instants 0
=
t
i
0
<
t
i
1
<
⋯
<
t
i
p
i
=
t
i
⋆ and 0
=
t
0
<
t
1
<
⋯
<
t
p
=
t
i
⋆. p
i
,
p
∈
N
>
0 are either finite or infinite. At each t
i
p
i, mode q
i
p
i
∈
Q
i is activated, while, at each t
p, an impulsive interconnection rather than the continuous-time interconnection is activated. From (17), we derive B
i
q
i
p
i
(
x
→
i
(
t
⋆
)
)
>
0. The impulsive interconnection u
→
i
d could be omitted considering(21)
∑
l
=
1
p
∫
t
l
t
l
∂
B
i
x
→
i
∂
x
→
i
f
i
j
t
i
,
x
→
i
t
i
,
u
→
i
d
=
0for any finite p. And from (20), it concludes that B
i
(
x
→
i
) decreases at each switching. Over the continuous-time interval [
0
,
t
i
⋆
], we have(22)
B
i
x
→
i
t
i
⋆
=
B
i
x
→
i
t
i
0
+
∑
l
=
1
p
i
∫
t
i
l
t
i
l
+
1
∂
B
i
j
x
→
i
∂
x
→
i
f
i
j
t
i
,
x
→
i
t
i
,
u
→
i
c
+
∑
l
=
1
p
u
→
i
d
T
f
i
j
t
i
,
x
→
i
t
i
+
∑
l
=
1
p
B
i
x
→
i
-
B
i
l
x
→
i
≤
B
i
x
→
i
t
i
0
+
∑
l
=
1
p
i
∫
t
i
l
t
i
l
+
1
∂
B
i
x
→
i
∂
x
→
i
f
i
j
t
i
,
x
→
i
t
i
,
u
→
i
c
≤
B
i
x
→
i
t
i
0
+
∑
l
=
1
p
i
ln
⁡
B
i
x
→
i
t
i
l
+
1
-
ln
⁡
B
i
x
→
i
t
i
l
≤
B
i
x
→
i
t
i
0
≤
0
.Therefore, the derived B
i
(
x
→
i
(
t
i
⋆
)
)
≤
0 contradicts the assumption B
i
(
x
→
i
(
t
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
i
(
x
→
i
) is sufficient for safety of H
i.Remark 12.
Intuitively, the value ofB
i
(
x
→
i
) decreases along both continuous flows as well as switchings, since B
i
(
x
→
i
0
)
<
0, all states of trajectories of H
i are negative, and reachable states would not intersect with the unsafe states region. It should be admitted that B
i
(
x
→
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 feedbackh
i
c
(
x
→
i
), g
i
c
(
y
→
1
c
,
…
,
y
→
M
c
) is rewritten as(23)
h
i
c
x
→
i
g
i
c
y
→
1
c
,
…
,
y
→
M
c
H
i
=
h
1,1
⋯
h
1
,
M
i
⋮
⋱
⋮
h
M
i
,
1
⋯
h
M
i
,
M
x
1,1
i
⋮
x
M
i
,
1
i
G
i
=
g
1,1
⋯
g
1
,
M
⋮
⋱
⋮
g
M
,
1
⋯
g
M
,
M
y
→
1
c
⋮
y
→
M
c
,where x
→
i
=
[
x
1,1
i
,
…
,
x
M
i
,
1
i
]
T (x
1,1
i denotes the 1st-row, 1st-column element of vector x
→
i) and [
y
→
1
c
,
…
,
y
→
M
c
]
T is a concatenation of vectors y
→
1
c
,
…
,
y
→
M
c. Additionally, H
i
,
G
i are polynomial matrices; please distinguish them from the symbols H
i
,
G
i.Lemma 13 (coupling constraints on interconnections).
Let an interconnected I/O automatonH be given. For each interconnected individual hybrid system H
i, define H
=
[
H
1
T
,
…
,
H
M
T
] and G
=
[
G
1
T
,
…
,
G
M
T
], if there exists Γ
=
diag
⁡
{
γ
1
,
…
,
γ
M
}
>
0
M
×
M such that(24)
G
⊗
I
r
×
r
≤
Γ
H
T
K
T
K
H
⊗
I
r
×
rholds, where γ
1
,
…
,
γ
M
∈
R
>
0. Then there exits u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c
≤
0, ∀
i
=
1,2
,
…
,
M, satisfying(25)
∂
B
i
x
→
i
∂
x
→
i
f
i
j
t
i
,
x
→
i
t
i
,
u
→
i
c
≤
u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c
,
∀
x
→
i
∈
X
i
∧
B
i
x
→
i
=
0for all i
∈
I.Proof.
Since there existsΓ
=
diag
⁡
{
γ
1
,
…
,
γ
M
}
>
0
M
×
M with γ
1
,
…
,
γ
M
∈
R
>
0 such that G
⊗
I
r
×
r
≤
Γ
H
T
K
T
K
H
⊗
I
r
×
r, it could be verified that each column of G
⊗
I
r
×
r
≤
Γ
H
T
K
T
K
H
⊗
I
r
×
r
=
u
→
c
T
y
→
c
-
Γ
y
→
c
T
y
→
c
≤
0 through matrix computation; therefore, ∀
i
∈
I
:
u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c stands. Under constraint (19), the rest is proved by contradiction. Assume that, ∀
γ
i
∈
R
>
0 satisfying (24), (
∂
B
i
x
→
i
/
∂
x
→
i
)
f
i
j
(
t
i
,
x
→
i
(
t
i
)
,
u
→
i
c
)
≥
u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c holds; then take Γ
=
(
y
→
c
)
-
1
u
→
c
T, and derive (
∂
B
i
x
→
i
/
∂
x
→
i
)
f
i
j
(
t
i
,
x
→
i
(
t
i
)
,
u
→
i
c
)
≥
0, which is contradiction to constraint (19). Therefore, Γ satisfying (24) is sufficient for (
∂
B
i
x
→
i
/
∂
x
→
i
)
f
i
j
(
t
i
,
x
→
i
(
t
i
)
,
u
→
i
c
)
≤
u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c
,
∀
x
→
i
∈
X
i
∧
B
i
(
x
→
i
)
=
0.Remark 14.
Note that if inequality constraint (24) is satisfied, then Lie-derivative of B
i
(
x
→
i
) is negative definite under the constraint of u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c. 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 forH).
Let an interconnected hybrid I/O automatonH be given. For each interconnected individual hybrid system H
i, suppose that both B
i
(
x
→
i
) satisfying constraints (17)–(20) in Lemma 11 and a vector Γ
=
diag
⁡
{
γ
1
,
…
,
γ
M
} satisfying (24) in Lemma 13 have been found, if there exists a diagonal matrix D
=
diag
⁡
{
d
1
,
…
,
d
M
}
>
0
M
×
M such that(26)
D
G
K
-
Γ
+
K
G
-
Γ
T
D
≤
0
,where d
1
,
…
,
d
M
∈
R
>
0; then H is safe.Proof.
SinceB
i
(
x
→
i
)s satisfying (17)–(20) and Γ
=
diag
⁡
{
γ
1
,
…
,
γ
M
} satisfying (24) exist, and there is a diagonal matrix D
=
diag
⁡
{
d
1
,
…
,
d
M
}
>
0
M
×
M satisfying (26), a compositional function B
(
x
→
) is built as(27)
B
x
→
=
∑
i
∈
I
γ
i
B
i
x
→
i
.
Since we haveB
i
(
x
→
i
0
)
<
0, for x
→
=
x
→
i
0
∈
X
0, it yields B
(
x
→
)
=
γ
1
B
1
(
x
→
1
0
)
+
⋯
+
γ
M
B
M
(
x
→
M
0
)
<
0. Similarly, ∀
x
→
=
x
→
i
u
∈
X
u
:
B
(
x
→
)
≥
0 is derived. Through introducing (24) and (26), for all x
→
∈
X
-
X
u, we derive(28)
∂
B
x
→
∂
x
→
f
→
t
,
x
→
t
,
u
→
c
=
∑
i
∈
I
∂
B
i
x
→
i
∂
x
→
i
f
i
t
i
,
x
→
i
t
i
,
u
→
i
c
≤
∑
i
∈
I
d
i
u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c
=
y
→
i
c
T
D
⊗
I
M
×
M
u
→
i
c
-
y
→
i
c
T
D
Γ
⊗
I
M
×
M
y
→
i
c
=
y
→
i
c
T
D
⊗
I
M
×
M
K
G
⊗
I
M
×
M
y
→
i
c
-
y
→
i
c
T
D
Γ
⊗
I
M
×
M
y
→
i
c
=
y
→
i
c
T
D
G
K
-
Γ
+
K
G
-
Γ
T
D
⊗
I
M
×
M
y
→
i
c
≤
0
.
Considering∀
i
∈
I
∀
x
→
l
∈
G
i
:
B
i
(
q
i
k
)
≤
B
i
(
q
i
j
), where q
i
k
≠
q
i
j, q
i
j
,
q
i
k
∈
Q
i, we derive ∑
l
∈
I
,
l
≠
i
γ
l
B
l
(
x
→
l
)
+
B
i
(
q
i
k
)
≤
∑
l
∈
I
,
l
≠
i
γ
l
B
l
(
x
→
l
)
+
B
i
(
q
i
j
); equivalently, B
(
x
→
) is nonincreasing at mode switchings. Therefore, B
(
x
→
) is the barrier certificate for H; furthermore, safety of H is guaranteed.Remark 16.
On the assumption of existences of barrier certificates for eachH
i and appropriate D
=
diag
⁡
{
d
1
,
…
,
d
M
}
>
0
M
×
M, Lie-derivatives of each B
i
(
x
→
i
) would be negative definite consistently. Then, B
(
x
→
) is negative definite along their trajectories of states under the restrictions of interconnections. Naturally, safety of H is guaranteed.


## 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 certificateB
:
X
→
→
R (X
→ 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 x
→
∈
X
→ satisfying B
(
x
→
)
=
0 form a barrier separating all unsafe states from possible system trajectories. B
(
x
→
) takes different values on different regions: for example, for each x
→
∈
X
u (X
u denotes unsafe states region), it satisfies B
x
→
>
0, while for each x
→
∈
X
s (X
s denotes reachable states region of trajectories) B
(
x
→
≤
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.Figure 1
Intuitive interpretation of barrier certificates.


## 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 forH
i).
Let an interconnected individual hybrid I/O automatonH
i
=
{
X
i
,
U
i
,
Y
i
,
S
i
,
Q
i
,
G
i
,
F
i
,
T
i
,
X
i
0
,
X
i
u
} be given. For each u
→
i
c
,
u
→
i
d
∈
U
i, suppose there exists a function B
i
(
x
→
i
) for all m
i modes of H
i. B
i
(
x
→
i
) is piecewise differentiable with respect to its state variable and satisfies(17)
B
i
x
→
i
>
0
,
∀
x
→
i
∈
X
i
u
,
(18)
B
i
x
→
i
≤
0
,
∀
x
→
i
∈
X
i
0
,
(19)
∂
B
i
x
→
i
∂
x
→
i
f
i
j
t
i
,
x
→
i
t
i
,
u
→
i
c
≤
0
,
∀
x
→
i
∈
X
i
∧
B
i
x
→
i
=
0
,
(20)
B
i
q
i
k
≤
B
i
q
i
j
,
∀
x
→
i
∈
G
i
,
q
i
k
≠
q
i
j
,
q
i
j
,
q
i
k
∈
Q
i
,where, for the case in (20), H
i undergoes a switching from mode q
i
j to mode q
i
k. If such B
i
(
x
→
i
) exists, then the safety of H
i is guaranteed.Proof (by contradiction).
For eachu
→
i
c, assume that barrier certificates B
i
j
(
x
→
i
) satisfying (17)–(20) can be found and suppose there exists an instant t
i
⋆
∈
[
0
,
T
] when x
→
i
(
t
i
⋆
)
∈
X
i
u. Suppose there exist two sequences of instants 0
=
t
i
0
<
t
i
1
<
⋯
<
t
i
p
i
=
t
i
⋆ and 0
=
t
0
<
t
1
<
⋯
<
t
p
=
t
i
⋆. p
i
,
p
∈
N
>
0 are either finite or infinite. At each t
i
p
i, mode q
i
p
i
∈
Q
i is activated, while, at each t
p, an impulsive interconnection rather than the continuous-time interconnection is activated. From (17), we derive B
i
q
i
p
i
(
x
→
i
(
t
⋆
)
)
>
0. The impulsive interconnection u
→
i
d could be omitted considering(21)
∑
l
=
1
p
∫
t
l
t
l
∂
B
i
x
→
i
∂
x
→
i
f
i
j
t
i
,
x
→
i
t
i
,
u
→
i
d
=
0for any finite p. And from (20), it concludes that B
i
(
x
→
i
) decreases at each switching. Over the continuous-time interval [
0
,
t
i
⋆
], we have(22)
B
i
x
→
i
t
i
⋆
=
B
i
x
→
i
t
i
0
+
∑
l
=
1
p
i
∫
t
i
l
t
i
l
+
1
∂
B
i
j
x
→
i
∂
x
→
i
f
i
j
t
i
,
x
→
i
t
i
,
u
→
i
c
+
∑
l
=
1
p
u
→
i
d
T
f
i
j
t
i
,
x
→
i
t
i
+
∑
l
=
1
p
B
i
x
→
i
-
B
i
l
x
→
i
≤
B
i
x
→
i
t
i
0
+
∑
l
=
1
p
i
∫
t
i
l
t
i
l
+
1
∂
B
i
x
→
i
∂
x
→
i
f
i
j
t
i
,
x
→
i
t
i
,
u
→
i
c
≤
B
i
x
→
i
t
i
0
+
∑
l
=
1
p
i
ln
⁡
B
i
x
→
i
t
i
l
+
1
-
ln
⁡
B
i
x
→
i
t
i
l
≤
B
i
x
→
i
t
i
0
≤
0
.Therefore, the derived B
i
(
x
→
i
(
t
i
⋆
)
)
≤
0 contradicts the assumption B
i
(
x
→
i
(
t
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
i
(
x
→
i
) is sufficient for safety of H
i.Remark 12.
Intuitively, the value ofB
i
(
x
→
i
) decreases along both continuous flows as well as switchings, since B
i
(
x
→
i
0
)
<
0, all states of trajectories of H
i are negative, and reachable states would not intersect with the unsafe states region. It should be admitted that B
i
(
x
→
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 feedbackh
i
c
(
x
→
i
), g
i
c
(
y
→
1
c
,
…
,
y
→
M
c
) is rewritten as(23)
h
i
c
x
→
i
g
i
c
y
→
1
c
,
…
,
y
→
M
c
H
i
=
h
1,1
⋯
h
1
,
M
i
⋮
⋱
⋮
h
M
i
,
1
⋯
h
M
i
,
M
x
1,1
i
⋮
x
M
i
,
1
i
G
i
=
g
1,1
⋯
g
1
,
M
⋮
⋱
⋮
g
M
,
1
⋯
g
M
,
M
y
→
1
c
⋮
y
→
M
c
,where x
→
i
=
[
x
1,1
i
,
…
,
x
M
i
,
1
i
]
T (x
1,1
i denotes the 1st-row, 1st-column element of vector x
→
i) and [
y
→
1
c
,
…
,
y
→
M
c
]
T is a concatenation of vectors y
→
1
c
,
…
,
y
→
M
c. Additionally, H
i
,
G
i are polynomial matrices; please distinguish them from the symbols H
i
,
G
i.Lemma 13 (coupling constraints on interconnections).
Let an interconnected I/O automatonH be given. For each interconnected individual hybrid system H
i, define H
=
[
H
1
T
,
…
,
H
M
T
] and G
=
[
G
1
T
,
…
,
G
M
T
], if there exists Γ
=
diag
⁡
{
γ
1
,
…
,
γ
M
}
>
0
M
×
M such that(24)
G
⊗
I
r
×
r
≤
Γ
H
T
K
T
K
H
⊗
I
r
×
rholds, where γ
1
,
…
,
γ
M
∈
R
>
0. Then there exits u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c
≤
0, ∀
i
=
1,2
,
…
,
M, satisfying(25)
∂
B
i
x
→
i
∂
x
→
i
f
i
j
t
i
,
x
→
i
t
i
,
u
→
i
c
≤
u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c
,
∀
x
→
i
∈
X
i
∧
B
i
x
→
i
=
0for all i
∈
I.Proof.
Since there existsΓ
=
diag
⁡
{
γ
1
,
…
,
γ
M
}
>
0
M
×
M with γ
1
,
…
,
γ
M
∈
R
>
0 such that G
⊗
I
r
×
r
≤
Γ
H
T
K
T
K
H
⊗
I
r
×
r, it could be verified that each column of G
⊗
I
r
×
r
≤
Γ
H
T
K
T
K
H
⊗
I
r
×
r
=
u
→
c
T
y
→
c
-
Γ
y
→
c
T
y
→
c
≤
0 through matrix computation; therefore, ∀
i
∈
I
:
u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c stands. Under constraint (19), the rest is proved by contradiction. Assume that, ∀
γ
i
∈
R
>
0 satisfying (24), (
∂
B
i
x
→
i
/
∂
x
→
i
)
f
i
j
(
t
i
,
x
→
i
(
t
i
)
,
u
→
i
c
)
≥
u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c holds; then take Γ
=
(
y
→
c
)
-
1
u
→
c
T, and derive (
∂
B
i
x
→
i
/
∂
x
→
i
)
f
i
j
(
t
i
,
x
→
i
(
t
i
)
,
u
→
i
c
)
≥
0, which is contradiction to constraint (19). Therefore, Γ satisfying (24) is sufficient for (
∂
B
i
x
→
i
/
∂
x
→
i
)
f
i
j
(
t
i
,
x
→
i
(
t
i
)
,
u
→
i
c
)
≤
u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c
,
∀
x
→
i
∈
X
i
∧
B
i
(
x
→
i
)
=
0.Remark 14.
Note that if inequality constraint (24) is satisfied, then Lie-derivative of B
i
(
x
→
i
) is negative definite under the constraint of u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c. 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 forH).
Let an interconnected hybrid I/O automatonH be given. For each interconnected individual hybrid system H
i, suppose that both B
i
(
x
→
i
) satisfying constraints (17)–(20) in Lemma 11 and a vector Γ
=
diag
⁡
{
γ
1
,
…
,
γ
M
} satisfying (24) in Lemma 13 have been found, if there exists a diagonal matrix D
=
diag
⁡
{
d
1
,
…
,
d
M
}
>
0
M
×
M such that(26)
D
G
K
-
Γ
+
K
G
-
Γ
T
D
≤
0
,where d
1
,
…
,
d
M
∈
R
>
0; then H is safe.Proof.
SinceB
i
(
x
→
i
)s satisfying (17)–(20) and Γ
=
diag
⁡
{
γ
1
,
…
,
γ
M
} satisfying (24) exist, and there is a diagonal matrix D
=
diag
⁡
{
d
1
,
…
,
d
M
}
>
0
M
×
M satisfying (26), a compositional function B
(
x
→
) is built as(27)
B
x
→
=
∑
i
∈
I
γ
i
B
i
x
→
i
.
Since we haveB
i
(
x
→
i
0
)
<
0, for x
→
=
x
→
i
0
∈
X
0, it yields B
(
x
→
)
=
γ
1
B
1
(
x
→
1
0
)
+
⋯
+
γ
M
B
M
(
x
→
M
0
)
<
0. Similarly, ∀
x
→
=
x
→
i
u
∈
X
u
:
B
(
x
→
)
≥
0 is derived. Through introducing (24) and (26), for all x
→
∈
X
-
X
u, we derive(28)
∂
B
x
→
∂
x
→
f
→
t
,
x
→
t
,
u
→
c
=
∑
i
∈
I
∂
B
i
x
→
i
∂
x
→
i
f
i
t
i
,
x
→
i
t
i
,
u
→
i
c
≤
∑
i
∈
I
d
i
u
→
i
c
T
y
→
i
c
-
γ
i
y
→
i
c
T
y
→
i
c
=
y
→
i
c
T
D
⊗
I
M
×
M
u
→
i
c
-
y
→
i
c
T
D
Γ
⊗
I
M
×
M
y
→
i
c
=
y
→
i
c
T
D
⊗
I
M
×
M
K
G
⊗
I
M
×
M
y
→
i
c
-
y
→
i
c
T
D
Γ
⊗
I
M
×
M
y
→
i
c
=
y
→
i
c
T
D
G
K
-
Γ
+
K
G
-
Γ
T
D
⊗
I
M
×
M
y
→
i
c
≤
0
.
Considering∀
i
∈
I
∀
x
→
l
∈
G
i
:
B
i
(
q
i
k
)
≤
B
i
(
q
i
j
), where q
i
k
≠
q
i
j, q
i
j
,
q
i
k
∈
Q
i, we derive ∑
l
∈
I
,
l
≠
i
γ
l
B
l
(
x
→
l
)
+
B
i
(
q
i
k
)
≤
∑
l
∈
I
,
l
≠
i
γ
l
B
l
(
x
→
l
)
+
B
i
(
q
i
j
); equivalently, B
(
x
→
) is nonincreasing at mode switchings. Therefore, B
(
x
→
) is the barrier certificate for H; furthermore, safety of H is guaranteed.Remark 16.
On the assumption of existences of barrier certificates for eachH
i and appropriate D
=
diag
⁡
{
d
1
,
…
,
d
M
}
>
0
M
×
M, Lie-derivatives of each B
i
(
x
→
i
) would be negative definite consistently. Then, B
(
x
→
) 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 Section4. 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
i
(
x
→
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 forH
is

To compute individual barrier certificates, all the sets of states in (17)–(20) should be transformed into semialgebraic sets. Let X
i
=
{
x
→
i
:
p
X
i
(
x
→
i
)
≥
0
}, X
i
0
=
{
x
→
i
:
p
X
i
0
(
x
→
i
)
≥
0
}, X
i
u
=
{
x
→
i
:
p
X
i
u
(
x
→
i
)
≥
0
}, and G
i
=
{
x
→
i
:
p
G
i
(
x
→
i
)
≥
0
} be given as vectors of polynomials p
X
i
(
x
→
i
)
,
p
X
i
0
(
x
→
i
)
,
p
X
i
u
(
x
→
i
)
,
p
G
i
(
x
→
i
)
∈
P
n
i in x
→
i, where those inequalities are satisfied entry-wise. For example, when X is defined as {
x
→
i
:
x
→
m
i
n
≤
x
→
i
≤
x
→
m
a
x
}, it is equivalent to the semialgebraic set X
=
{
x
→
i
:
p
X
i
(
x
→
i
)
=
(
x
→
m
a
x
-
x
→
i
)
(
x
→
i
-
x
→
m
i
n
)
≥
0
}.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 functionsp
0
x
→
,
p
1
x
→
,
…
,
p
m
(
x
→
)
∈
P
n, if there exist s
1
(
x
→
)
,
s
2
(
x
→
)
,
…
,
s
m
(
x
→
)
∈
Σ
n such that p
0
(
x
→
)
-
∑
i
=
1
m
s
i
(
x
→
)
p
i
(
x
→
)
∈
Σ
n, then it holds that(29)
x
→
∈
R
n
:
p
1
x
→
,
…
,
p
m
x
→
≥
0
⊆
x
→
∈
R
n
:
p
0
x
→
≥
0
.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 automatonH
i
=
{
X
i
,
U
i
,
Y
i
,
S
i
,
Q
i
,
G
i
,
F
i
,
T
i
,
X
i
0
,
X
i
u
} be given, and X
i
,
X
i
0
,
X
i
u
,
G
i have been transformed into semialgebraic sets. The polynomial barrier certificate B
i
(
x
→
i
) could be computed through solving the following bilinear SOS program:(30)
B
i
x
→
i
-
ϵ
i
-
s
1
x
→
i
x
→
p
X
i
u
x
→
i
∈
Σ
n
,
(31)
-
B
i
x
→
i
-
s
2
x
→
i
x
→
i
p
X
i
0
x
→
i
∈
Σ
n
,
(32)
-
∂
B
i
x
→
i
∂
x
→
i
f
i
q
i
t
i
,
x
→
i
t
i
,
u
→
i
c
+
s
3
x
→
i
p
G
i
x
→
i
+
λ
i
x
→
i
B
i
x
→
i
∈
Σ
n
,
∀
q
i
∈
Q
i
,
(33)
-
ν
i
-
s
4
x
→
i
p
G
i
x
→
i
∈
Σ
n
,where λ
i
(
x
→
i
)
∈
P
n is a polynomial decision variable, ϵ
i
,
ν
i
∈
R
>
0 are scalar decision variables, and s
1
(
x
→
i
)
,
s
2
(
x
→
i
)
,
s
3
(
x
→
i
)
,
s
4
(
x
→
i
) are all SOS polynomial decision variables.Proof.
Notice that there exists a coupling between the polynomial decision variablesλ
i
(
x
→
i
) and B
i
(
x
→
i
), and this programming problem is bilinear. Here is the sketch of a proof. Since X
i
u
=
{
x
→
i
:
p
X
i
u
(
x
→
i
)
≥
0
}, and ∀
x
→
i
∈
X
i
u
:
B
i
(
x
→
i
)
≥
0, the positive definiteness could be guaranteed by B
i
(
x
→
i
)
-
ϵ
i
-
s
1
(
x
→
i
)
(
x
→
)
p
X
i
u
(
x
→
i
)
∈
Σ
n by applying generalized S-procedure. Similarly, (31)–(33) could be derived. Scalar ν
i decision variable introduced in (33) is for the switching. Therefore, B
i
(
x
→
i
) derived by solving the bilinear SOS program satisfying (30)–(33) is a barrier certificate for H
i.Remark 19.
Loosely speaking, generalized S-procedure is for determining satisfaction of an inequality constraintp
0
(
x
→
)
≥
0 when other inequality constraints p
1
x
→
≥
0
,
…
,
p
m
(
x
→
)
≥
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 forH

In order to derive the compositional barrier certificate forH, Γ should be estimated first by solving the following optimization problem:(34)
M
i
n
Γ
=
diag
⁡
γ
1
,
…
,
γ
M
s.t.
G
⊗
I
r
×
r
≤
Γ
H
T
K
T
K
H
⊗
I
r
×
r
Γ
>
0
M
×
M
.The above optimization is a linear program problem which could be solved with the help of linear programming solvers. With derivedΓ, compositional barrier certificates for H could be computed directly by solving a bilinear SOS program.Theorem 20 (compositional barrier certificate forH as bilinear SOS program).
Let an interconnected hybrid I/O automatonH be given. For each interconnected H
i, there exists an individual barrier certificate B
i
(
x
→
i
); then, the compositional barrier certificate B
(
x
→
) could be computed through solving the following bilinear SOS program:(35)
M
i
n
D
=
diag
⁡
d
1
,
…
,
d
m
(36)
s
.
t
.
-
D
B
x
→
-
s
1
x
→
p
X
s
x
→
∈
Σ
n
×
m
i
(37)
D
-
ϵ
-
s
2
x
→
p
X
u
x
→
∈
Σ
n
×
m
i
(38)
-
H
T
D
⊗
I
r
×
r
K
G
⊗
I
r
×
r
+
K
G
⊗
I
r
×
r
T
D
⊗
I
r
×
r
H
-
1
m
T
D
-
Γ
H
2
+
p
x
→
D
B
x
→
∈
Σ
n
×
m
i
(39)
D
>
0
m
×
m
,where B
(
x
→
)
=
[
B
1
(
x
→
1
)
,
…
,
B
m
(
x
→
m
)
]
T, p
X
s
(
x
→
)
=
[
p
X
1
s
(
x
→
1
)
,
…
,
p
X
m
s
(
x
→
m
)
]
T, p
X
u
(
x
→
)
=
[
p
X
1
u
(
x
→
1
)
,
…
,
p
X
m
u
(
x
→
m
)
]
T (∀
i
∈
I
:
p
X
i
s
(
x
→
i
)
=
p
X
i
(
x
→
i
)
-
p
X
i
u
(
x
→
i
)). D is a scalar matrix decision variable, ϵ
=
[
ϵ
1
,
…
,
ϵ
m
] is a scalar vectorial decision variable, s
1
(
x
→
)
,
s
2
(
x
→
) are SOS polynomials decision variables, and p
(
x
→
) is a polynomial decision variable.Proof.
Here is the sketch of a proof. As indicated in the above theorem,B
1
(
x
→
1
)
,
…
,
B
m
(
x
→
m
) are barrier certificates for H
is. Constraints (36) and (37) imply that B
(
x
→
) is nonpositive on X
u and positive on X
s
=
X
-
X
u. Constraints (38) and (39) imply that(40)
-
H
T
D
⊗
I
r
×
r
K
G
⊗
I
r
×
r
+
K
G
⊗
I
r
×
r
T
D
⊗
I
r
×
r
H
+
1
m
T
D
H
T
Γ
H
≥
0
⟹
H
T
G
K
D
+
D
K
G
T
H
-
1
m
T
D
H
T
Γ
H
≤
0
⟹
H
T
G
K
D
+
D
K
G
T
H
-
H
T
D
T
Γ
D
H
≤
0
⟹
D
G
K
-
Γ
+
K
G
-
Γ
T
D
≤
0
.
In conclusion, the derivedB
(
x
→
) satisfies Theorem 15, and B
(
x
→
) is the compositional barrier certificate for H; thus, H is safe.Remark 21.
Sincep
(
x
→
) 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].


## 5.1. Computation of Individual Barrier Certificates forH
is

To compute individual barrier certificates, all the sets of states in (17)–(20) should be transformed into semialgebraic sets. Let X
i
=
{
x
→
i
:
p
X
i
(
x
→
i
)
≥
0
}, X
i
0
=
{
x
→
i
:
p
X
i
0
(
x
→
i
)
≥
0
}, X
i
u
=
{
x
→
i
:
p
X
i
u
(
x
→
i
)
≥
0
}, and G
i
=
{
x
→
i
:
p
G
i
(
x
→
i
)
≥
0
} be given as vectors of polynomials p
X
i
(
x
→
i
)
,
p
X
i
0
(
x
→
i
)
,
p
X
i
u
(
x
→
i
)
,
p
G
i
(
x
→
i
)
∈
P
n
i in x
→
i, where those inequalities are satisfied entry-wise. For example, when X is defined as {
x
→
i
:
x
→
m
i
n
≤
x
→
i
≤
x
→
m
a
x
}, it is equivalent to the semialgebraic set X
=
{
x
→
i
:
p
X
i
(
x
→
i
)
=
(
x
→
m
a
x
-
x
→
i
)
(
x
→
i
-
x
→
m
i
n
)
≥
0
}.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 functionsp
0
x
→
,
p
1
x
→
,
…
,
p
m
(
x
→
)
∈
P
n, if there exist s
1
(
x
→
)
,
s
2
(
x
→
)
,
…
,
s
m
(
x
→
)
∈
Σ
n such that p
0
(
x
→
)
-
∑
i
=
1
m
s
i
(
x
→
)
p
i
(
x
→
)
∈
Σ
n, then it holds that(29)
x
→
∈
R
n
:
p
1
x
→
,
…
,
p
m
x
→
≥
0
⊆
x
→
∈
R
n
:
p
0
x
→
≥
0
.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 automatonH
i
=
{
X
i
,
U
i
,
Y
i
,
S
i
,
Q
i
,
G
i
,
F
i
,
T
i
,
X
i
0
,
X
i
u
} be given, and X
i
,
X
i
0
,
X
i
u
,
G
i have been transformed into semialgebraic sets. The polynomial barrier certificate B
i
(
x
→
i
) could be computed through solving the following bilinear SOS program:(30)
B
i
x
→
i
-
ϵ
i
-
s
1
x
→
i
x
→
p
X
i
u
x
→
i
∈
Σ
n
,
(31)
-
B
i
x
→
i
-
s
2
x
→
i
x
→
i
p
X
i
0
x
→
i
∈
Σ
n
,
(32)
-
∂
B
i
x
→
i
∂
x
→
i
f
i
q
i
t
i
,
x
→
i
t
i
,
u
→
i
c
+
s
3
x
→
i
p
G
i
x
→
i
+
λ
i
x
→
i
B
i
x
→
i
∈
Σ
n
,
∀
q
i
∈
Q
i
,
(33)
-
ν
i
-
s
4
x
→
i
p
G
i
x
→
i
∈
Σ
n
,where λ
i
(
x
→
i
)
∈
P
n is a polynomial decision variable, ϵ
i
,
ν
i
∈
R
>
0 are scalar decision variables, and s
1
(
x
→
i
)
,
s
2
(
x
→
i
)
,
s
3
(
x
→
i
)
,
s
4
(
x
→
i
) are all SOS polynomial decision variables.Proof.
Notice that there exists a coupling between the polynomial decision variablesλ
i
(
x
→
i
) and B
i
(
x
→
i
), and this programming problem is bilinear. Here is the sketch of a proof. Since X
i
u
=
{
x
→
i
:
p
X
i
u
(
x
→
i
)
≥
0
}, and ∀
x
→
i
∈
X
i
u
:
B
i
(
x
→
i
)
≥
0, the positive definiteness could be guaranteed by B
i
(
x
→
i
)
-
ϵ
i
-
s
1
(
x
→
i
)
(
x
→
)
p
X
i
u
(
x
→
i
)
∈
Σ
n by applying generalized S-procedure. Similarly, (31)–(33) could be derived. Scalar ν
i decision variable introduced in (33) is for the switching. Therefore, B
i
(
x
→
i
) derived by solving the bilinear SOS program satisfying (30)–(33) is a barrier certificate for H
i.Remark 19.
Loosely speaking, generalized S-procedure is for determining satisfaction of an inequality constraintp
0
(
x
→
)
≥
0 when other inequality constraints p
1
x
→
≥
0
,
…
,
p
m
(
x
→
)
≥
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 forH

In order to derive the compositional barrier certificate forH, Γ should be estimated first by solving the following optimization problem:(34)
M
i
n
Γ
=
diag
⁡
γ
1
,
…
,
γ
M
s.t.
G
⊗
I
r
×
r
≤
Γ
H
T
K
T
K
H
⊗
I
r
×
r
Γ
>
0
M
×
M
.The above optimization is a linear program problem which could be solved with the help of linear programming solvers. With derivedΓ, compositional barrier certificates for H could be computed directly by solving a bilinear SOS program.Theorem 20 (compositional barrier certificate forH as bilinear SOS program).
Let an interconnected hybrid I/O automatonH be given. For each interconnected H
i, there exists an individual barrier certificate B
i
(
x
→
i
); then, the compositional barrier certificate B
(
x
→
) could be computed through solving the following bilinear SOS program:(35)
M
i
n
D
=
diag
⁡
d
1
,
…
,
d
m
(36)
s
.
t
.
-
D
B
x
→
-
s
1
x
→
p
X
s
x
→
∈
Σ
n
×
m
i
(37)
D
-
ϵ
-
s
2
x
→
p
X
u
x
→
∈
Σ
n
×
m
i
(38)
-
H
T
D
⊗
I
r
×
r
K
G
⊗
I
r
×
r
+
K
G
⊗
I
r
×
r
T
D
⊗
I
r
×
r
H
-
1
m
T
D
-
Γ
H
2
+
p
x
→
D
B
x
→
∈
Σ
n
×
m
i
(39)
D
>
0
m
×
m
,where B
(
x
→
)
=
[
B
1
(
x
→
1
)
,
…
,
B
m
(
x
→
m
)
]
T, p
X
s
(
x
→
)
=
[
p
X
1
s
(
x
→
1
)
,
…
,
p
X
m
s
(
x
→
m
)
]
T, p
X
u
(
x
→
)
=
[
p
X
1
u
(
x
→
1
)
,
…
,
p
X
m
u
(
x
→
m
)
]
T (∀
i
∈
I
:
p
X
i
s
(
x
→
i
)
=
p
X
i
(
x
→
i
)
-
p
X
i
u
(
x
→
i
)). D is a scalar matrix decision variable, ϵ
=
[
ϵ
1
,
…
,
ϵ
m
] is a scalar vectorial decision variable, s
1
(
x
→
)
,
s
2
(
x
→
) are SOS polynomials decision variables, and p
(
x
→
) is a polynomial decision variable.Proof.
Here is the sketch of a proof. As indicated in the above theorem,B
1
(
x
→
1
)
,
…
,
B
m
(
x
→
m
) are barrier certificates for H
is. Constraints (36) and (37) imply that B
(
x
→
) is nonpositive on X
u and positive on X
s
=
X
-
X
u. Constraints (38) and (39) imply that(40)
-
H
T
D
⊗
I
r
×
r
K
G
⊗
I
r
×
r
+
K
G
⊗
I
r
×
r
T
D
⊗
I
r
×
r
H
+
1
m
T
D
H
T
Γ
H
≥
0
⟹
H
T
G
K
D
+
D
K
G
T
H
-
1
m
T
D
H
T
Γ
H
≤
0
⟹
H
T
G
K
D
+
D
K
G
T
H
-
H
T
D
T
Γ
D
H
≤
0
⟹
D
G
K
-
Γ
+
K
G
-
Γ
T
D
≤
0
.
In conclusion, the derivedB
(
x
→
) satisfies Theorem 15, and B
(
x
→
) is the compositional barrier certificate for H; thus, H is safe.Remark 21.
Sincep
(
x
→
) 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 systemsH consisting of two coupled hybrid systems H
1
,
H
2:(41)
H
1
:
x
→
˙
1
=
A
x
→
1
+
k
→
1
x
→
2
,
x
→
1
=
x
11
,
x
12
T
x
→
1
0
=
x
→
1
:
4
-
x
11
x
11
+
4
≥
0
,
4
-
x
12
x
12
+
4
≥
0
,
x
→
1
u
=
x
→
1
:
10
-
x
11
x
11
+
10
≥
0
,
10
-
x
12
x
12
+
10
≥
0
,
x
11
x
12
<
0
:
A
1
=
0.1
-
1
2
0.1
,
x
11
x
12
≥
0
:
A
2
=
0.1
-
2
1
0.1
k
→
1
=
-
2
0
-
3
-
4
H
2
:
x
→
˙
2
=
B
x
→
2
+
k
→
2
x
→
1
,
x
→
2
=
x
21
,
x
22
T
x
→
2
0
=
x
→
2
:
4
-
x
21
x
21
+
4
≥
0
,
4
-
x
22
x
22
+
4
≥
0
,
x
→
2
u
=
x
→
2
:
10
-
x
21
x
21
+
10
≥
0
,
10
-
x
22
x
22
+
10
≥
0
,
x
21
x
22
<
0
:
B
1
=
-
5
-
4
-
1
-
2
,
x
21
x
22
≥
0
:
B
2
=
-
2
-
4
20
-
2
k
→
2
=
-
1
0
0
1
, where x
→
1
0
,
x
→
2
0 are admissible initial states, x
→
1
u
,
x
→
2
u are unsafe states, and inequalities x
11
x
12
<
0, x
11
x
12
≥
0, x
21
x
22
<
0, and x
21
x
22
≥
0 are switching conditions. A
1
,
A
2 and B
1
,
B
2 are modes of H
1 and H
2, respectively. k
→
1
,
k
→
2 are interconnection matrices. The derived barrier certificate is -
0.01
x
11
3
-
1.88
x
11
2
x
12
-
0.3
x
11
2
x
21
-
476.42
x
11
2
+
5.77
x
11
x
12
2 − 0.03
x
11
x
12
x
21
-
0.03
x
11
x
12
x
22
+
77.25
x
11
x
12
-
16.43
x
11
x
21
2
+
0.03
x
11
x
21
x
22 + 475.47
x
11
x
21
-
0.03
x
11
x
22
2
+
0.5
x
11
x
22
-
0.51
x
11
-
0.01
x
12
3
+
0.02
x
12
2
x
21
-
0.42
x
12
2
x
22 − 154.77
x
12
2
+
11.13
x
12
x
21
2
+
0.01
x
12
x
21
x
22
+
254.32
x
12
x
21
-
2.1
x
12
x
22
2
+
102
x
12
x
22 + 1.12
x
12
+
1.85
x
21
2
x
22
+
191.09
x
21
2
+
1.95
x
21
x
22
2
-
27.16
x
21
x
22
+
1.21
x
21 − 0.01
x
22
3
-
65.95
x
22
2
+
1.48
x
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.



---

*Source: 4149059-2016-03-23.xml*