Prajna, Stephen (2005) Optimization-based methods for nonlinear and hybrid systems verification. Dissertation (Ph.D.), California Institute of Technology. http://resolver.caltech.edu/CaltechETD:etd-05272005-144358
Complex behaviors that can be exhibited by hybrid systems make the verification of such systems 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 in safety critical applications makes it evident that verification is an issue that has to be addressed.
In this thesis, 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, eventuality, and their combinations. 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 computing an upper-bound on 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 theorem in safety verification using barrier certificates.
|Item Type:||Thesis (Dissertation (Ph.D.))|
|Subject Keywords:||barrier certificates; hybrid systems; nonlinear systems; optimization; sum of squares programming; verification|
|Degree Grantor:||California Institute of Technology|
|Division:||Engineering and Applied Science|
|Major Option:||Control and Dynamical Systems|
|Thesis Availability:||Public (worldwide access)|
|Defense Date:||14 January 2005|
|Default Usage Policy:||No commercial reproduction, distribution, display or performance rights in this work are provided.|
|Deposited By:||Imported from ETD-db|
|Deposited On:||31 May 2005|
|Last Modified:||26 Dec 2012 02:47|
- Final Version
See Usage Policy.
Repository Staff Only: item control page