Convex programs for temporal verification of nonlinear dynamical systems
Prajna, Stephen and Rantzer, Anders LU
(2007)
In SIAM Journal of Control and Optimization
46(3).
p.999-1021
- Abstract
- A methodology for safety verification of continuous and hybrid systems using barrier certi.ficates has been proposed recently. Conditions that must be satisfi.ed by a barrier certi. cate 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... (More)
- A methodology for safety verification of continuous and hybrid systems using barrier certi.ficates has been proposed recently. Conditions that must be satisfi.ed by a barrier certi. cate 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 veri. ed 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 veri. cation using barrier certificates. (Less)
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/656877
- author
- Prajna, Stephen
and Rantzer, Anders
LU
- organization
- publishing date
- 2007
- type
- Contribution to journal
- publication status
- published
- subject
- keywords
- density function, barrier certificate, reachability analysis, temporal verification, safety verification, convex programming, duality
- in
- SIAM Journal of Control and Optimization
- volume
- 46
- issue
- 3
- pages
- 999 - 1021
- publisher
- Society for Industrial and Applied Mathematics
- external identifiers
-
- wos:000249318700010
- scopus:34548217202
- ISSN
- 1095-7138
- DOI
- 10.1137/050645178
- language
- English
- LU publication?
- yes
- id
- 0ae78723-21ea-4ad8-baeb-f1caa77dc670 (old id 656877)
- date added to LUP
- 2016-04-01 12:10:38
- date last changed
- 2023-11-11 15:37:44
@article{0ae78723-21ea-4ad8-baeb-f1caa77dc670,
abstract = {{A methodology for safety verification of continuous and hybrid systems using barrier certi.ficates has been proposed recently. Conditions that must be satisfi.ed by a barrier certi. cate 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 veri. ed 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 veri. cation using barrier certificates.}},
author = {{Prajna, Stephen and Rantzer, Anders}},
issn = {{1095-7138}},
keywords = {{density function; barrier certificate; reachability analysis; temporal verification; safety verification; convex programming; duality}},
language = {{eng}},
number = {{3}},
pages = {{999--1021}},
publisher = {{Society for Industrial and Applied Mathematics}},
series = {{SIAM Journal of Control and Optimization}},
title = {{Convex programs for temporal verification of nonlinear dynamical systems}},
url = {{http://dx.doi.org/10.1137/050645178}},
doi = {{10.1137/050645178}},
volume = {{46}},
year = {{2007}},
}