CaltechAUTHORS
  A Caltech Library Service

Convex Programs for Temporal Verification of Nonlinear Dynamical Systems

Prajna, Stephen and Rantzer, Anders (2007) Convex Programs for Temporal Verification of Nonlinear Dynamical Systems. SIAM Journal on Control and Optimization, 48 (3). pp. 999-1021. ISSN 0363-0129. doi:10.1137/050645178. https://resolver.caltech.edu/CaltechAUTHORS:PRAsiamjco07

[img]
Preview
PDF
See Usage Policy.

324kB

Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:PRAsiamjco07

Abstract

A methodology for safety verification of continuous and hybrid systems using barrier certificates has been proposed recently. Conditions that must be satisfied by a barrier certificate can be formulated as a convex program, and the feasibility of the program implies system safety in the sense that there is no trajectory starting from a given set of initial states that reaches a given unsafe region. The dual of this problem, i.e., the reachability problem, concerns proving the existence of a trajectory starting from the initial set that reaches another given set. Using insights from the linear programming duality appearing in the discrete shortest path problem, we show in this paper that reachability of continuous systems can also be verified through convex programming. Several convex programs for verifying safety and reachability, as well as other temporal properties such as eventuality, avoidance, and their combinations, are formulated. Some examples are provided to illustrate the application of the proposed methods. Finally, we exploit the convexity of our methods to derive a converse theorem for safety verification using barrier certificates.


Item Type:Article
Related URLs:
URLURL TypeDescription
https://doi.org/10.1137/050645178DOIUNSPECIFIED
Additional Information:©2007 Society for Industrial and Applied Mathematics. Received by the editors November 15, 2005; accepted for publication (in revised form) September 26, 2006; published electronically June 29, 2007. Preliminary versions of this paper appeared in Hybrid Systems: Computation and Control 2005 and Proceedings of the IFAC World Congress 2005.
Subject Keywords:temporal verification; safety verification; reachability analysis; barrier certificate; density function; convex programming; duality
Issue or Number:3
DOI:10.1137/050645178
Record Number:CaltechAUTHORS:PRAsiamjco07
Persistent URL:https://resolver.caltech.edu/CaltechAUTHORS:PRAsiamjco07
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:9034
Collection:CaltechAUTHORS
Deposited By: Archive Administrator
Deposited On:22 Oct 2007
Last Modified:08 Nov 2021 20:55

Repository Staff Only: item control page