CaltechTHESIS
  A Caltech Library Service

Optimization-based methods for nonlinear and hybrid systems verification

Citation

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

Abstract

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)
Research Advisor(s):
  • Doyle, John Comstock
Thesis Committee:
  • Doyle, John Comstock (chair)
  • Rantzer, Anders
  • Marsden, Jerrold E.
  • Chandy, K. Mani
  • Murray, Richard M.
Defense Date:14 January 2005
Record Number:CaltechETD:etd-05272005-144358
Persistent URL:http://resolver.caltech.edu/CaltechETD:etd-05272005-144358
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:2155
Collection:CaltechTHESIS
Deposited By: Imported from ETD-db
Deposited On:31 May 2005
Last Modified:26 Dec 2012 02:47

Thesis Files

[img]
Preview
PDF (thesis.pdf) - Final Version
See Usage Policy.

836Kb

Repository Staff Only: item control page