Thesis Seminar: Optimization-Based Methods for Nonlinear and Hybrid Systems Verification

Stephen Prajna, Caltech, Control and Dynamical Systems

Complex behaviors that can be exhibited by hybrid systems make the verification of correctness of such a system both important and challenging. Due to the infinite number of possibilities taken by the continuous state and the uncertainties in the system, exhaustive simulation is impossible, and also computing the set of reachable states is generally intractable. Nevertheless, the ever-increasing presence of hybrid systems -- including embedded and software-based systems -- in safety critical applications makes it evident that verification has to be done in one or another way.

In this work, we develop a unified methodology for verifying temporal properties of continuous and hybrid systems. Our framework does not require explicit computation of reachable states. Instead, functions of state termed barrier certificates and density functions are used in conjunction with deductive inference to prove properties such as safety, reachability, and eventuality, which form the basis for more general temporal logic formulas. As a consequence, the proposed methods are directly applicable to systems with nonlinearity, uncertainty, and constraints. Moreover, it is possible to treat safety verification of stochastic systems in a similar fashion, by upper-bounding the probability of reaching the unsafe states.

We formulate verification using barrier certificates and density functions as convex programming problems. For systems with polynomial descriptions, sum of squares optimization can be used to construct polynomial barrier certificates and density functions in a computationally scalable manner. Some examples are presented to illustrate the use of the methods. At the end, the convexity of the problem formulation is also exploited to prove a converse statement in safety verification using barrier certificates.