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.
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 denote the field of real numbers, and stand for the -dimensional real vector space. refer to the sets of positive real numbers and positive natural numbers, respectively. Lower case alphabets such as represent variables, while symbols such as are vectorial variables. refers to the Euclidean vector norm. For matrices or vectors, the superscript “” denotes matrix transposition. is the identity matrix, denotes zero vector, is scalar, and is an zero matrix. The notation indicates a square diagonal matrix with the arguments along the diagonal. is the inverse of matrix .
Definition 1 (positive-definite polynomial and its Lie-derivative). Let denote the -tuple , will be taken as the polynomial field over variables in with the highest degree of , and a polynomial function is said to be positive definite ifffor all with . The first-order Lie-derivative of along a continuous flow is as follows:
Definition 2 (SOS polynomial). A multivariate polynomial is an SOS polynomial if there exist finite polynomials such thatLet ( for short) denote the set of all SOS polynomials in under the degree of .
Definition 3 (semialgebraic set). A set is called a semialgebraic set iff and is finite.
Definition 4 ( polynomial function). A polynomial function is of class ; equivalently , if it is strictly increasing and .
Definition 5 (Kronecker product). Let , denote two matrices, and then the Kronecker product of and is defined as the matrix:
Definition 6 ( for matrices). For two matrices , , if and only if
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 iswhere , , and are decision variables. , , 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 which is a composition of finite hybrid I/O automaton 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 of is a tuple with the following components: (i) is a set of real-valued system internal variables . The number is called the dimension of .(ii) is a set of real-valued system external inputs , where denotes the continuous input while denotes the discrete input. is disjoint from .(iii) is a set of real-valued system external outputs , where denotes the continuous output while denotes the discrete output. is disjoint from .(iv) is a finite set of indexes of switching signals. The index function denotes the sequence of activated switching signals over the continuous-time interval .(v) is a finite set of modes. The overall state space of individual hybrid systems is , and a state is denoted by . denote different modes of when .(vi) is the set of guard conditions for . A switching is enabled at once holds, namely, a state-dependent switching. Throughout this paper, all switchings of are assumed to be state-dependent. Furthermore, is taken as the complement of ().(vii) is a set of continuous vector fields. For each state , incorporates a differential constraint on the continuous evolution according to the differential equation:where , , , and .(viii) is a relation capturing discrete switchings between two modes. Here a switching indicates that from mode , can undergo a switching to the mode at the instant . Only finite switchings are allowed over finite-time intervals.(ix) is the set of admissible initial states of .(x) is the set of unsafe states of .
Trajectories of start from the admissible initial states and are concatenations of a sequence of continuous evolutions in and discrete switchings among different modes satisfying the following.
Initiation. is an admissible initial state of .
Discrete Consecution. At the instant , the switching signal activates and produces a discrete output according tosimultaneously.
Continuous Consecution. For an activating mode over the holds and produces continuous outputs according toover the continuous interval.
Here, denotes the left limit of and denotes its right limit. Additionally, s, s, and s are all restricted to polynomials throughout this paper.
Compositional hybrid I/O automaton is given as an interconnection of finite individual hybrid I/O automaton consisting of assignments relating the inputs and outputs of interconnected .
Definition 9 (compositional hybrid I/O automaton). A compositional hybrid I/O automaton is a finite set of interconnected hybrid I/O automata indexed by . Formally, is a tuple with the following components: (i) is a finite set of indexes of interconnected hybrid automaton . Without loss of generality, we assume has elements.(ii) is a finite set of interconnected hybrid I/O automata. of are the Cartesian products of each corresponding item of all individual s, respectively. Particularly, , which means if there exists an of which intersects corresponding guard . Dually, is defined as . Besides, only finite switchings are allowed over any finite-time intervals.(iii) represents the static topology of the interconnection, which is in the form of an matrix , , , .(iv) is a finite set of interconnections following continuous assignmentsover continuous-time intervals, where is the interconnection over a continuous-time interval. is the th row of . s are assumed to be polynomial functions.(v) is a finite set of interconnections following discrete assignmentsat discrete instants, where is the interconnection at switching instant, and is the th row of . s are assumed to be polynomial functions.
Intuitively, trajectory of is the composition of trajectories of s under restrictions of the interconnections. We take to represent the trajectory of ; thus, the trajectory of is a Cartesian product satisfying the following.
Initiation. for all .
Discrete Consecution. For , at least one 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:
Continuous Consecution. For , states of all trajectories of evolve continuously under the continuous interconnections according to the following differential equations:
For compositional hybrid I/O automata , evolves continuously when all trajectories of s evolve continuously, while switchings occur once there exists a discrete consecution among s.
Based on the concept of trajectories of , safety of could be formalized as follows.
Definition 10 (safety of ). Let an interconnected hybrid I/O automaton be given. Take as the trajectory of ; then is unsafe if there exists an instant such that holds. Furthermore, is safe when none of the trajectories of starting from admissible initial states would intersect unsafe states of .
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 ( 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 satisfying form a barrier separating all unsafe states from possible system trajectories. takes different values on different regions: for example, for each ( denotes unsafe states region), it satisfies , while for each ( denotes reachable states region of trajectories) 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 ). Let an interconnected individual hybrid I/O automaton be given. For each , suppose there exists a function for all modes of . is piecewise differentiable with respect to its state variable and satisfieswhere, for the case in (20), undergoes a switching from mode to mode . If such exists, then the safety of is guaranteed.
Proof (by contradiction). For each , assume that barrier certificates satisfying (17)–(20) can be found and suppose there exists an instant when . Suppose there exist two sequences of instants and . are either finite or infinite. At each , mode is activated, while, at each , an impulsive interconnection rather than the continuous-time interconnection is activated. From (17), we derive . The impulsive interconnection could be omitted consideringfor any finite . And from (20), it concludes that decreases at each switching. Over the continuous-time interval , we haveTherefore, the derived contradicts the assumption . Thus, we conclude that any trajectory starting from admissible initial states would not intersect unsafe states. In conclusion, the existence of barrier certificates is sufficient for safety of .
Remark 12. Intuitively, the value of decreases along both continuous flows as well as switchings, since , all states of trajectories of are negative, and reachable states would not intersect with the unsafe states region. It should be admitted that derived in Lemma 11 is conservative; however, for the safety of interconnected hybrid systems , this conservatism is justified.
For the convenience of expression, output as well as feedback , is rewritten aswhere ( denotes the 1st-row, 1st-column element of vector ) and is a concatenation of vectors . Additionally, are polynomial matrices; please distinguish them from the symbols .
Lemma 13 (coupling constraints on interconnections). Let an interconnected I/O automaton be given. For each interconnected individual hybrid system , define and , if there exists such thatholds, where . Then there exits , , satisfyingfor all .
Proof. Since there exists with such that , it could be verified that each column of through matrix computation; therefore, stands. Under constraint (19), the rest is proved by contradiction. Assume that, satisfying (24), holds; then take , and derive , which is contradiction to constraint (19). Therefore, satisfying (24) is sufficient for .
Remark 14. Note that if inequality constraint (24) is satisfied, then Lie-derivative of is negative definite under the constraint of . 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 ). Let an interconnected hybrid I/O automaton be given. For each interconnected individual hybrid system , suppose that both satisfying constraints (17)–(20) in Lemma 11 and a vector satisfying (24) in Lemma 13 have been found, if there exists a diagonal matrix such thatwhere ; then is safe.
Proof. Since s satisfying (17)–(20) and satisfying (24) exist, and there is a diagonal matrix satisfying (26), a compositional function is built asSince we have , for , it yields . Similarly, is derived. Through introducing (24) and (26), for all , we deriveConsidering , where , , we derive ; equivalently, is nonincreasing at mode switchings. Therefore, is the barrier certificate for ; furthermore, safety of is guaranteed.
Remark 16. On the assumption of existences of barrier certificates for each and appropriate , Lie-derivatives of each would be negative definite consistently. Then, is negative definite along their trajectories of states under the restrictions of interconnections. Naturally, safety of 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 . 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 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 s
To compute individual barrier certificates, all the sets of states in (17)–(20) should be transformed into semialgebraic sets. Let , , , and be given as vectors of polynomials in , where those inequalities are satisfied entry-wise. For example, when is defined as , it is equivalent to the semialgebraic set .
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 , if there exist such that , then it holds that
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 be given, and have been transformed into semialgebraic sets. The polynomial barrier certificate could be computed through solving the following bilinear SOS program:where is a polynomial decision variable, are scalar decision variables, and are all SOS polynomial decision variables.
Proof. Notice that there exists a coupling between the polynomial decision variables and , and this programming problem is bilinear. Here is the sketch of a proof. Since , and , the positive definiteness could be guaranteed by by applying generalized S-procedure. Similarly, (31)–(33) could be derived. Scalar decision variable introduced in (33) is for the switching. Therefore, derived by solving the bilinear SOS program satisfying (30)–(33) is a barrier certificate for .
Remark 19. Loosely speaking, generalized S-procedure is for determining satisfaction of an inequality constraint when other inequality constraints 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
In order to derive the compositional barrier certificate for , should be estimated first by solving the following optimization problem:
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 could be computed directly by solving a bilinear SOS program.
Theorem 20 (compositional barrier certificate for as bilinear SOS program). Let an interconnected hybrid I/O automaton be given. For each interconnected , there exists an individual barrier certificate ; then, the compositional barrier certificate could be computed through solving the following bilinear SOS program:where , , (). is a scalar matrix decision variable, is a scalar vectorial decision variable, are SOS polynomials decision variables, and is a polynomial decision variable.
Proof. Here is the sketch of a proof. As indicated in the above theorem, are barrier certificates for s. Constraints (36) and (37) imply that is nonpositive on and positive on . Constraints (38) and (39) imply thatIn conclusion, the derived satisfies Theorem 15, and is the compositional barrier certificate for ; thus, is safe.
Remark 21. Since is coupled with , 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 consisting of two coupled hybrid systems : where are admissible initial states, are unsafe states, and inequalities , , , and are switching conditions. and are modes of and , respectively. are interconnection matrices. The derived barrier certificate is − + − + − . 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 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.
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 Liu would 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.